Commit graph

46 commits

Author SHA1 Message Date
Ravishankar Bhagavandas
e39c34ba7e
Adding unit tests for stream buffer and message buffer (#528)
* Initial commit

* Add more stream buffer tests

* Adding message buffer tests

* Adding tests to cover config assert branches

Co-authored-by: alfred gedeon <28123637+alfred2g@users.noreply.github.com>
2021-03-30 12:56:02 -07:00
Paul Bartell
7020db5403
Force a branch in the definition of configASSERT in the default CMock FreeRTOSConfig.h file (#538)
* Force a branch in the definition of configASSERT in the default CMock FreeRTOSConfig.h file
* Run uncrustify on FreeRTOSConfig.h
2021-03-24 13:08:15 -07:00
Paul Bartell
92aca6e910
Collect initial coverage data so that untagged functions are still included in the lcov report (#537)
Collect initial coverage data with lcov --initial and add this to coverage data to the combined coverage from each test binary.
This ensures that all functions in the target file(s) are included in coverage statistics, even if those functions are not tagged in a _utest.c file.
Note: Functions which are excluded by the preprocessor will not have initial coverage data generated for them.
2021-03-23 18:41:14 -07:00
Paul Bartell
3a48781a03 Skip filtering of coverage if no @coverage tags are found in a _utest.c file 2021-03-22 14:58:52 -07:00
Paul Bartell
f39765be22
Kernel UT: Enable preprocessor when running cflow in callgraph.py (#530)
* Add INCLUDE_DIR to the commandline call to cflow in callgraph.py

This removes dependent functions from the list when they are disabled in the FreeRTOS config.

* Add argparse to callgraph.py so that no output file is created on failure.
2021-03-19 17:30:20 -07:00
Paul Bartell
6257160ee6
Make the address sanitizer optional for CMock kernel unit tests (#526)
* Make the address sanitizer optional

The address sanitizer is now disabled by default for CMock tests because it introduces additional branches into the compiled code. When make is run with the ENABLE_SANITIZER=1 argument, the address sanitizer is enabled and coverage data may not be accurate.

* Change from ifdef to ifeq ($(ENABLE_SANITIZER),1) to address PR comment
2021-03-16 13:55:01 -07:00
Paul Bartell
d7e5f40885
Clean up CMock makefiles and add coverage filtering (#523)
* Cleanup Makefiles

* Add lcovrc configuration file

* Add CMock test build directory to .gitignore

* Add callgraph.py and filtercov.py scripts

* Cleanup list Makefile and update list_utest.c with coverage tags

* Add information about coverage filtering and running single test cases

* Remove -fprofile-exclude-files for compatibility with older versions of gcc.
Fix line endings (change to unix style)

* Lint callgraph.py and filtercov.py. Print and error when no target functions are defined.

* Indent with spaces when possible

* Replace tabs with spaces and enable .RECIPEPREFIX

* Add fake_port.h and related portmacro.h changes

* Fix list makefile when bin directory is not available

* Clean up grouped rules

* Update makesfile.. Add "two_tests" example dir

* Fix memory checker error

* Move common makefile items to subdir.mk and testdir.mk includes

* Update core_checker.py exclusions

* Remove line from portmacro.h that doesn't match core_checker.py
2021-03-15 17:01:29 -07:00
Nathan Chong
5309372245
Minor VeriFast proof changes to match V10.4.3 (#519)
* Minor changes for V10.4.3

* Update license
2021-02-25 14:00:22 -07:00
Paul Bartell
570ae6bb52
Add unity memory extension, fake_assert, and enable -fsanitize=address (#506)
* Enable libunitymemory extension to track dynamic memory usage during unit tests
* Use UnityMemory in timers_utest.c
* Add fake_assert.h to allow mocking of configASSERT calls
* Add .editorconfig to make github show indentation correctly
* Add unity memory and fake_assert to queue_utest.c
* Add -fsanitize=address CFLAG when running unit tests
* Define mtCOVERAGE_TEST_MARKER macro to include mtCOVERAGE_TEST_MARKER lines in coverage figures
* Add additional memory check / protection CFLAGS for CMock tests
* Fix out of bounds array access in list_utest.c
* Move the fake_assert.h include to the top of FreeRTOSConfig.h
2021-02-18 10:15:01 -08:00
alfred gedeon
c4d8002634
Generate JUnit style report for kernel unit test (#504)
* Add JUnit test report to ut
* Add JUnit test report with make run
* Fix gcc path
2021-02-15 14:09:24 -08:00
David Chalco
63aec3607d
Unit Test/timer[0] (#502)
* define CC/LD iff undef. Add timers suite

* timers_utest[0]
2021-02-14 11:24:55 -08:00
Carl Lundin
f6dff3fea3
Add Litani to run CBMC proofs (#501)
Update to out of source makefile build and add run-cbmc-proofs.py

CBMC proofs can now be run with Litani with the command
"./run-cbmc-proofs.py"

Based on commits:
* 1646301 - Ignore CBMC proof failures, fail the build later (4 months ago) <Kareem Khazem>
* 7e8c91a - Fix Makefile prerequisite symbol for CBMC proofs (4 months ago) <Kareem Khazem>
* bee04be - Enable CBMC proofs to run in CI (4 months ago) <Kareem Khazem>

Found in https://github.com/FreeRTOS/FreeRTOS-Plus-TCP
2021-02-12 10:21:07 -08:00
alfred gedeon
cd92c42b52
Kernel list.c Unit Test (#497)
* Test: List.c Unit Test

* Test: test list.h macros

* Test: Fix UT bug

* Remove unecessary statement from Makefile

* Update list_utest.c

* Update list_utest.c

Co-authored-by: Cobus van Eeden <35851496+cobusve@users.noreply.github.com>
2021-02-11 18:10:49 -08:00
alfred gedeon
9b9011917a
Add Kernel Unit Tests Environment (#494)
* Implement Kernel Unit Test Framework with CMock

* Add Readme.md to unit tests

* Add Posix build checker to git actions

* Add Ruby requirement

* Fix file header checks

* Fix header checks

* Add color output to test runs
2021-02-08 15:26:01 -08:00
Joseph Julicher
da9b9a800d [AUTO][RELEASE]: Bump file header version to "202012.00" 2020-12-15 11:50:37 -07:00
Joseph Julicher
2e2ba99a74 [AUTO][RELEASE]: Bump file header version to "202012.00" 2020-12-15 10:20:29 -07:00
Carl Lundin
b035e0321f
Re-add missing license files caused by PR #471 and fix patches (#477)
* Re-add missing license files caused by PR #471.
* Fix proof patch.
2020-12-14 17:35:36 -08:00
Carl Lundin
cf39a90d6d
Fix CBMC patches. (#471)
* Fix CBMC patches.
2020-12-12 21:00:03 -08:00
Ming Yue
9d937aa0ab
Remove duplicate WinBase.h and Windows.h. (#458) 2020-12-09 13:40:20 -08:00
Cobus van Eeden
c6f4284b76
Update kernel submodule pointer to version 47338393f (#456)
* Update kernel submodule pointer to version 47338393f

* Fix patches.

Co-authored-by: Carl Lundin <lundinc@amazon.com>
2020-12-08 15:44:14 -08:00
David Chalco
07f3cbafee [AUTO][RELEASE]: Bump file header version to "202011.00" 2020-11-10 14:45:34 -08:00
Nathan Chong
bc54c6bc10
Syntactic proof changes to track 10.4.1 changes (#322)
All changes restricted to comments/formatting.
2020-10-06 13:17:29 -07:00
Aniruddha Kanhere
8979b3817b
Remove CBMC proofs of TCP source code (#325)
* Add CMock back for the integration tests.

* Removed the CBMC proofs for TCP

* Add the windows files to allow the CBMC proofs to run
2020-10-06 13:03:52 -07:00
David Chalco
7bcc5b48b1
Move ./scripts --> FreeRTOS/Test/CMock/scripts (#298) 2020-09-24 17:17:34 -07:00
David Chalco
190c9e780d
Inititial stub for cmock tests (#297) 2020-09-24 17:06:28 -07:00
Cobus van Eeden
d5862dbe01
Sync back V10.4.1 (#282)
* Move Kernel submodule pointer to 10.4.1
* Update version number to V10.4.1 (#281)
2020-09-17 17:16:33 -07:00
David Chalco
89d475e9b1
Update Version number to 10.4.0 (#237) 2020-09-10 19:40:24 -07:00
Ravishankar Bhagavandas
584517d467
cbmc: Add patch to remove overflow assert (#232) 2020-09-01 09:26:25 -07:00
Nathan Chong
669084ee8f
List proofs and signoff (#194) 2020-08-27 11:59:12 -07:00
Cobus van Eeden
4a026fd703
Move forward Kernel submodule pointer (#218)
* Move forward Kernel submodule pointer
* Fixing patches for CBMC proofs
* Update proofs to assume cTxLock != 127
* Update proofs to assume cRxLock != 127
2020-08-26 23:50:09 -07:00
Cobus van Eeden
a691c6199e
Updating queue.c patches for CBMC proofs (#216) 2020-08-26 13:07:15 -07:00
Aniruddha Kanhere
f32a0647c8
Remove CBMC patch which is not used anymore (#187)
* Delete 0002-Change-FreeRTOS_IP_Private.h-union-to-struct.patch

* Delete 0002-Change-FreeRTOS_IP_Private.h-union-to-struct.patch
2020-08-03 16:45:10 -07:00
Aniruddha Kanhere
08af68ef90
Remove dependency of CBMC on Patches (#181)
* Changes to DHCP

* CBMC DNS changes

* Changes for TCP_IP

* Changes to TCP_WIN

* Define away static to nothing

* Remove patches

* Changes after Mark's comments v1

* Update MakefileCommon.json

* Correction!
2020-08-01 16:38:23 -07:00
Aniruddha Kanhere
f2611cc5e5
MISRA compliance changes in FreeRTOS_Sockets{.c/.h} (#161)
* MISRA changes Sockets

* add other changes

* Update FreeRTOSIPConfig.h

* Update FreeRTOSIPConfig.h

* Update FreeRTOSIPConfig.h

* Update FreeRTOSIPConfig.h

* correction

* Add 'U'

* Update FreeRTOS_Sockets.h

* Update FreeRTOS_Sockets.h

* Update FreeRTOS_Sockets.c

* Update FreeRTOS_Sockets.h

* Update after Gary's comments

* Correction reverted
2020-07-29 15:38:37 -07:00
Nathan Chong
8e36bee30e
Prove buffer lemmas (#124)
* Prove buffer lemmas

* Update queue proofs to latest kernel source

All changes were syntactic due to uncrustify code-formatting

* Strengthen prvCopyDataToQueue proof

* Add extract script for diff comparison

Co-authored-by: Yuhui Zheng <10982575+yuhui-zheng@users.noreply.github.com>
2020-07-21 09:51:20 -07:00
Nathan Chong
529c481c39
Add VeriFast kernel queue proofs (#117) 2020-07-02 12:55:20 -07:00
Aniruddha Kanhere
f11bcc8acc
Fix a Bug and corresponding CBMC patch (#84)
* Update remove-static-in-freertos-tcp-ip.patch

* Update FreeRTOS_TCP_IP.c

* Update remove-static-in-freertos-tcp-ip.patch

* Update remove-static-in-freertos-tcp-ip.patch

Co-authored-by: Yuhui Zheng <10982575+yuhui-zheng@users.noreply.github.com>
2020-06-03 16:52:31 -07:00
Aniruddha Kanhere
cb7edd2323
Sync with a:FR (#75)
* AFR sync

* AFR sync: CBMC

* AFR sync: CBMC: remove .bak files

* AFR sync: CBMC: more cleanup

* Corrected CBMC proofs

* Corrected CBMC patches

* Corrected CBMC patches-1

* Corrected CBMC patches-2

* remove .bak files (3)

Co-authored-by: Yuhui Zheng <10982575+yuhui-zheng@users.noreply.github.com>
2020-05-28 10:11:58 -07:00
AniruddhaKanhere
d95624c5d6
Move CBMC proofs to FreeRTOS+ directory (#64)
* move CBMC proofs to FreeRTOS+ directory

* Failing proofs corrected

* ParseDNSReply proof added back

* removed queue_init.h from -Plus/Test

Co-authored-by: Yuhui Zheng <10982575+yuhui-zheng@users.noreply.github.com>
2020-05-05 09:57:18 -07:00
markrtuttle
95ae7c6575
Change cbmc-viewer invocation in CBMC makefile (#63)
* Exclude FreeRTOS/Demo from CBMC proof reports.

The script cbmc-viewer generates the CBMC proof reports.  The script
searches source files for symbol definitions and annotates source
files with coverage information.  This patch causes cbmc-viewer to
ignore the directory FreeRTOS/Demo containing 348M of data.  The
script now terminates in a few seconds.

* Make report default target for CBMC Makefile.

Modify the Makefile for CBMC proofs to generate the report by default
(and not just property checking) and modify property checking to
ignore failures (due to property assertions failing) and terminating
report generation.

Co-authored-by: Mark R. Tuttle <mrtuttle@amazon.com>
2020-04-28 21:27:45 -07:00
Yuhui Zheng
d421ccc89f
Reword readme.md under ./Test. (#61) 2020-04-25 16:57:35 -07:00
Carl Lundin
3841286598
Removed a:FR reference. (#60) 2020-04-25 16:56:54 -07:00
AniruddhaKanhere
4db195c916
Adding FreeRTOS+TCP CBMC proofs to FreeRTOS/FreeRTOS (#56)
ParseDNSReply is to be added in the next PR.
2020-04-21 15:40:08 -07:00
Yuhui Zheng
5b9777e11e A readme file to introduce what ./Test directory is about. 2020-03-31 14:21:53 -07:00
Yuhui Zheng
211bb4cbd9 Ignore whitespace when working with patches. 2020-03-31 14:21:53 -07:00
Yuhui Zheng
8156f64d1c Copying CBMC proofs from aws/amazon-freertos repo ./tools/cbmc to this repo ./FreeRTOS/Test/CBMC as is.
The commit ID in aws/amazon-freertos is 0c8e0217f2a43bdeb364b58ae01c6c259e03ef1b.
2020-03-31 14:21:53 -07:00