01e59a036c
Restructure platform directory ( #382 )
...
This updates the platform and logging directory and moves it to the following places:
FreeRTOS\FreeRTOS-Plus\Source\Utilities
FreeRTOS\FreeRTOS-Plus\Source\Application-Protocols\network_transport\freertos_plus_tcp
Project files are updated to follow suite. All updated demos are tested to work as expected.
2020-11-05 16:47:43 -08:00
330b8c002f
Delete printf-stdarg.c and move logging.c from Source/Logging ( #381 )
...
printf-stdarg.c seems have to been moved by mistake when moving logging sources to a common folder.
Also, because logging.c is specific to Windows, it is moved to FreeRTOS-Plus/Demo/Common/Logging/Logging_WinSim.c.
2020-11-05 10:12:06 -08:00
10842c9189
Relocate logging sources under FreeRTOS-Plus/Source/Logging ( #354 )
...
As suggested, because logging_stack.h and logging_levels.h are used not only by demos but also by platform-specific transport code, it would make sense to move FreeRTOS-Plus/Demos/Common/Logging to FreeRTOS-Plus/Source/Logging. The same is done for demo_logging.c and demo_logging.h, which are duplicated by several demos. Win32.vcxproj project files are also updated to follow suite.
2020-10-20 20:31:54 -07:00
56d44da270
Exercise xTaskDelayUntil() in demos and tests ( #335 )
...
* Update AbortDelay.c so it uses both vTaskDelayUntil() and xTaskDelayUntil().
Update TaskNotifyArray.c to prevent false positive test failures that appear to be caused by unwarranted integer promotion.
Add use of xTaskDelayUntil() to blocktim.c
2020-10-11 17:07:09 -07:00
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
