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
d37b651e77
Add CMock back for the integration tests. ( #321 )
2020-10-05 14:07:28 -07:00
a6393ee653
This PR adds the TCP submodule to the FreeRTOS/FreeRTOS repo ( #307 )
...
* MISRA v5
* Remove TCP code
* Add TCP submodule
* Remove unit test and CMock submodule
* Update submodule pointer
2020-10-05 13:20:42 -07:00
cdf6d93cb9
Modify CBMC proofs to make assumptions about malloc explicit. ( #312 )
...
Some proofs assume that some pointers returned by malloc are not
NULL. This patch modifies those proofs to make these assumptions
explicit with `__CPROVER_assume(pointer != NULL)` for all such
pointers.
Co-authored-by: Mark R. Tuttle <mrtuttle@amazon.com>
Co-authored-by: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
2020-10-02 18:18:16 -04:00
a8290734d8
Bring in the patches from FreeRTOS dir to FreeRTOS-Plus ( #306 )
...
* MISRA v5
* Update patches in FreeRTOS-Plus to match those in FreeRTOS
2020-10-01 16:04:56 -04:00
6fb8b1fc33
+TCP: Fix spellings ( #302 )
...
* MISRA v5
* Add spelling corrections
* Update after Shubham's comments
* Actually fix the spelling
2020-09-28 12:55:22 -04:00
1fc1bd4321
Add CBMC proofs for FreeRTOS-Plus-CLI ( #296 )
2020-09-24 13:32:10 -07:00
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
89d475e9b1
Update Version number to 10.4.0 ( #237 )
2020-09-10 19:40:24 -07:00
40e410ee8e
Create winbase.h ( #248 )
2020-09-08 12:15:59 -07:00
66371d0cf0
Add CBMC proof for prvProcessEthernetPacket ( #199 )
...
* Add proof
* Remove and Rename files
* Modify the makefile
* Update Makefile.json
* Add _static to FreeRTOS_IP.c
* Update prvProcessEthernetPacket_harness.c
* Update the proof and add list to stubs
* add assertions
* Update the proof
* cleanup
* Update
* Update after @yanjos-dev's comment
* Remove unnecessary assumption
2020-08-27 16:25:17 -07:00
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
86117b5173
CBMC proof for vProcessGeneratedUDPPacket ( #203 )
...
* Add Proof
* Update
* Update the proof
* Update the proof
* Clean-up
* Clean-up v2
* Update freertos_api.c
* update stub
2020-08-24 17:06:31 -07:00
3c573ad091
CBMC proof for ulARPRemoveCacheEntryByMac ( #198 )
...
* Add Proof
* update
* Delete ulARPRemoveCacheEntryByMAC_harness.c
* Changes after Mark's comments
* Update after @yanjos-dev's comment
* Remove confusing variable name
* Update ulARPRemoveCacheEntryByMac_harness.c
2020-08-24 16:46:50 -07:00
6eba275f89
CBMC: Add proof for vSocketBind ( #202 )
...
* Add proof
* Update
* Update MakefileCommon.json
* Undo changes
* Undo changes in MakefileCommon.json
* Update Makefile.json
* Update Makefile.json
* Update Makefile.json
* Change v1
* Change v2
2020-08-24 11:35:48 -07:00
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
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
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
7caa328634
Add Full TCP test suite - not using secure sockets ( #131 )
...
* Add Full-TCP suite
* delete unnecessary files
* Change after Joshua's comments
2020-07-10 23:32:30 -07:00
a9b2aac4e9
Folder structure change + Fix broken Projects ( #103 )
...
* Update folder structure
* Correct project files
* Move test folder
* Some changes after Yuki's comments
2020-06-26 12:09:36 -07:00
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
6efc39f44b
Add Project for running integration tests v2 ( #80 )
...
* Project for integration tests
* relative paths in project files
* relative paths in project files-1
* relative paths in project files-2
* addressed comments
* addressed comments v2
Co-authored-by: Yuhui Zheng <10982575+yuhui-zheng@users.noreply.github.com>
2020-06-02 15:09:25 -07:00
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
95a3a02f95
FreeRTOS-Plus: Unit testing Infrastructure and examples ( #72 )
...
* Added CMock as submodule
* Makefile added
* Removed TEMP from Makefile
* Added configuration files and header files
* Update Makefile
* Test runner working
* make clean
* Example added with README
* Update README.md
* Restored +TCP files
* Cleared +TCP changes
* removed comments from Makefile
* Update README.md
* Update README.md
* Update README.md
* Updated Test/Unit-test/readme.md
2020-05-22 16:26:59 -07:00
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
