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
