Commit Graph

33 Commits (68a500bca34b7924d6b8f61ccbee779beedd7675)

Author SHA1 Message Date
Joseph Julicher da9b9a800d [AUTO][RELEASE]: Bump file header version to "202012.00" 4 years ago
David Chalco 07f3cbafee [AUTO][RELEASE]: Bump file header version to "202011.00" 4 years ago
David Chalco 82916bfda8
Manual version update - files not autoversioned with upcoming prefix (#399) 4 years ago
Oscar Michael Abrina c7cd06488f
Update path for WinSim logging port (#385)
Moves Logging_WinSim.c to a nested windows folder
4 years ago
Oscar Michael Abrina 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.
4 years ago
Oscar Michael Abrina 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.
4 years ago
Oscar Michael Abrina 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.
4 years ago
RichardBarry 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
4 years ago
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
4 years ago
Aniruddha Kanhere d37b651e77
Add CMock back for the integration tests. (#321) 4 years ago
Aniruddha Kanhere 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
4 years ago
markrtuttle 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>
4 years ago
Aniruddha Kanhere a8290734d8
Bring in the patches from FreeRTOS dir to FreeRTOS-Plus (#306)
* MISRA v5

* Update patches in FreeRTOS-Plus to match those in FreeRTOS
4 years ago
Aniruddha Kanhere 6fb8b1fc33
+TCP: Fix spellings (#302)
* MISRA v5

* Add spelling corrections

* Update after Shubham's comments

* Actually fix the spelling
4 years ago
Ravishankar Bhagavandas 1fc1bd4321
Add CBMC proofs for FreeRTOS-Plus-CLI (#296) 4 years ago
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)
4 years ago
David Chalco 89d475e9b1
Update Version number to 10.4.0 (#237) 4 years ago
Aniruddha Kanhere 40e410ee8e
Create winbase.h (#248) 4 years ago
Aniruddha Kanhere 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
4 years ago
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
4 years ago
Aniruddha Kanhere 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
5 years ago
Aniruddha Kanhere 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
5 years ago
Aniruddha Kanhere 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
5 years ago
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
5 years ago
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!
5 years ago
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
5 years ago
Aniruddha Kanhere 7caa328634
Add Full TCP test suite - not using secure sockets (#131)
* Add Full-TCP suite

* delete unnecessary files

* Change after Joshua's comments
5 years ago
Aniruddha Kanhere a9b2aac4e9
Folder structure change + Fix broken Projects (#103)
* Update folder structure

* Correct project files

* Move test folder

* Some changes after Yuki's comments
5 years ago
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>
5 years ago
Aniruddha Kanhere 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>
5 years ago
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>
5 years ago
Aniruddha Kanhere 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
5 years ago
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>
5 years ago