diff options
| author | lundinc <lundinc@1d2547de-c912-0410-9cb9-b8ca96c0e9e2> | 2020-08-12 19:11:51 +0000 |
|---|---|---|
| committer | lundinc <lundinc@1d2547de-c912-0410-9cb9-b8ca96c0e9e2> | 2020-08-12 19:11:51 +0000 |
| commit | 42255af1e27a3157d541f0812eaca447c569ca49 (patch) | |
| tree | 5c8702c2f0dc1cb9be1a4d5ff285897d96b97dd2 /FreeRTOS/Test/CBMC/patches | |
| parent | f5221dff43de249079c2da081723cb7a456f981f (diff) | |
| download | freertos-master.tar.gz | |
Author: Ming Yue <mingyue86010@gmail.com>
Date: Tue Aug 11 17:06:59 2020 -0700
Remove unused wolfSSL files. (#197)
* Remove unused wolfSSL files.
* Add back some removed ciphers.
* Update VS project file.
commit 0e0edd96e8236b2ea4a6e6018812807be828c77f
Author: RichardBarry <3073890+RichardBarry@users.noreply.github.com>
Date: Tue Aug 11 10:50:30 2020 -0700
Use new QEMU test project to improve stream/message buffer tests (#168)
* Add Eclipse/GCC project that targets the LM3S8962 QEMU model.
* Get the Cortex-M QEMU project working.
* Continue working on making stream buffer demo more robust and QEMU project.
* Rename directory CORTEX_LM3S8986_QEMU to CORTEX_LM3S6965_QEMU.
Work on making the Stream Buffer tests more robust.
Check in before adding in the trace recorder.
* Rename CORTEX_LM3S6969_QEMU to CORTEX_LM3S6969_GCC_QEMU.
* Make the StreamBufferDemo.c common demo file (test file) more robust to other test tasks running at an equally high priority.
* Work in progress checkin only - comments in main.c are incorrect.
* Correct comments at the top of FreeRTOS/Demo/CORTEX_LM3S6965_GCC_QEMU/main.c
Make the message buffer tests more robust in the case the a message buffer becomes full when prvSenderTask() has a higher priority than the reader task.
* Disable trace recorder in the LM3S6965 QEMU demo.
* I'm dropping FreeRTOS-Kernel reference update, since this seems to break the CMBC CI.
Co-authored-by: Yuhui Zheng <10982575+yuhui-zheng@users.noreply.github.com>
commit 157a7fc39f19583ac8481e93fa3e1c91b1e1860c
Author: Gaurav-Aggarwal-AWS <33462878+aggarg@users.noreply.github.com>
Date: Sun Aug 9 22:21:44 2020 -0700
Use chacheable RAM in IAR project for MPU_M7_NUCLEO_H743ZI2 project (#193)
This change updates the IAR project for Nucleo H743ZI2 to use the
cacheable DTC RAM and enables L1 cache. In order to ensure the correct
functioning of cache, the project sets configTEX_S_C_B_SRAM in
FreeRTOSConfig.h to not mark the RAM as shareable.
Signed-off-by: Gaurav Aggarwal <aggarg@amazon.com>
commit f3e43556f90f01b82918ad533b0c616489331919
Author: Gaurav-Aggarwal-AWS <33462878+aggarg@users.noreply.github.com>
Date: Sun Aug 9 16:23:53 2020 -0700
Add MPU demo projects for NUCLEO-H743ZI2 board (#155)
* Add MPU demo projects for NUCLEO-H743ZI2 board
It contains projects for Keil uVision, STM32CubeIDE and IAR EW. This
demo shows the use of newly added support for 16 MPU regions.
Signed-off-by: Gaurav Aggarwal <aggarg@amazon.com>
* Delete not needed CMSIS files
Signed-off-by: Gaurav Aggarwal <aggarg@amazon.com>
commit 94aa31c3cbae7c929b8a412768b74631f4a6b461
Author: TakayukiMatsuo <62984531+TakayukiMatsuo@users.noreply.github.com>
Date: Sat Aug 8 07:58:14 2020 +0900
Update wolfSSL to the latest version(v.4.4.0) (#186)
* deleted old version wolfSSL before updating
* updated wolfSSL to the latest version(v4.4.0)
* updated wolfSSL to the latest version(v4.4.0)
* added macros for timing resistance
Co-authored-by: RichardBarry <3073890+RichardBarry@users.noreply.github.com>
Co-authored-by: Ming Yue <mingyue86010@gmail.com>
commit 68518f5866aac58793c737d9a46dd07a6a816aaf
Author: RichardBarry <3073890+RichardBarry@users.noreply.github.com>
Date: Fri Aug 7 14:59:24 2020 -0700
Removed a 16MByte flash image file that was checked in by mistake (several years ago). (#173)
Remove the copies of lwIP that are no longer reference from demo projects.
Co-authored-by: Carl Lundin <53273776+lundinc2@users.noreply.github.com>
commit d4bf09480a2c77b1a25cce35b32293be61ab586f
Author: m17336 <45935231+m17336@users.noreply.github.com>
Date: Thu Aug 6 22:37:08 2020 +0300
Update previous AVR ATmega0 and AVR Dx projecs + addition of equivalent projects in MPLAB.X and IAR (#180)
* Updated indentation in AVR_ATMega4809_Atmel_Studio and AVR_Dx_Atmel_Studio projects, plus small fixes in their readme files.
* Added AVR_ATMega4809_IAR, AVR_ATMega4809_MPLAB.X, AVR_Dx_IAR and AVR_Dx_MPLAB.X demo projects.
* Removed build artefacts and added .gitignore files in AVR_ATMega4809_MPLAB.X and AVR_Dx_MPLAB.X projects.
Co-authored-by: Yuhui Zheng <10982575+yuhui-zheng@users.noreply.github.com>
commit f32a0647c8228ddd066f5d69a85b2e49086e4c95
Author: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
Date: Mon Aug 3 16:45:10 2020 -0700
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
commit 08af68ef9049279b265c3d00e9c48fb9594129a8
Author: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
Date: Sat Aug 1 16:38:23 2020 -0700
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!
commit a7fec906a415363338449447daf10d7517b78848
Author: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
Date: Wed Jul 29 17:39:36 2020 -0700
Misc changes (#183)
commit 07cf5e07e4a05d6775a2f9e753269f43f82cf6ba
Author: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
Date: Wed Jul 29 16:15:38 2020 -0700
MISRA compliance changes for FreeRTOS+TCP headers (#165)
* misra changes
* Update FreeRTOS_IP_Private.h
* Update FreeRTOS_IP_Private.h
commit e903ac0fed7ce59916899e404f3e5ae5b08d1478
Author: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
Date: Wed Jul 29 16:03:14 2020 -0700
UPD MISRA changes (#164)
Co-authored-by: Yuhui Zheng <10982575+yuhui-zheng@users.noreply.github.com>
commit 97551bf44e7dc7dc1e4484a8fd30f699255e8569
Author: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
Date: Wed Jul 29 15:52:00 2020 -0700
MISRA changes in FreeRTOS_TCP_WIN.c (#162)
commit f2611cc5e5999c4c87e040a8c2d2e6b5e77a16a6
Author: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
Date: Wed Jul 29 15:38:37 2020 -0700
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
commit ae4d4d38d9b2685bae159b4c87619cdb157c0bf7
Author: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
Date: Wed Jul 29 13:56:57 2020 -0700
MISRA compliance changes for FreeRTOS_TCP_IP.c (#160)
* MISRA tcp-ip changes
* Changes after Hein's comments on original PR
* Update FreeRTOS_TCP_IP.c
Co-authored-by: Yuhui Zheng <10982575+yuhui-zheng@users.noreply.github.com>
commit a457f43c66eb0f4be9d8f8678c0e3fb8d7ebd57b
Author: Carl Lundin <53273776+lundinc2@users.noreply.github.com>
Date: Tue Jul 28 13:01:38 2020 -0700
Add missing error state assignment. (#166)
commit 915af50524e15a78ceb6c62b3d33f6562621ee46
Author: Yuhui Zheng <10982575+yuhui-zheng@users.noreply.github.com>
Date: Mon Jul 27 17:30:53 2020 -0700
Add Atmel Studio projects for ATMega4809 and AVR128DA48 (#159)
* Added explicit cast to allow roll over and avoid integer promotion during cycles counters comparison in recmutex.c.
* Fixed type mismatch between declaration and definition of function xAreSemaphoreTasksStillRunning( void ).
* Added Atmel Studio demo projects for ATMega4809 and AVR128DA48.
* Per https://www.freertos.org/upgrading-to-FreeRTOS-V8.html, I'm updating portBASE_TYPE to BaseType_t.
Signed-off-by: Yuhui Zheng <10982575+yuhui-zheng@users.noreply.github.com>
* Update register test for ATmega4809
- to cover r28, r29, r31.
- call public API taskYIELD() instead of portYIELD().
* Update ATmega4809 readme.md to include info for serial port setup, and minor wording fix.
Co-authored-by: Alexandru Niculae - M17336 <alexandru.niculae@microchip.com>
commit 4a7a48790d64127f85cc763721b575c51c452833
Author: Carl Lundin <53273776+lundinc2@users.noreply.github.com>
Date: Thu Jul 23 10:22:33 2020 -0700
Add Uncrustify file used for Kernel. (#163)
commit e0d62163b08769fd74f020709c398f994088ca96
Author: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
Date: Wed Jul 22 18:06:23 2020 -0700
Sync with +TCP amazon-FreeRTOS (#158)
* DNS.c commit
* IP.c commit
* Add various source & header files
commit 8e36bee30eef2107e128edb58e83ee46e8241a91
Author: Nathan Chong <52972368+nchong-at-aws@users.noreply.github.com>
Date: Tue Jul 21 12:51:20 2020 -0400
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>
commit c720c18ada40b502436ea811e8d03dca919726d8
Author: Hein Tibosch <hein_tibosch@yahoo.es>
Date: Tue Jul 14 05:35:44 2020 +0800
FreeRTOS+TCP Adding the combined driver for SAM4E and SAME70 v2 (#78)
* Adding a combined +TCP driver for SAM4E and SAME70
* Changes after review from Aniruddha
Co-authored-by: Hein Tibosch <hein@htibosch.net>
Co-authored-by: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
commit 4237049b12d9bb6b03694fecf6ea26a353e637c8
Author: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
Date: Mon Jul 13 12:07:56 2020 -0700
Add changes from 2225-2227 amazon-FreeRTOS (#134)
commit 7caa32863458c4470d3c620945c30824199f524c
Author: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
Date: Fri Jul 10 23:32:30 2020 -0700
Add Full TCP test suite - not using secure sockets (#131)
* Add Full-TCP suite
* delete unnecessary files
* Change after Joshua's comments
commit d7667a0034841f2968f9f9f805030cc608bfbce1
Author: Gaurav-Aggarwal-AWS <33462878+aggarg@users.noreply.github.com>
Date: Fri Jul 3 15:45:44 2020 -0700
Remove unnecessary semicolon from the linker file (#121)
This was creating problem with the onboard LPCLink debug probe.
Signed-off-by: Gaurav Aggarwal <aggarg@amazon.com>
commit 529c481c39506d0b331bfd0cdea35e5d1aeaaad0
Author: Nathan Chong <52972368+nchong-at-aws@users.noreply.github.com>
Date: Thu Jul 2 15:55:20 2020 -0400
Add VeriFast kernel queue proofs (#117)
commit d5fedeaa96b5b1d3c0f6b9b52a8064ab72ff2821
Author: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
Date: Wed Jul 1 13:56:27 2020 -0700
Add checks in FreeRTOS_Socket.c (#104)
* Add fail-safes to FreeRTOS_Socket.c
* Use all 'pd' errors
* Correction after Hein's comments
* Correction after Hein's comments v2
* Changes after Hein's comments
* Update after Gary's comments
commit a9b2aac4e9fda2a259380156df9cc0af51384d2d
Author: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
Date: Fri Jun 26 12:09:36 2020 -0700
Folder structure change + Fix broken Projects (#103)
* Update folder structure
* Correct project files
* Move test folder
* Some changes after Yuki's comments
commit 98bfc38bf3404414878dc68ea41753bea4e24c8e
Author: Hein Tibosch <hein_tibosch@yahoo.es>
Date: Thu Jun 25 13:01:45 2020 +0800
FreeRTOS+TCP : add memory statistics and dump packets, v3 (#83)
* FreeRTOS+TCP : add memory statistics and dump packets, v3
* Two changes as requested by Aniruddha
Co-authored-by: Hein Tibosch <hein@htibosch.net>
Co-authored-by: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
commit 072a173c9df31c75ff64bde440f3f316cedb9033
Author: S.Burch <8697966+wholl0p@users.noreply.github.com>
Date: Mon Jun 22 23:39:26 2020 +0200
Fixed Imports for Infineon XMC1100 Board (#88)
Co-authored-by: RichardBarry <3073890+RichardBarry@users.noreply.github.com>
commit 2df5eeef5763045c4c74ff0e2a4091b7d19bea89
Author: RichardBarry <3073890+RichardBarry@users.noreply.github.com>
Date: Mon Jun 8 14:22:46 2020 -0700
Feature/multiple direct to task notifications (#73)
* Add TaskNotifyArray.c with the single task tests updated to use the task notification array up to the point where the timer is created.
* Continue working on TaskNotifyArray.c to test the new task notification indexes. Next TaskNotifyArray.c will be refactored to break the tests up a bit.
* Refactor and update the comments in TaskNotifyArray.c - no functional changes.
* Change from the task notify "array" to task notification "indexed" nomenclature in the new task notification API functions that work on one particular task notification with the array of task notifications.
* Update the implementation of the taskNOTIFY_TAKE() and taskNOTIFY_WAIT() trace macros to take the array index of the task notification they are acting on.
Rename configNUMBER_OF_TASK_NOTIFICATIONS to configTASK_NOTIFICATION_ARRAY_ENTRIES.
Add FreeRTOS/Demo/Common/Minimal/TaskNotifyArray.c to the Visual Studio project - the file implements tests specific to the behaviour of the indexed task notification functions and should be used in addition to the tests already provided in FreeRTOS/Demo/Common/Minimal/TaskNotify.c.
commit b9e4ecfaf7286d8493d4a96a93fbb325534ad97b
Author: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
Date: Fri Jun 5 11:10:58 2020 -0700
Remove Empty and Un-referenced folder from Demo (#86)
commit f11bcc8acc57a23fb03603762e758c25b9d0efb7
Author: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
Date: Wed Jun 3 16:52:31 2020 -0700
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>
commit bb9f92f771e5f6ea2b9b09c7e89130a75e562eb7
Author: Yuhui Zheng <10982575+yuhui-zheng@users.noreply.github.com>
Date: Wed Jun 3 10:46:55 2020 -0700
Submodule FreeRTOS/Source 10bbbcf0b..6199b72fb (#82)
commit 6efc39f44be5b269168836e95aebbdb8ae77dce3
Author: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
Date: Tue Jun 2 15:09:25 2020 -0700
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>
commit 0eb5909fb02bac9dc074ff1bc2fe338d77f73764
Author: Yuhui Zheng <10982575+yuhui-zheng@users.noreply.github.com>
Date: Thu May 28 17:05:24 2020 -0700
readme.md for ATmega328PB Xplained Mini. (#76)
readme.md to get users jump started.
commit cb7edd2323a77f3dbea144c1f48f95582becc99e
Author: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
Date: Thu May 28 10:11:58 2020 -0700
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>
commit 6557291e5407ca7ec6beca53fced1aaa620c5c02
Author: alfred gedeon <alfred2g@hotmail.com>
Date: Wed May 27 14:44:33 2020 -0700
Test: Add Linux Networking support with demo application (#71)
* Test: Add Linux Networking support with demo application
* Test: revert files affected by uncrustify
* Test: revert files affected by uncrustify
Co-authored-by: Alfred Gedeon <gedeonag@amazon.com>
Co-authored-by: Yuhui Zheng <10982575+yuhui-zheng@users.noreply.github.com>
commit 8b079bc394e7b205d72210ce9e052404d782938f
Author: Yuhui Zheng <10982575+yuhui-zheng@users.noreply.github.com>
Date: Wed May 27 10:44:03 2020 -0700
ATmega328PB Xplained Mini -- demo project for ATmega port. (#70)
* Bootstrap a demo from START. No driver is added in this commit.
* Add FreeRTOS source code to project. Remove unnecessary folder nesting.
Heap_4 is used here.
* Copy over main.c, FreeRTOSConfig.h, and regtest.{c, h}.
This commit compiles, but will need some work on timer used.
* This port has 2KB RAM. We are using 1KB for heap.
Further decreasing minimum stack size, and also use stack overflow check 1 to save some stack space.
* Preserve EEPROM set to false.
* End of the line.
* Reduce register test stack size.
32 8-bit register + 10 bytes for stack frame cost. Round up to 50.
* Adding Queue test in Integer test.
- g3 to easy debugging.
- mainCHECK_PERIOD is set to 1000 ticks. Note that this port for now use WDT as tick timer, and period is set to 15ms.
- vErrorChecks, is of highest priority. So if this task gets run before other tasks, the very first check will fail.
* Avoid false alarm.
Since we don't know in which order the tasks are scheduled, clearing any error for the first entry of vErrorChecks.
Signed-off-by: Yuhui Zheng <10982575+yuhui-zheng@users.noreply.github.com>
* ParTest.c to init, set, toggle onboard user LED at PB5.
* Added a task to blink onboard user LED.
Need a magic number for stack size.
Signed-off-by: Yuhui Zheng <10982575+yuhui-zheng@users.noreply.github.com>
* Explicitly setting timing slicing to 0.
This is to avoid unecessary context switch when multiple tasks are of the same priority.
Signed-off-by: Yuhui Zheng <10982575+yuhui-zheng@users.noreply.github.com>
* Add taskYIELD() at the end of the loop in each register test task.
This is to give other tasks of the same priority a chance to run, regardless of scheduling algorithm.
Signed-off-by: Yuhui Zheng <10982575+yuhui-zheng@users.noreply.github.com>
* minor, update comment in main.c.
commit 95a3a02f95749fb7a600723076e291f9dee7426c
Author: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
Date: Fri May 22 16:26:59 2020 -0700
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
commit 5003d17feda25490e655c0f1c15d2b13e395c9f7
Author: Hein Tibosch <hein_tibosch@yahoo.es>
Date: Wed May 6 14:16:56 2020 -0400
FreeRTOS+TCP : renewing DHCP lease while network is down (#53)
Co-authored-by: Hein Tibosch <hein@htibosch.net>
Co-authored-by: Gary Wicker <14828980+gkwicker@users.noreply.github.com>
commit d95624c5d6ba95ec0474867d7165de2c28ed41b7
Author: AniruddhaKanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
Date: Tue May 5 09:57:18 2020 -0700
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>
commit 95ae7c65758a9473ea16ab08182f056f72331de2
Author: markrtuttle <tuttle@acm.org>
Date: Wed Apr 29 04:27:45 2020 +0000
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>
commit d421ccc89f6f6473dfdd566a00567b0e1fd4cfc3
Author: Yuhui Zheng <10982575+yuhui-zheng@users.noreply.github.com>
Date: Sat Apr 25 16:57:35 2020 -0700
Reword readme.md under ./Test. (#61)
commit 38412865985235b90dbd9da9708b68c4de5918f5
Author: Carl Lundin <53273776+lundinc2@users.noreply.github.com>
Date: Sat Apr 25 16:56:54 2020 -0700
Removed a:FR reference. (#60)
commit 4db195c916c7b13c82ab3a34a499fe606f266810
Author: AniruddhaKanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
Date: Tue Apr 21 15:40:08 2020 -0700
Adding FreeRTOS+TCP CBMC proofs to FreeRTOS/FreeRTOS (#56)
ParseDNSReply is to be added in the next PR.
commit 40a31b6d35a866a3a6c551d95bf08dae855da5bd
Author: AniruddhaKanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
Date: Mon Apr 13 13:58:33 2020 -0700
'uL' -> 'UL'
commit 5b3a289b69fc92089aa8bd4d1b44ab816f326f73
Author: AniruddhaKanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
Date: Mon Apr 13 13:50:53 2020 -0700
Changes after Gary's comments
commit edf68637dd22470a8d4f59fecc15b51379bcfeda
Author: AniruddhaKanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
Date: Fri Apr 10 16:26:03 2020 -0700
Update FreeRTOS_ARP.c
commit 35f3ac32a8899dd714a8a48952a4224fbcebc4aa
Author: AniruddhaKanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
Date: Fri Apr 10 15:56:18 2020 -0700
correct debug output
commit 5e12a70db4b6a8e68a434489683306f040252efa
Author: AniruddhaKanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
Date: Fri Apr 10 15:44:45 2020 -0700
Debugging flag check added
commit 4e8ac8de25ac4088b9c789b88a77cd39df4d9167
Author: AniruddhaKanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
Date: Thu Apr 9 16:57:19 2020 -0700
Comment style consistency and Yuhui's suggestions
commit e43f7cd086096ad60491fedba69927a1e1a82f20
Author: AniruddhaKanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
Date: Thu Apr 9 16:47:41 2020 -0700
Cleanup
commit ab3b51c7a0d880a6bf453ec63ae604e15050f310
Author: AniruddhaKanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
Date: Thu Apr 9 16:33:03 2020 -0700
Update after Gary's comments
commit 97f7009699ffb972c0745dfdb526d1fa4e0faf84
Author: AniruddhaKanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
Date: Wed Apr 8 14:30:15 2020 -0700
Update after richard's comments
commit a9fcafc074cec559dd67961ef44273df6180c2db
Author: AniruddhaKanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
Date: Wed Apr 8 14:07:39 2020 -0700
Corrected the formatting
- visual studio had messed up the formatting
commit c381861014a8043ce30723fc5a8cf5107719c8df
Author: AniruddhaKanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
Date: Wed Apr 8 13:01:12 2020 -0700
commit 2 after gary's comments
commit 75677a8d85fa802cca9058d6e23796d5043a0982
Author: AniruddhaKanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
Date: Wed Apr 8 12:51:10 2020 -0700
Commit after Gary's comments
commit 666c0da366030109db2c0c5e7253cebb2f899db7
Author: AniruddhaKanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
Date: Wed Apr 8 10:56:01 2020 -0700
Update after Yuhui's comments
- removed (void) from before memcpy, memset etc.
- corrected memcpy style as suggested by Yuhui
- Added logging for xNetworkInterfaceOutput. No need to configASSERT
commit 4a1148d15b6b8169d2412f8179f734683b179795
Author: AniruddhaKanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
Date: Wed Apr 1 16:05:36 2020 -0700
Coverity + MISRA compliance
Modified code to conform to the MISRA directives more closely.
commit fa74f7dccf6b1a356993c6a894f8e1173b8c8157
Author: Yuhui Zheng <10982575+yuhui-zheng@users.noreply.github.com>
Date: Thu Apr 2 20:26:10 2020 -0700
Removing writes to read-only PLIC interrupt pending registers.
Signed-off-by: Yuhui Zheng <10982575+yuhui-zheng@users.noreply.github.com>
commit 5b9777e11e16609648fb98d2f9a47553ab238950
Author: Yuhui Zheng <10982575+yuhui-zheng@users.noreply.github.com>
Date: Tue Mar 31 10:45:23 2020 -0700
A readme file to introduce what ./Test directory is about.
commit 211bb4cbd9ae6dfa95e8d8501f37d272bde5ab26
Author: Yuhui Zheng <10982575+yuhui-zheng@users.noreply.github.com>
Date: Tue Mar 24 15:14:24 2020 -0700
Ignore whitespace when working with patches.
commit 8156f64d1c45dd59ef12279f19a99f03e79e1f8a
Author: Yuhui Zheng <10982575+yuhui-zheng@users.noreply.github.com>
Date: Tue Feb 25 18:04:23 2020 -0800
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.
commit 9f316c246baafa15c542a5aea81a94f26e3d6507
Author: David Vrabel <david.vrabel@cambridgeconsultants.com>
Date: Mon Mar 16 11:21:46 2020 +0000
Demo/Posix_GCC: add demo application for Posix port using GCC
This is largely a copy of the Windows demo application with a few key
changes:
- heap_3 (use malloc()/free()) so tools like valgrind "just work".
- printf() wrapped in a mutex to prevent deadlocks on the internal
pthread mutexes inside printf().
SCons (https://scons.org/) is used as the build system.
This will be built as a 64-bit application, but note that the memory
allocation trace points only record the lower 32-bits of the address.
commit f78f919b3e2f0d707531a301a8ca07cd02bc4778
Author: Markus Rinne <markus.ka.rinne@gmail.com>
Date: Thu Mar 19 21:00:24 2020 +0200
Fix function comments
commit 1cd2d38d960a3576addb224582c88489bade5141
Author: David Chalco <david@chalco.io>
Date: Fri Mar 20 10:29:05 2020 -0700
unix separators for path and remove .exe suffix from risc compiler (works on windows/mac)
commit 938b19419eded12817737ab0644e94ed2ba7e95d
Author: Yuhui Zheng <10982575+yuhui-zheng@users.noreply.github.com>
Date: Thu Mar 19 18:23:09 2020 -0700
Removing ./FreeRTOS-Labs directory, since:
- IoT libraries are now in LTS branch.
- FAT/POSIX/Light-weight MQTT are in https://github.com/FreeRTOS/FreeRTOS-Labs.
commit 1a4abbc9e91b13fd6394464ade59d5e048320c7c
Author: Yuhui Zheng <10982575+yuhui-zheng@users.noreply.github.com>
Date: Tue Mar 17 19:30:02 2020 -0700
Maintenance -- clean up readme.txt and add url to GitHub. (#38)
* Removing readme.txt, as now we have README.md in place.
The only information missing from README.md is about FAQ.
* Adding FAQ information in README.md.
* Adding a .url to root to redict user to FreeRTOS github home page.
commit 47bb466aa19395b7785bcb830e2e4dd35f6bafc5
Author: Yuhui Zheng <10982575+yuhui-zheng@users.noreply.github.com>
Date: Tue Mar 17 13:07:44 2020 -0700
Update issue templates
Template maintenance.
- adding title prefix.
- adding examples to "additional context" section.
commit f506290041f56867765f8efa70ed2862125bdb7c
Author: Yuhui Zheng <10982575+yuhui-zheng@users.noreply.github.com>
Date: Tue Mar 17 10:15:07 2020 -0700
Create SECURITY.md
Apply the recommended SECURITY.md from AWS to our repo.
commit 8982a2f80a80a2a0a47cf82de07b52101bd9d606
Author: Yuhui Zheng <10982575+yuhui-zheng@users.noreply.github.com>
Date: Fri Mar 13 12:50:10 2020 -0700
Add ./lib directory to make sure Zynq project compiles.
commit ecf0f12aa14ad6fdafe1ef37257cbb4e03e2abd5
Author: AniruddhaKanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
Date: Wed Mar 11 10:19:48 2020 -0700
Sync up with Amazon-freertos repo (10th March 2020) (#34)
* Sync up with amazon-freertos
* Sync up with amazon-freertos
* Sync up with amazon-freertos
commit 0acffef047973e2e61c2201fd69cd9bbd317f674
Author: Yuhui Zheng <10982575+yuhui-zheng@users.noreply.github.com>
Date: Tue Mar 10 10:20:48 2020 -0700
GitHub PR template. (#29)
commit c40a6da2e4cb8042b56d1b174051cbbe9813781a
Author: AniruddhaKanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
Date: Mon Mar 9 11:18:48 2020 -0700
pass payload length when calling UDP callback (#30)
* pass payload length when calling UDP callback
commit 12d580e93d4d9074b9a867632f0681a511b4ad12
Author: Yuhui Zheng <10982575+yuhui-zheng@users.noreply.github.com>
Date: Fri Mar 6 18:16:51 2020 -0800
Update issue templates
Initial issue template. Created following https://help.github.com/en/github/building-a-strong-community/configuring-issue-templates-for-your-repository#configuring-the-template-chooser.
If change is needed, we could go another round.
commit 9debffb5e0e42ff716f58b2270b3af09652294af
Author: Yuhui Zheng <10982575+yuhui-zheng@users.noreply.github.com>
Date: Fri Mar 6 17:27:46 2020 -0800
Update README.md to remove dead link.
See the conversation https://github.com/FreeRTOS/FreeRTOS/commit/42c627b2b88cb3b487fea983d8b566a8bbae54fa#comments .
Linkage for both ```./FreeRTOS/Source``` and ```./FreeRTOS/Demo``` are removed, since it looks weird to only provide linkage to Demo.
commit 7e1a4bf563240501fc45167aee9d929c533939dd
Author: AniruddhaKanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
Date: Fri Mar 6 15:18:09 2020 -0800
Fix DHCP option Client-identifier (#28)
commit 42c627b2b88cb3b487fea983d8b566a8bbae54fa
Author: Yuhui.Zheng <10982575+yuhui-zheng@users.noreply.github.com>
Date: Fri Mar 6 09:15:11 2020 -0800
Update readme and revert relative URL. (#27)
* Reordering: bumping cloning instruction up.
* Rewording readme.md to be clear kernel code is a submodule of this repository.
* Reverting relative URL, since user cannot click through on GitHub page.
(With URL, user could still download the correct version of the code. Reverting simply due to UI issue.)
commit 5751ae9b60e248ebd0b4dd7c58df54364d2bb9d5
Author: Gaurav-Aggarwal-AWS <33462878+aggarg@users.noreply.github.com>
Date: Fri Mar 6 09:11:42 2020 -0800
Update CORTEX_MPU_M33F_NXP_LPC55S69_MCUXpresso project (#26)
This commit updates the project for LPC55S69 so that it works with the
latest version of MCUXpresso and SDK.
Signed-off-by: Gaurav Aggarwal <aggarg@amazon.com>
commit a9ffffe1f01f45f79e127c15727784984077932f
Author: Carl Lundin <53273776+lundinc2@users.noreply.github.com>
Date: Thu Mar 5 17:16:13 2020 -0800
Using Relative URL For Submoduling. (#24)
commit 52c82076b38fe73d1dc46c97abf74ae9b803696c
Author: Carl Lundin <53273776+lundinc2@users.noreply.github.com>
Date: Thu Mar 5 09:16:31 2020 -0800
use relative path to point to bundled toolchain instead (#25)
commit b877e4ec478de2c24d07ab46241070d7c66f375c
Author: lundinc2 <53273776+lundinc2@users.noreply.github.com>
Date: Tue Feb 25 13:18:38 2020 -0800
Moved vulnerability reporting and code of conduct to top of CONTRIBUTING.md (#20)
commit bef165d46799fb8faa58aaa224f80c16b6538e69
Author: Yuhui.Zheng <10982575+yuhui-zheng@users.noreply.github.com>
Date: Tue Feb 18 22:06:38 2020 -0800
Linking test source file from relative path. (#19)
commit 89e7bbe292afd3912d1f0b2402cc506878bad869
Author: Yuhui.Zheng <10982575+yuhui-zheng@users.noreply.github.com>
Date: Tue Feb 18 17:47:55 2020 -0800
A preliminary .gitignore file, to prevent us checking in files unnecessary. (#18)
https://github.com/github/gitignore.
commit c2a98127acb48c4562233230e66ca5c282688579
Author: RichardBarry <3073890+RichardBarry@users.noreply.github.com>
Date: Sun Feb 16 13:19:53 2020 -0800
Minor wording changes in the 'previous releases' section of the readme.me file. (#17)
commit 24c772d1439e5c291c0a29fce0a46996ca8afaa9
Author: Yuhui.Zheng <10982575+yuhui-zheng@users.noreply.github.com>
Date: Fri Feb 14 12:47:01 2020 -0800
Submodule kernel directory. (#16)
* Removing FreeRTOS/Source in readiness for submoduling.
* Submoduling kernel.
* README.md update due to submoduling.
When releasing, please follow these steps:
1. in local directory, clean directory and check "git status" shows "nothing to commit, working tree clean" for ALL subdirectories.
2. copy source code and instructions only to an empty folder. Git related should not be in this folder -- this covers .git, .gitignore, .github, .gitmodules, gitmessages, ......
3. zip the folder from step 2. (create both .zip and .7z)
4. attach .zip and .7z to the release. (e.g. attach these two in new release -- https://github.com/FreeRTOS/FreeRTOS/releases/new)
5. PLEASE download both, unzip, diff with your local git repo. (should not see any difference other than git related.) And, sanity check a couple of projects.
commit c3f8b91652392dc55e0d7067b90a40de5f5f0837
Author: Rashed Talukder <9218468+rashedtalukder@users.noreply.github.com>
Date: Thu Feb 13 17:47:14 2020 -0800
Update readme. Fixed typos and cli commands (#14)
commit 4723b825f2989213c1cdb2ebf4d6793e0292e363
Author: Julian Poidevin <julian-poidevin@users.noreply.github.com>
Date: Fri Feb 14 02:43:36 2020 +0100
Fixed wrong git clone SSH command (#13)
Replaced bad https URL with proper SSH URL
commit fc819b821715c42602819e58499846147a6394f5
Author: RichardBarry <3073890+RichardBarry@users.noreply.github.com>
Date: Thu Feb 13 17:42:22 2020 -0800
Correct the xTimerCreate() documentation which said NULL was returned if the timer period was passed into the function as 0, whereas that is not the case. (#15)
Add a note to the documentation for both the xTimerCreate() and xTimerCreateStatic() functions that the timer period must be greater than 0.
commit 1c711ab530b5f0dbd811d7d62e0a3763706ffff4
Author: Rashed Talukder <9218468+rashedtalukder@users.noreply.github.com>
Date: Wed Feb 12 23:00:18 2020 -0800
Updated contributions guidelines (#12)
commit 84fcc0d5317d96c6b086034093c8c1c83e050819
Author: Cobus van Eeden <35851496+cobusve@users.noreply.github.com>
Date: Wed Feb 12 15:05:06 2020 -0800
Updates to Markdown files and readme.txt (#11)
git-svn-id: http://svn.code.sf.net/p/freertos/code/trunk@2826 1d2547de-c912-0410-9cb9-b8ca96c0e9e2
Diffstat (limited to 'FreeRTOS/Test/CBMC/patches')
| -rw-r--r-- | FreeRTOS/Test/CBMC/patches/.gitattributes | 2 | ||||
| -rw-r--r-- | FreeRTOS/Test/CBMC/patches/.gitignore | 2 | ||||
| -rw-r--r-- | FreeRTOS/Test/CBMC/patches/0005-Remove-volatile-qualifier-from-tasks-variables.patch | 79 | ||||
| -rw-r--r-- | FreeRTOS/Test/CBMC/patches/0005-remove-static-from-prvCopyDataToQueue.patch | 22 | ||||
| -rw-r--r-- | FreeRTOS/Test/CBMC/patches/0006-Remove-static-from-prvNotifyQueueSetContainer.patch | 22 | ||||
| -rw-r--r-- | FreeRTOS/Test/CBMC/patches/0007-Remove-static-from-prvUnlockQueue.patch | 22 | ||||
| -rw-r--r-- | FreeRTOS/Test/CBMC/patches/FreeRTOSConfig.h | 237 | ||||
| -rw-r--r-- | FreeRTOS/Test/CBMC/patches/FreeRTOSIPConfig.h | 307 | ||||
| -rw-r--r-- | FreeRTOS/Test/CBMC/patches/Makefile | 24 | ||||
| -rw-r--r-- | FreeRTOS/Test/CBMC/patches/README.md | 6 | ||||
| -rwxr-xr-x | FreeRTOS/Test/CBMC/patches/__init__.py | 0 | ||||
| -rwxr-xr-x | FreeRTOS/Test/CBMC/patches/compute_patch.py | 241 | ||||
| -rwxr-xr-x | FreeRTOS/Test/CBMC/patches/patch.py | 36 | ||||
| -rwxr-xr-x | FreeRTOS/Test/CBMC/patches/patches_constants.py | 42 | ||||
| -rwxr-xr-x | FreeRTOS/Test/CBMC/patches/unpatch.py | 42 |
15 files changed, 1084 insertions, 0 deletions
diff --git a/FreeRTOS/Test/CBMC/patches/.gitattributes b/FreeRTOS/Test/CBMC/patches/.gitattributes new file mode 100644 index 000000000..a41fc7b45 --- /dev/null +++ b/FreeRTOS/Test/CBMC/patches/.gitattributes @@ -0,0 +1,2 @@ +# It seems git apply does not want crlf line endings on Windows +*.patch eol=lf diff --git a/FreeRTOS/Test/CBMC/patches/.gitignore b/FreeRTOS/Test/CBMC/patches/.gitignore new file mode 100644 index 000000000..4dec98ff0 --- /dev/null +++ b/FreeRTOS/Test/CBMC/patches/.gitignore @@ -0,0 +1,2 @@ +auto_patch* +patched diff --git a/FreeRTOS/Test/CBMC/patches/0005-Remove-volatile-qualifier-from-tasks-variables.patch b/FreeRTOS/Test/CBMC/patches/0005-Remove-volatile-qualifier-from-tasks-variables.patch new file mode 100644 index 000000000..29cde0e77 --- /dev/null +++ b/FreeRTOS/Test/CBMC/patches/0005-Remove-volatile-qualifier-from-tasks-variables.patch @@ -0,0 +1,79 @@ +This patch removes the volatile qualifier from some global variable +declarations in the tasks.c file. For task pool proofs, we are running +`goto-instrument` with the `--nondet-volatile` flag on, which causes reads from +volatile variable to be nondeterministic (i.e., any possible value can be +returned). This is actually the desired behavior for volatile variables +regarding verification purposes. However, this causes a lot of trouble when +such variables are pointers, since one of the possible values we can get when +dereferencing a volatile pointer is `NULL`. + +In the case of `uxPendedTicks`, a non-volatile copy of the variable is done +before the following loop in tasks.c (lines 2231-2255): + +{ + UBaseType_t uxPendedCounts = uxPendedTicks; /* Non-volatile copy. */ + + if( uxPendedCounts > ( UBaseType_t ) 0U ) + { + do + { + if( xTaskIncrementTick() != pdFALSE ) + { + xYieldPending = pdTRUE; + } + else + { + mtCOVERAGE_TEST_MARKER(); + } + --uxPendedCounts; + } while( uxPendedCounts > ( UBaseType_t ) 0U ); + + uxPendedTicks = 0; + } + else + { + mtCOVERAGE_TEST_MARKER(); + } +} + +Here, `uxPendedTicks` could return any value, making it impossible to unwind +(or unroll) this loop in CBMC. Therefore, we require `uxPendedTicks` to behave +as a regular variable so that the loop can be unwound. + +--- +diff --git a/FreeRTOS/Source/tasks.c b/FreeRTOS/Source/tasks.c +index ff657733..8b57d198 100644 +--- a/FreeRTOS/Source/tasks.c ++++ b/FreeRTOS/Source/tasks.c +@@ -331,7 +331,7 @@ typedef tskTCB TCB_t; + + /*lint -save -e956 A manual analysis and inspection has been used to determine + which static variables must be declared volatile. */ +-PRIVILEGED_DATA TCB_t * volatile pxCurrentTCB = NULL; ++PRIVILEGED_DATA TCB_t * pxCurrentTCB = NULL; + + /* Lists for ready and blocked tasks. -------------------- + xDelayedTaskList1 and xDelayedTaskList2 could be move to function scople but +@@ -340,8 +340,8 @@ the static qualifier. */ + PRIVILEGED_DATA static List_t pxReadyTasksLists[ configMAX_PRIORITIES ];/*< Prioritised ready tasks. */ + PRIVILEGED_DATA static List_t xDelayedTaskList1; /*< Delayed tasks. */ + PRIVILEGED_DATA static List_t xDelayedTaskList2; /*< Delayed tasks (two lists are used - one for delays that have overflowed the current tick count. */ +-PRIVILEGED_DATA static List_t * volatile pxDelayedTaskList; /*< Points to the delayed task list currently being used. */ +-PRIVILEGED_DATA static List_t * volatile pxOverflowDelayedTaskList; /*< Points to the delayed task list currently being used to hold tasks that have overflowed the current tick count. */ ++PRIVILEGED_DATA static List_t * pxDelayedTaskList; /*< Points to the delayed task list currently being used. */ ++PRIVILEGED_DATA static List_t * pxOverflowDelayedTaskList; /*< Points to the delayed task list currently being used to hold tasks that have overflowed the current tick count. */ + PRIVILEGED_DATA static List_t xPendingReadyList; /*< Tasks that have been readied while the scheduler was suspended. They will be moved to the ready list when the scheduler is resumed. */ + + #if( INCLUDE_vTaskDelete == 1 ) +@@ -368,10 +368,10 @@ PRIVILEGED_DATA static volatile UBaseType_t uxCurrentNumberOfTasks = ( UBaseTyp + + /* Other file private variables. --------------------------------*/ + PRIVILEGED_DATA static volatile UBaseType_t uxCurrentNumberOfTasks = ( UBaseType_t ) 0U; + PRIVILEGED_DATA static volatile TickType_t xTickCount = ( TickType_t ) configINITIAL_TICK_COUNT; + PRIVILEGED_DATA static volatile UBaseType_t uxTopReadyPriority = tskIDLE_PRIORITY; + PRIVILEGED_DATA static volatile BaseType_t xSchedulerRunning = pdFALSE; +-PRIVILEGED_DATA static volatile TickType_t xPendedTicks = ( TickType_t ) 0U; ++PRIVILEGED_DATA static TickType_t xPendedTicks = ( TickType_t ) 0U; + PRIVILEGED_DATA static volatile BaseType_t xYieldPending = pdFALSE; + PRIVILEGED_DATA static volatile BaseType_t xNumOfOverflows = ( BaseType_t ) 0; + PRIVILEGED_DATA static UBaseType_t uxTaskNumber = ( UBaseType_t ) 0U; diff --git a/FreeRTOS/Test/CBMC/patches/0005-remove-static-from-prvCopyDataToQueue.patch b/FreeRTOS/Test/CBMC/patches/0005-remove-static-from-prvCopyDataToQueue.patch new file mode 100644 index 000000000..5a79ae8cd --- /dev/null +++ b/FreeRTOS/Test/CBMC/patches/0005-remove-static-from-prvCopyDataToQueue.patch @@ -0,0 +1,22 @@ +diff --git a/FreeRTOS/Source/queue.c b/FreeRTOS/Source/queue.c +index df2b9c8c..c2265c26 100644 +--- a/FreeRTOS/Source/queue.c ++++ b/FreeRTOS/Source/queue.c +@@ -105,7 +105,7 @@ static BaseType_t prvIsQueueFull( const Queue_t *pxQueue ) PRIVILEGED_FUNCTION; + * Copies an item into the queue, either at the front of the queue or the + * back of the queue. + */ +-static BaseType_t prvCopyDataToQueue( Queue_t * const pxQueue, const void *pvItemToQueue, const BaseType_t xPosition ) PRIVILEGED_FUNCTION; ++BaseType_t prvCopyDataToQueue( Queue_t * const pxQueue, const void *pvItemToQueue, const BaseType_t xPosition ) PRIVILEGED_FUNCTION; + + /* + * Copies an item out of a queue. +@@ -1985,7 +1985,7 @@ Queue_t * const pxQueue = xQueue; + #endif /* configUSE_MUTEXES */ + /*-----------------------------------------------------------*/ + +-static BaseType_t prvCopyDataToQueue( Queue_t * const pxQueue, const void *pvItemToQueue, const BaseType_t xPosition ) ++BaseType_t prvCopyDataToQueue( Queue_t * const pxQueue, const void *pvItemToQueue, const BaseType_t xPosition ) + { + BaseType_t xReturn = pdFALSE; + UBaseType_t uxMessagesWaiting; diff --git a/FreeRTOS/Test/CBMC/patches/0006-Remove-static-from-prvNotifyQueueSetContainer.patch b/FreeRTOS/Test/CBMC/patches/0006-Remove-static-from-prvNotifyQueueSetContainer.patch new file mode 100644 index 000000000..9cbe7cf5f --- /dev/null +++ b/FreeRTOS/Test/CBMC/patches/0006-Remove-static-from-prvNotifyQueueSetContainer.patch @@ -0,0 +1,22 @@ +diff --git a/FreeRTOS/Source/queue.c b/FreeRTOS/Source/queue.c +index 17a6964e..24a40c29 100644 +--- a/FreeRTOS/Source/queue.c ++++ b/FreeRTOS/Source/queue.c +@@ -207,7 +207,7 @@ static void prvCopyDataFromQueue( Queue_t * const pxQueue, void * const pvBuffer + * Checks to see if a queue is a member of a queue set, and if so, notifies + * the queue set that the queue contains data. + */ +- static BaseType_t prvNotifyQueueSetContainer( const Queue_t * const pxQueue ) PRIVILEGED_FUNCTION; ++ BaseType_t prvNotifyQueueSetContainer( const Queue_t * const pxQueue ) PRIVILEGED_FUNCTION; + #endif + + /* +@@ -2887,7 +2887,7 @@ Queue_t * const pxQueue = xQueue; + + #if ( configUSE_QUEUE_SETS == 1 ) + +- static BaseType_t prvNotifyQueueSetContainer( const Queue_t * const pxQueue ) ++ BaseType_t prvNotifyQueueSetContainer( const Queue_t * const pxQueue ) + { + Queue_t *pxQueueSetContainer = pxQueue->pxQueueSetContainer; + BaseType_t xReturn = pdFALSE; diff --git a/FreeRTOS/Test/CBMC/patches/0007-Remove-static-from-prvUnlockQueue.patch b/FreeRTOS/Test/CBMC/patches/0007-Remove-static-from-prvUnlockQueue.patch new file mode 100644 index 000000000..eaae401c6 --- /dev/null +++ b/FreeRTOS/Test/CBMC/patches/0007-Remove-static-from-prvUnlockQueue.patch @@ -0,0 +1,22 @@ +diff --git a/FreeRTOS/Source/queue.c b/FreeRTOS/Source/queue.c +index 17a6964e..60ea3e69 100644 +--- a/FreeRTOS/Source/queue.c ++++ b/FreeRTOS/Source/queue.c +@@ -175,7 +175,7 @@ typedef xQUEUE Queue_t; + * to indicate that a task may require unblocking. When the queue in unlocked + * these lock counts are inspected, and the appropriate action taken. + */ +-static void prvUnlockQueue( Queue_t * const pxQueue ) PRIVILEGED_FUNCTION; ++void prvUnlockQueue( Queue_t * const pxQueue ) PRIVILEGED_FUNCTION; + + /* + * Uses a critical section to determine if there is any data in a queue. +@@ -2175,7 +2175,7 @@ static void prvCopyDataFromQueue( Queue_t * const pxQueue, void * const pvBuffer + } + /*-----------------------------------------------------------*/ + +-static void prvUnlockQueue( Queue_t * const pxQueue ) ++void prvUnlockQueue( Queue_t * const pxQueue ) + { + /* THIS FUNCTION MUST BE CALLED WITH THE SCHEDULER SUSPENDED. */ + diff --git a/FreeRTOS/Test/CBMC/patches/FreeRTOSConfig.h b/FreeRTOS/Test/CBMC/patches/FreeRTOSConfig.h new file mode 100644 index 000000000..28de2bd15 --- /dev/null +++ b/FreeRTOS/Test/CBMC/patches/FreeRTOSConfig.h @@ -0,0 +1,237 @@ +/* + * FreeRTOS Kernel V10.0.1 + * Copyright (C) 2017 Amazon.com, Inc. or its affiliates. All Rights Reserved. + * + * Permission is hereby granted, free of charge, to any person obtaining a copy of + * this software and associated documentation files (the "Software"), to deal in + * the Software without restriction, including without limitation the rights to + * use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of + * the Software, and to permit persons to whom the Software is furnished to do so, + * subject to the following conditions: + * + * The above copyright notice and this permission notice shall be included in all + * copies or substantial portions of the Software. + * + * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS + * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR + * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER + * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN + * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. + * + * http://aws.amazon.com/freertos + * http://www.FreeRTOS.org + */ + +#ifndef FREERTOS_CONFIG_H +#define FREERTOS_CONFIG_H + +/*----------------------------------------------------------- +* Application specific definitions. +* +* These definitions should be adjusted for your particular hardware and +* application requirements. +* +* THESE PARAMETERS ARE DESCRIBED WITHIN THE 'CONFIGURATION' SECTION OF THE +* FreeRTOS API DOCUMENTATION AVAILABLE ON THE FreeRTOS.org WEB SITE. +* http://www.freertos.org/a00110.html +* +* The bottom of this file contains some constants specific to running the UDP +* stack in this demo. Constants specific to FreeRTOS+TCP itself (rather than +* the demo) are contained in FreeRTOSIPConfig.h. +*----------------------------------------------------------*/ +#define configENABLE_BACKWARD_COMPATIBILITY 1 +#define configUSE_PREEMPTION 1 +#define configUSE_PORT_OPTIMISED_TASK_SELECTION 1 +#define configMAX_PRIORITIES ( 7 ) +#define configTICK_RATE_HZ ( 1000 ) /* In this non-real time simulated environment the tick frequency has to be at least a multiple of the Win32 tick frequency, and therefore very slow. */ +#define configMINIMAL_STACK_SIZE ( ( unsigned short ) 60 ) /* In this simulated case, the stack only has to hold one small structure as the real stack is part of the Win32 thread. */ +#define configTOTAL_HEAP_SIZE ( ( size_t ) ( 2048U * 1024U ) ) +#define configMAX_TASK_NAME_LEN ( 15 ) +#define configUSE_16_BIT_TICKS 0 +#define configIDLE_SHOULD_YIELD 1 +#define configUSE_CO_ROUTINES 0 +#ifndef configUSE_MUTEXES + #define configUSE_MUTEXES 1 +#endif +#ifndef configUSE_RECURSIVE_MUTEXES + #define configUSE_RECURSIVE_MUTEXES 1 +#endif +#define configQUEUE_REGISTRY_SIZE 0 +#define configUSE_APPLICATION_TASK_TAG 1 +#define configUSE_COUNTING_SEMAPHORES 1 +#define configUSE_ALTERNATIVE_API 0 +#define configNUM_THREAD_LOCAL_STORAGE_POINTERS 3 /* FreeRTOS+FAT requires 2 pointers if a CWD is supported. */ +#define configRECORD_STACK_HIGH_ADDRESS 1 + +/* Hook function related definitions. */ +#ifndef configUSE_TICK_HOOK + #define configUSE_TICK_HOOK 0 +#endif +#define configUSE_IDLE_HOOK 1 +#define configUSE_MALLOC_FAILED_HOOK 1 +#define configCHECK_FOR_STACK_OVERFLOW 0 /* Not applicable to the Win32 port. */ + +/* Software timer related definitions. */ +#define configUSE_TIMERS 1 +#define configTIMER_TASK_PRIORITY ( configMAX_PRIORITIES - 1 ) +#define configTIMER_QUEUE_LENGTH 5 +#define configTIMER_TASK_STACK_DEPTH ( configMINIMAL_STACK_SIZE * 2 ) + +/* Event group related definitions. */ +#define configUSE_EVENT_GROUPS 1 + +/* Co-routine definitions. */ +#define configUSE_CO_ROUTINES 0 +#define configMAX_CO_ROUTINE_PRIORITIES ( 2 ) + +/* Memory allocation strategy. */ +#ifndef configSUPPORT_DYNAMIC_ALLOCATION + #define configSUPPORT_DYNAMIC_ALLOCATION 1 +#endif +#ifndef configSUPPORT_STATIC_ALLOCATION + #define configSUPPORT_STATIC_ALLOCATION 1 +#endif + + +/* Set the following definitions to 1 to include the API function, or zero + * to exclude the API function. */ +#define INCLUDE_vTaskPrioritySet 1 +#define INCLUDE_uxTaskPriorityGet 1 +#define INCLUDE_vTaskDelete 1 +#define INCLUDE_vTaskCleanUpResources 0 +#ifndef INCLUDE_vTaskSuspend + #define INCLUDE_vTaskSuspend 1 +#endif +#define INCLUDE_vTaskDelayUntil 1 +#define INCLUDE_vTaskDelay 1 +#define INCLUDE_uxTaskGetStackHighWaterMark 1 +#ifndef INCLUDE_xTaskGetSchedulerState + #define INCLUDE_xTaskGetSchedulerState 1 +#endif +#define INCLUDE_xTimerGetTimerTaskHandle 0 +#define INCLUDE_xTaskGetIdleTaskHandle 0 +#define INCLUDE_xQueueGetMutexHolder 1 +#define INCLUDE_eTaskGetState 1 +#define INCLUDE_xEventGroupSetBitsFromISR 1 +#define INCLUDE_xTimerPendFunctionCall 1 +#define INCLUDE_xTaskGetCurrentTaskHandle 1 +#define INCLUDE_xTaskAbortDelay 1 + +/* This demo makes use of one or more example stats formatting functions. These + * format the raw data provided by the uxTaskGetSystemState() function in to human + * readable ASCII form. See the notes in the implementation of vTaskList() within + * FreeRTOS/Source/tasks.c for limitations. configUSE_STATS_FORMATTING_FUNCTIONS + * is set to 2 so the formatting functions are included without the stdio.h being + * included in tasks.c. That is because this project defines its own sprintf() + * functions. */ +#define configUSE_STATS_FORMATTING_FUNCTIONS 1 + +/* Assert call defined for debug builds. */ +extern void vAssertCalled( const char * pcFile, + uint32_t ulLine ); +#ifndef configASSERT +#define configASSERT( x ) if( ( x ) == 0 ) vAssertCalled( __FILE__, __LINE__ ) +#endif + +/* Remove logging in formal verification */ +#define configPRINTF( X ) + +/* Non-format version thread-safe print. */ +#define configPRINT_STRING( X ) + +/* Application specific definitions follow. **********************************/ + +/* If configINCLUDE_DEMO_DEBUG_STATS is set to one, then a few basic IP trace + * macros are defined to gather some UDP stack statistics that can then be viewed + * through the CLI interface. */ +#define configINCLUDE_DEMO_DEBUG_STATS 1 + +/* The size of the global output buffer that is available for use when there + * are multiple command interpreters running at once (for example, one on a UART + * and one on TCP/IP). This is done to prevent an output buffer being defined by + * each implementation - which would waste RAM. In this case, there is only one + * command interpreter running, and it has its own local output buffer, so the + * global buffer is just set to be one byte long as it is not used and should not + * take up unnecessary RAM. */ +#define configCOMMAND_INT_MAX_OUTPUT_SIZE 1 + +/* Only used when running in the FreeRTOS Windows simulator. Defines the + * priority of the task used to simulate Ethernet interrupts. */ +#define configMAC_ISR_SIMULATOR_PRIORITY ( configMAX_PRIORITIES - 1 ) + +/* This demo creates a virtual network connection by accessing the raw Ethernet + * or WiFi data to and from a real network connection. Many computers have more + * than one real network port, and configNETWORK_INTERFACE_TO_USE is used to tell + * the demo which real port should be used to create the virtual port. The ports + * available are displayed on the console when the application is executed. For + * example, on my development laptop setting configNETWORK_INTERFACE_TO_USE to 4 + * results in the wired network being used, while setting + * configNETWORK_INTERFACE_TO_USE to 2 results in the wireless network being + * used. */ +#define configNETWORK_INTERFACE_TO_USE ( 0L ) + +/* The address of an echo server that will be used by the two demo echo client + * tasks: + * http://www.freertos.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/TCP_Echo_Clients.html, + * http://www.freertos.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/UDP_Echo_Clients.html. */ +#define configECHO_SERVER_ADDR0 192 +#define configECHO_SERVER_ADDR1 168 +#define configECHO_SERVER_ADDR2 2 +#define configECHO_SERVER_ADDR3 6 +#define configTCP_ECHO_CLIENT_PORT 7 + +/* Default MAC address configuration. The demo creates a virtual network + * connection that uses this MAC address by accessing the raw Ethernet/WiFi data + * to and from a real network connection on the host PC. See the + * configNETWORK_INTERFACE_TO_USE definition above for information on how to + * configure the real network connection to use. */ +#define configMAC_ADDR0 0x00 +#define configMAC_ADDR1 0x11 +#define configMAC_ADDR2 0x22 +#define configMAC_ADDR3 0x33 +#define configMAC_ADDR4 0x44 +#define configMAC_ADDR5 0x21 + +/* Default IP address configuration. Used in ipconfigUSE_DHCP is set to 0, or + * ipconfigUSE_DHCP is set to 1 but a DNS server cannot be contacted. */ +#define configIP_ADDR0 192 +#define configIP_ADDR1 168 +#define configIP_ADDR2 0 +#define configIP_ADDR3 105 + +/* Default gateway IP address configuration. Used in ipconfigUSE_DHCP is set to + * 0, or ipconfigUSE_DHCP is set to 1 but a DNS server cannot be contacted. */ +#define configGATEWAY_ADDR0 192 +#define configGATEWAY_ADDR1 168 +#define configGATEWAY_ADDR2 0 +#define configGATEWAY_ADDR3 1 + +/* Default DNS server configuration. OpenDNS addresses are 208.67.222.222 and + * 208.67.220.220. Used in ipconfigUSE_DHCP is set to 0, or ipconfigUSE_DHCP is + * set to 1 but a DNS server cannot be contacted.*/ +#define configDNS_SERVER_ADDR0 208 +#define configDNS_SERVER_ADDR1 67 +#define configDNS_SERVER_ADDR2 222 +#define configDNS_SERVER_ADDR3 222 + +/* Default netmask configuration. Used in ipconfigUSE_DHCP is set to 0, or + * ipconfigUSE_DHCP is set to 1 but a DNS server cannot be contacted. */ +#define configNET_MASK0 255 +#define configNET_MASK1 255 +#define configNET_MASK2 255 +#define configNET_MASK3 0 + +/* The UDP port to which print messages are sent. */ +#define configPRINT_PORT ( 15000 ) + +#define configPROFILING ( 0 ) + +/* Pseudo random number generater used by some demo tasks. */ +extern uint32_t ulRand(); +#define configRAND32() ulRand() + +/* The platform that FreeRTOS is running on. */ +#define configPLATFORM_NAME "WinSim" + +#endif /* FREERTOS_CONFIG_H */ diff --git a/FreeRTOS/Test/CBMC/patches/FreeRTOSIPConfig.h b/FreeRTOS/Test/CBMC/patches/FreeRTOSIPConfig.h new file mode 100644 index 000000000..5e9180f8e --- /dev/null +++ b/FreeRTOS/Test/CBMC/patches/FreeRTOSIPConfig.h @@ -0,0 +1,307 @@ +/* +FreeRTOS Kernel V10.2.0 +Copyright (C) 2017 Amazon.com, Inc. or its affiliates. All Rights Reserved. + +Permission is hereby granted, free of charge, to any person obtaining a copy of +this software and associated documentation files (the "Software"), to deal in +the Software without restriction, including without limitation the rights to +use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of +the Software, and to permit persons to whom the Software is furnished to do so, +subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all +copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS +FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR +COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER +IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN +CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. + + http://aws.amazon.com/freertos + http://www.FreeRTOS.org +*/ + + +/***************************************************************************** +* +* See the following URL for configuration information. +* http://www.freertos.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/TCP_IP_Configuration.html +* +*****************************************************************************/ + +#ifndef FREERTOS_IP_CONFIG_H +#define FREERTOS_IP_CONFIG_H + +/* Set to 1 to print out debug messages. If ipconfigHAS_DEBUG_PRINTF is set to + * 1 then FreeRTOS_debug_printf should be defined to the function used to print + * out the debugging messages. */ +#define ipconfigHAS_DEBUG_PRINTF 0 +#if ( ipconfigHAS_DEBUG_PRINTF == 1 ) + #define FreeRTOS_debug_printf( X ) configPRINTF( X ) +#endif + +/* Set to 1 to print out non debugging messages, for example the output of the + * FreeRTOS_netstat() command, and ping replies. If ipconfigHAS_PRINTF is set to 1 + * then FreeRTOS_printf should be set to the function used to print out the + * messages. */ +#define FreeRTOS_printf( X ) + + +/* Define the byte order of the target MCU (the MCU FreeRTOS+TCP is executing + * on). Valid options are pdFREERTOS_BIG_ENDIAN and pdFREERTOS_LITTLE_ENDIAN. */ +#define ipconfigBYTE_ORDER pdFREERTOS_LITTLE_ENDIAN + +/* If the network card/driver includes checksum offloading (IP/TCP/UDP checksums) + * then set ipconfigDRIVER_INCLUDED_RX_IP_CHECKSUM to 1 to prevent the software + * stack repeating the checksum calculations. */ +#define ipconfigDRIVER_INCLUDED_RX_IP_CHECKSUM 1 + +/* Several API's will block until the result is known, or the action has been + * performed, for example FreeRTOS_send() and FreeRTOS_recv(). The timeouts can be + * set per socket, using setsockopt(). If not set, the times below will be + * used as defaults. */ +#define ipconfigSOCK_DEFAULT_RECEIVE_BLOCK_TIME ( 5000 ) +#define ipconfigSOCK_DEFAULT_SEND_BLOCK_TIME ( 5000 ) + +/* Include support for DNS caching. For TCP, having a small DNS cache is very + * useful. When a cache is present, ipconfigDNS_REQUEST_ATTEMPTS can be kept low + * and also DNS may use small timeouts. If a DNS reply comes in after the DNS + * socket has been destroyed, the result will be stored into the cache. The next + * call to FreeRTOS_gethostbyname() will return immediately, without even creating + * a socket. */ +#define ipconfigUSE_DNS_CACHE ( 1 ) +#define ipconfigDNS_REQUEST_ATTEMPTS ( 2 ) + +/* The IP stack executes it its own task (although any application task can make + * use of its services through the published sockets API). ipconfigUDP_TASK_PRIORITY + * sets the priority of the task that executes the IP stack. The priority is a + * standard FreeRTOS task priority so can take any value from 0 (the lowest + * priority) to (configMAX_PRIORITIES - 1) (the highest priority). + * configMAX_PRIORITIES is a standard FreeRTOS configuration parameter defined in + * FreeRTOSConfig.h, not FreeRTOSIPConfig.h. Consideration needs to be given as to + * the priority assigned to the task executing the IP stack relative to the + * priority assigned to tasks that use the IP stack. */ +#define ipconfigIP_TASK_PRIORITY ( configMAX_PRIORITIES - 2 ) + +/* The size, in words (not bytes), of the stack allocated to the FreeRTOS+TCP + * task. This setting is less important when the FreeRTOS Win32 simulator is used + * as the Win32 simulator only stores a fixed amount of information on the task + * stack. FreeRTOS includes optional stack overflow detection, see: + * http://www.freertos.org/Stacks-and-stack-overflow-checking.html. */ +#define ipconfigIP_TASK_STACK_SIZE_WORDS ( configMINIMAL_STACK_SIZE * 5 ) + +/* ipconfigRAND32() is called by the IP stack to generate random numbers for + * things such as a DHCP transaction number or initial sequence number. Random + * number generation is performed via this macro to allow applications to use their + * own random number generation method. For example, it might be possible to + * generate a random number by sampling noise on an analogue input. */ +extern uint32_t ulRand(); +#define ipconfigRAND32() ulRand() + +/* If ipconfigUSE_NETWORK_EVENT_HOOK is set to 1 then FreeRTOS+TCP will call the + * network event hook at the appropriate times. If ipconfigUSE_NETWORK_EVENT_HOOK + * is not set to 1 then the network event hook will never be called. See: + * http://www.FreeRTOS.org/FreeRTOS-Plus/FreeRTOS_Plus_UDP/API/vApplicationIPNetworkEventHook.shtml. + */ +#define ipconfigUSE_NETWORK_EVENT_HOOK 1 + +/* Sockets have a send block time attribute. If FreeRTOS_sendto() is called but + * a network buffer cannot be obtained then the calling task is held in the Blocked + * state (so other tasks can continue to executed) until either a network buffer + * becomes available or the send block time expires. If the send block time expires + * then the send operation is aborted. The maximum allowable send block time is + * capped to the value set by ipconfigMAX_SEND_BLOCK_TIME_TICKS. Capping the + * maximum allowable send block time prevents prevents a deadlock occurring when + * all the network buffers are in use and the tasks that process (and subsequently + * free) the network buffers are themselves blocked waiting for a network buffer. + * ipconfigMAX_SEND_BLOCK_TIME_TICKS is specified in RTOS ticks. A time in + * milliseconds can be converted to a time in ticks by dividing the time in + * milliseconds by portTICK_PERIOD_MS. */ +#define ipconfigUDP_MAX_SEND_BLOCK_TIME_TICKS ( 5000U / portTICK_PERIOD_MS ) + +/* If ipconfigUSE_DHCP is 1 then FreeRTOS+TCP will attempt to retrieve an IP + * address, netmask, DNS server address and gateway address from a DHCP server. If + * ipconfigUSE_DHCP is 0 then FreeRTOS+TCP will use a static IP address. The + * stack will revert to using the static IP address even when ipconfigUSE_DHCP is + * set to 1 if a valid configuration cannot be obtained from a DHCP server for any + * reason. The static configuration used is that passed into the stack by the + * FreeRTOS_IPInit() function call. */ +#define ipconfigUSE_DHCP 1 +#define ipconfigDHCP_REGISTER_HOSTNAME 1 +#define ipconfigDHCP_USES_UNICAST 1 + +/* If ipconfigDHCP_USES_USER_HOOK is set to 1 then the application writer must + * provide an implementation of the DHCP callback function, + * xApplicationDHCPUserHook(). */ +#define ipconfigUSE_DHCP_HOOK 0 + +/* When ipconfigUSE_DHCP is set to 1, DHCP requests will be sent out at + * increasing time intervals until either a reply is received from a DHCP server + * and accepted, or the interval between transmissions reaches + * ipconfigMAXIMUM_DISCOVER_TX_PERIOD. The IP stack will revert to using the + * static IP address passed as a parameter to FreeRTOS_IPInit() if the + * re-transmission time interval reaches ipconfigMAXIMUM_DISCOVER_TX_PERIOD without + * a DHCP reply being received. */ +#define ipconfigMAXIMUM_DISCOVER_TX_PERIOD \ + ( 120000U / portTICK_PERIOD_MS ) + +/* The ARP cache is a table that maps IP addresses to MAC addresses. The IP + * stack can only send a UDP message to a remove IP address if it knowns the MAC + * address associated with the IP address, or the MAC address of the router used to + * contact the remote IP address. When a UDP message is received from a remote IP + * address the MAC address and IP address are added to the ARP cache. When a UDP + * message is sent to a remote IP address that does not already appear in the ARP + * cache then the UDP message is replaced by a ARP message that solicits the + * required MAC address information. ipconfigARP_CACHE_ENTRIES defines the maximum + * number of entries that can exist in the ARP table at any one time. */ +#define ipconfigARP_CACHE_ENTRIES 6 + +/* ARP requests that do not result in an ARP response will be re-transmitted a + * maximum of ipconfigMAX_ARP_RETRANSMISSIONS times before the ARP request is + * aborted. */ +#define ipconfigMAX_ARP_RETRANSMISSIONS ( 5 ) + +/* ipconfigMAX_ARP_AGE defines the maximum time between an entry in the ARP + * table being created or refreshed and the entry being removed because it is stale. + * New ARP requests are sent for ARP cache entries that are nearing their maximum + * age. ipconfigMAX_ARP_AGE is specified in tens of seconds, so a value of 150 is + * equal to 1500 seconds (or 25 minutes). */ +#define ipconfigMAX_ARP_AGE 150 + +/* Implementing FreeRTOS_inet_addr() necessitates the use of string handling + * routines, which are relatively large. To save code space the full + * FreeRTOS_inet_addr() implementation is made optional, and a smaller and faster + * alternative called FreeRTOS_inet_addr_quick() is provided. FreeRTOS_inet_addr() + * takes an IP in decimal dot format (for example, "192.168.0.1") as its parameter. + * FreeRTOS_inet_addr_quick() takes an IP address as four separate numerical octets + * (for example, 192, 168, 0, 1) as its parameters. If + * ipconfigINCLUDE_FULL_INET_ADDR is set to 1 then both FreeRTOS_inet_addr() and + * FreeRTOS_indet_addr_quick() are available. If ipconfigINCLUDE_FULL_INET_ADDR is + * not set to 1 then only FreeRTOS_indet_addr_quick() is available. */ +#define ipconfigINCLUDE_FULL_INET_ADDR 1 + +/* ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS defines the total number of network buffer that + * are available to the IP stack. The total number of network buffers is limited + * to ensure the total amount of RAM that can be consumed by the IP stack is capped + * to a pre-determinable value. */ +#ifndef ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS + #define ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS 60 +#endif + +/* A FreeRTOS queue is used to send events from application tasks to the IP + * stack. ipconfigEVENT_QUEUE_LENGTH sets the maximum number of events that can + * be queued for processing at any one time. The event queue must be a minimum of + * 5 greater than the total number of network buffers. */ +#define ipconfigEVENT_QUEUE_LENGTH \ + ( ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS + 5 ) + +/* The address of a socket is the combination of its IP address and its port + * number. FreeRTOS_bind() is used to manually allocate a port number to a socket + * (to 'bind' the socket to a port), but manual binding is not normally necessary + * for client sockets (those sockets that initiate outgoing connections rather than + * wait for incoming connections on a known port number). If + * ipconfigALLOW_SOCKET_SEND_WITHOUT_BIND is set to 1 then calling + * FreeRTOS_sendto() on a socket that has not yet been bound will result in the IP + * stack automatically binding the socket to a port number from the range + * socketAUTO_PORT_ALLOCATION_START_NUMBER to 0xffff. If + * ipconfigALLOW_SOCKET_SEND_WITHOUT_BIND is set to 0 then calling FreeRTOS_sendto() + * on a socket that has not yet been bound will result in the send operation being + * aborted. */ +#define ipconfigALLOW_SOCKET_SEND_WITHOUT_BIND 1 + +/* Defines the Time To Live (TTL) values used in outgoing UDP packets. */ +#define ipconfigUDP_TIME_TO_LIVE 128 +/* Also defined in FreeRTOSIPConfigDefaults.h. */ +#define ipconfigTCP_TIME_TO_LIVE 128 + +/* USE_TCP: Use TCP and all its features. */ +#define ipconfigUSE_TCP ( 1 ) + +/* USE_WIN: Let TCP use windowing mechanism. */ +#define ipconfigUSE_TCP_WIN ( 1 ) + +/* The MTU is the maximum number of bytes the payload of a network frame can + * contain. For normal Ethernet V2 frames the maximum MTU is 1500. Setting a + * lower value can save RAM, depending on the buffer management scheme used. If + * ipconfigCAN_FRAGMENT_OUTGOING_PACKETS is 1 then (ipconfigNETWORK_MTU - 28) must + * be divisible by 8. */ +#define ipconfigNETWORK_MTU 1200U + +/* Set ipconfigUSE_DNS to 1 to include a basic DNS client/resolver. DNS is used + * through the FreeRTOS_gethostbyname() API function. */ +#define ipconfigUSE_DNS 1 + +/* If ipconfigREPLY_TO_INCOMING_PINGS is set to 1 then the IP stack will + * generate replies to incoming ICMP echo (ping) requests. */ +#define ipconfigREPLY_TO_INCOMING_PINGS 1 + +/* If ipconfigSUPPORT_OUTGOING_PINGS is set to 1 then the + * FreeRTOS_SendPingRequest() API function is available. */ +#define ipconfigSUPPORT_OUTGOING_PINGS 0 + +/* If ipconfigSUPPORT_SELECT_FUNCTION is set to 1 then the FreeRTOS_select() + * (and associated) API function is available. */ +#define ipconfigSUPPORT_SELECT_FUNCTION 0 + +/* If ipconfigFILTER_OUT_NON_ETHERNET_II_FRAMES is set to 1 then Ethernet frames + * that are not in Ethernet II format will be dropped. This option is included for + * potential future IP stack developments. */ +#define ipconfigFILTER_OUT_NON_ETHERNET_II_FRAMES 1 + +/* If ipconfigETHERNET_DRIVER_FILTERS_FRAME_TYPES is set to 1 then it is the + * responsibility of the Ethernet interface to filter out packets that are of no + * interest. If the Ethernet interface does not implement this functionality, then + * set ipconfigETHERNET_DRIVER_FILTERS_FRAME_TYPES to 0 to have the IP stack + * perform the filtering instead (it is much less efficient for the stack to do it + * because the packet will already have been passed into the stack). If the + * Ethernet driver does all the necessary filtering in hardware then software + * filtering can be removed by using a value other than 1 or 0. */ +#define ipconfigETHERNET_DRIVER_FILTERS_FRAME_TYPES 1 + +/* The windows simulator cannot really simulate MAC interrupts, and needs to + * block occasionally to allow other tasks to run. */ +#define configWINDOWS_MAC_INTERRUPT_SIMULATOR_DELAY ( 20 / portTICK_PERIOD_MS ) + +/* Advanced only: in order to access 32-bit fields in the IP packets with + * 32-bit memory instructions, all packets will be stored 32-bit-aligned, + * plus 16-bits. This has to do with the contents of the IP-packets: all + * 32-bit fields are 32-bit-aligned, plus 16-bit. */ +#define ipconfigPACKET_FILLER_SIZE 2U + +/* Define the size of the pool of TCP window descriptors. On the average, each + * TCP socket will use up to 2 x 6 descriptors, meaning that it can have 2 x 6 + * outstanding packets (for Rx and Tx). When using up to 10 TP sockets + * simultaneously, one could define TCP_WIN_SEG_COUNT as 120. */ +#define ipconfigTCP_WIN_SEG_COUNT 240 + +/* Each TCP socket has a circular buffers for Rx and Tx, which have a fixed + * maximum size. Define the size of Rx buffer for TCP sockets. */ +#define ipconfigTCP_RX_BUFFER_LENGTH ( 10000 ) + +/* Define the size of Tx buffer for TCP sockets. */ +#define ipconfigTCP_TX_BUFFER_LENGTH ( 10000 ) + +/* When using call-back handlers, the driver may check if the handler points to + * real program memory (RAM or flash) or just has a random non-zero value. */ +#define ipconfigIS_VALID_PROG_ADDRESS( x ) ( ( x ) != NULL ) + +/* Include support for TCP keep-alive messages. */ +#define ipconfigTCP_KEEP_ALIVE ( 1 ) +#define ipconfigTCP_KEEP_ALIVE_INTERVAL ( 20 ) /* Seconds. */ + +/* The socket semaphore is used to unblock the MQTT task. */ +#define ipconfigSOCKET_HAS_USER_SEMAPHORE ( 0 ) + +#define ipconfigSOCKET_HAS_USER_WAKE_CALLBACK ( 1 ) +#define ipconfigUSE_CALLBACKS ( 0 ) + + +#define portINLINE __inline + +void vApplicationMQTTGetKeys( const char ** ppcRootCA, + const char ** ppcClientCert, + const char ** ppcClientPrivateKey ); + +#endif /* FREERTOS_IP_CONFIG_H */ diff --git a/FreeRTOS/Test/CBMC/patches/Makefile b/FreeRTOS/Test/CBMC/patches/Makefile new file mode 100644 index 000000000..27888e63b --- /dev/null +++ b/FreeRTOS/Test/CBMC/patches/Makefile @@ -0,0 +1,24 @@ +BRANCH=freertos + +PATCHED=patched + +default: + git format-patch $(BRANCH)..$(BRANCH)-cbmc-patches + +patch: + if [ ! -f $(PATCHED) ]; then \ + for p in *.patch; do \ + (cd ../../..; patch -p1 < CBMC/patches/$${p}) \ + done; \ + cat > $(PATCHED) < /dev/null; \ + fi + +unpatch: + git checkout ../../../lib + $(RM) $(PATCHED) + +#patching file lib/FreeRTOS-Plus-TCP/include/FreeRTOS_IP_Private.h +#patching file lib/include/private/list.h +#patching file lib/FreeRTOS-Plus-TCP/source/FreeRTOS_DHCP.c +#patching file lib/FreeRTOS-Plus-TCP/source/FreeRTOS_DNS.c +#patching file lib/FreeRTOS-Plus-TCP/source/FreeRTOS_TCP_WIN.c diff --git a/FreeRTOS/Test/CBMC/patches/README.md b/FreeRTOS/Test/CBMC/patches/README.md new file mode 100644 index 000000000..ec0e5d424 --- /dev/null +++ b/FreeRTOS/Test/CBMC/patches/README.md @@ -0,0 +1,6 @@ +This directory includes patches to FreeRTOS required to run the CBMC proofs. + +The patches fall into three classes: +* First is a refactoring of prvCheckOptions +* Second is the removal of static attributes from some functions +* Third is two patches dealing with shortcomings of CBMC that should be removed soon.
\ No newline at end of file diff --git a/FreeRTOS/Test/CBMC/patches/__init__.py b/FreeRTOS/Test/CBMC/patches/__init__.py new file mode 100755 index 000000000..e69de29bb --- /dev/null +++ b/FreeRTOS/Test/CBMC/patches/__init__.py diff --git a/FreeRTOS/Test/CBMC/patches/compute_patch.py b/FreeRTOS/Test/CBMC/patches/compute_patch.py new file mode 100755 index 000000000..3e854177c --- /dev/null +++ b/FreeRTOS/Test/CBMC/patches/compute_patch.py @@ -0,0 +1,241 @@ +#!/usr/bin/env python3 +# +# Generation of patches for CBMC proofs. +# +# Copyright (C) 2019 Amazon.com, Inc. or its affiliates. All Rights Reserved. +# +# Permission is hereby granted, free of charge, to any person obtaining a copy +# of this software and associated documentation files (the "Software"), to deal +# in the Software without restriction, including without limitation the rights +# to use, copy, modify, merge, publish, distribute, sublicense, and/or sell +# copies of the Software, and to permit persons to whom the Software is +# furnished to do so, subject to the following conditions: +# +# The above copyright notice and this permission notice shall be included in all +# copies or substantial portions of the Software. +# +# THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +# IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +# FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +# AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +# LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, +# OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE +# SOFTWARE. + + +import json +import os +import re +import subprocess +import textwrap +import unittest + +from patches_constants import PATCHES_DIR +from patches_constants import HEADERS + + +DEFINE_REGEX_MAKEFILE = re.compile(r"(?:['\"])?([\w]+)") +DEFINE_REGEX_HEADER = re.compile(r"\s*#\s*define\s*([\w]+)") + +class DirtyGitError(Exception): + pass + +class PatchCreationError(Exception): + pass + +def prolog(): + return textwrap.dedent("""\ + This script generates patch files for the header files used + in the cbmc proof. These patches permit setting values of preprocessor + macros as part of the proof configuration. + """) + + +def find_all_defines(): + """Collects all define values in Makefile.json. + + Some of the Makefiles use # in the json to make comments. + As this is non standard json, we need to remove the comment + lines before parsing. Then we extract all defines from the file. + """ + defines = set() + + proof_dir = os.path.abspath(os.path.join(PATCHES_DIR, "..", "proofs")) + + for fldr, _, fyles in os.walk(proof_dir): + if "Makefile.json" in fyles: + file = os.path.join(fldr, "Makefile.json") + key = "DEF" + elif "MakefileCommon.json" in fyles: + file = os.path.join(fldr, "MakefileCommon.json") + key = "DEF " + else: + continue + with open(file, "r") as source: + content = "".join([line for line in source + if line and not line.strip().startswith("#")]) + makefile = json.loads(content) + if key in makefile.keys(): + """This regex parses the define declaration in Makefile.json + 'macro(x)=false' is an example for a declaration. + 'macro' is expected to be matched. + """ + for define in makefile[key]: + matched = DEFINE_REGEX_MAKEFILE.match(define) + if matched: + defines.add(matched.group(1)) + return defines + +def manipulate_headerfile(defines, header_file): + """Wraps all defines used in an ifndef.""" + + # This regex matches the actual define in the header file. + modified_content = "" + with open(header_file, "r") as source: + last = "" + for line in source: + match = DEFINE_REGEX_HEADER.match(line) + if (match and + match.group(1) in defines and + not last.lstrip().startswith("#ifndef")): + full_def = line + # this loop deals with multiline definitions + while line.rstrip().endswith("\\"): + line = next(source) + full_def += line + # indentation for multiline definitions can be improved + modified_content += textwrap.dedent("""\ + #ifndef {target} + {original}\ + #endif + """.format(target=match.group(1), original=full_def)) + else: + modified_content += line + last = line + with open(header_file, "w") as output: + output.write(modified_content) + + +def header_dirty(header_files): + """Check that the header_file is not previously modified.""" + + # Git does not update the modified file list returned by diff-files on + # apply -R (at least not on MacOS). + # Running git status updates git's internal state. + status = subprocess.run(["git", "status"], stdout=subprocess.DEVNULL, + stderr=subprocess.PIPE, universal_newlines=True) + + diff_state = subprocess.run(["git", "diff-files"], stdout=subprocess.PIPE, + stderr=subprocess.PIPE, universal_newlines=True) + + if status.returncode: + raise DirtyGitError(textwrap.dedent("""\ + Could not run git status. Exited: {} + stderr: {} + """.format(status.returncode, status.stderr))) + + if diff_state.returncode: + raise DirtyGitError(textwrap.dedent("""\ + Could not run git diff-files. Exited: {} + stderr: {} + """.format(diff_state.returncode, diff_state.stderr))) + + for header_file in header_files: + if os.path.basename(header_file) + "\n" in diff_state.stdout: + return True + return False + + +def create_patch(defines, header_file): + """Computes a patch enclosing defines used in CBMC proofs with #ifndef.""" + manipulate_headerfile(defines, header_file) + patch = subprocess.run(["git", "diff", header_file], + stdout=subprocess.PIPE, + stderr=subprocess.PIPE, universal_newlines=True) + cleaned = subprocess.run(["git", "checkout", "--", header_file], + stdout=subprocess.DEVNULL, + stderr=subprocess.PIPE, universal_newlines=True) + + if patch.returncode: + raise PatchCreationError(textwrap.dedent("""\ + git diff exited with error code: {} + stderr: {} + """.format(patch.returncode, patch.stderr))) + + if cleaned.returncode: + raise DirtyGitError(textwrap.dedent("""\ + git checkout for cleaning files failed with error code: {} + on file {} + stderr: {} + """.format(cleaned.returncode, header_file, cleaned.stderr))) + + header_path_part = header_file.replace(os.sep, "_") + path_name = "auto_patch_" + header_path_part + ".patch" + path_name = os.path.join(PATCHES_DIR, path_name) + if patch.stdout: + with open(path_name, "w") as patch_file: + patch_file.write(patch.stdout) + + +def create_patches(headers): + defines = find_all_defines() + + if not header_dirty(headers): + for header in headers: + create_patch(defines, header) + else: + raise DirtyGitError(textwrap.dedent("""\ + It seems like one of the header files is in dirty state. + This script cannot patch files in dirty state. + """)) + +# Invoke 'python3 -m unittest compute_patch.py" for running tests. +class TestDefineRegexes(unittest.TestCase): + def test_makefile_regex(self): + input1 = "ipconfigETHERNET_MINIMUM_PACKET_BYTES={MINIMUM_PACKET_BYTES}" + input2 = "ipconfigETHERNET_MINIMUM_PACKET_BYTES=50" + input3 = "'configASSERT(X)=__CPROVER_assert(x, \"must hold\")'" + input4 = '"configASSERT (X)=__CPROVER_assert(x, "must hold")"' + input5 = "configASSERT(X)=__CPROVER_assert(x,\"must hold\")" + + match1 = DEFINE_REGEX_MAKEFILE.match(input1) + match2 = DEFINE_REGEX_MAKEFILE.match(input2) + match3 = DEFINE_REGEX_MAKEFILE.match(input3) + match4 = DEFINE_REGEX_MAKEFILE.match(input4) + match5 = DEFINE_REGEX_MAKEFILE.match(input5) + + self.assertIsNotNone(match1) + self.assertIsNotNone(match2) + self.assertIsNotNone(match3) + self.assertIsNotNone(match4) + self.assertIsNotNone(match5) + + self.assertEqual(match1.group(1), + "ipconfigETHERNET_MINIMUM_PACKET_BYTES") + self.assertEqual(match2.group(1), + "ipconfigETHERNET_MINIMUM_PACKET_BYTES") + self.assertEqual(match3.group(1), "configASSERT") + self.assertEqual(match4.group(1), "configASSERT") + self.assertEqual(match5.group(1), "configASSERT") + + + def test_header_regex(self): + input1 = ("#define configASSERT( x ) if( ( x ) == 0 )" + + "vAssertCalled( __FILE__, __LINE__ )") + input2 = "#define ipconfigMAX_ARP_RETRANSMISSIONS ( 5 )" + input3 = "#define ipconfigINCLUDE_FULL_INET_ADDR 1" + + match1 = DEFINE_REGEX_HEADER.match(input1) + match2 = DEFINE_REGEX_HEADER.match(input2) + match3 = DEFINE_REGEX_HEADER.match(input3) + + self.assertIsNotNone(match1) + self.assertIsNotNone(match2) + self.assertIsNotNone(match3) + + self.assertEqual(match1.group(1), "configASSERT") + self.assertEqual(match2.group(1), "ipconfigMAX_ARP_RETRANSMISSIONS") + self.assertEqual(match3.group(1), "ipconfigINCLUDE_FULL_INET_ADDR") + +if __name__ == '__main__': + create_patches(HEADERS) diff --git a/FreeRTOS/Test/CBMC/patches/patch.py b/FreeRTOS/Test/CBMC/patches/patch.py new file mode 100755 index 000000000..c2c0883a3 --- /dev/null +++ b/FreeRTOS/Test/CBMC/patches/patch.py @@ -0,0 +1,36 @@ +#!/usr/bin/env python3 + +import logging +import os +import subprocess +import sys +from glob import glob + +from patches_constants import PATCHES_DIR + +def patch(): + if os.path.isfile("patched"): + sys.exit() + + applied_patches = [] + failed_patches = [] + for tmpfile in glob(os.path.join(PATCHES_DIR, "*.patch")): + print("patch", tmpfile) + result = subprocess.run(["git", "apply", "--ignore-space-change", "--ignore-whitespace", tmpfile], + cwd=os.path.join("..", "..", "..", "..")) + if result.returncode: + failed_patches.append(tmpfile) + logging.error("patching failed: %s", tmpfile) + else: + applied_patches.append(tmpfile) + + with open(os.path.join(PATCHES_DIR, "patched"), "w") as outp: + print("Success:", file=outp) + print("\n".join(map(lambda x: "\t" + x, applied_patches)), file=outp) + + print("Failure:", file=outp) + print("\n".join(map(lambda x: "\t" + x, failed_patches)), file=outp) + + +if __name__ == "__main__": + patch() diff --git a/FreeRTOS/Test/CBMC/patches/patches_constants.py b/FreeRTOS/Test/CBMC/patches/patches_constants.py new file mode 100755 index 000000000..71f0b0537 --- /dev/null +++ b/FreeRTOS/Test/CBMC/patches/patches_constants.py @@ -0,0 +1,42 @@ +#!/usr/bin/env python3 +# +# Constants for the generation of patches for CBMC proofs. +# +# Copyright (C) 2019 Amazon.com, Inc. or its affiliates. All Rights Reserved. +# +# Permission is hereby granted, free of charge, to any person obtaining a copy +# of this software and associated documentation files (the "Software"), to deal +# in the Software without restriction, including without limitation the rights +# to use, copy, modify, merge, publish, distribute, sublicense, and/or sell +# copies of the Software, and to permit persons to whom the Software is +# furnished to do so, subject to the following conditions: +# +# The above copyright notice and this permission notice shall be included in all +# copies or substantial portions of the Software. +# +# THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +# IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +# FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +# AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +# LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, +# OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE +# SOFTWARE. + +import os + +PATCHES_DIR = os.path.dirname(os.path.abspath(__file__)) + + +shared_prefix = [ + "." +] +shared_prefix_port = [ + "..", "..", "..", "Source", "portable", "MSVC-MingW" +] + +absolute_prefix = os.path.abspath(os.path.join(PATCHES_DIR, *shared_prefix)) +absolute_prefix_port = os.path.abspath(os.path.join(PATCHES_DIR, *shared_prefix_port)) + +HEADERS = [os.path.join(absolute_prefix, "FreeRTOSConfig.h"), + os.path.join(absolute_prefix, "FreeRTOSIPConfig.h"), + os.path.join(absolute_prefix_port, "portmacro.h")] diff --git a/FreeRTOS/Test/CBMC/patches/unpatch.py b/FreeRTOS/Test/CBMC/patches/unpatch.py new file mode 100755 index 000000000..2162971fd --- /dev/null +++ b/FreeRTOS/Test/CBMC/patches/unpatch.py @@ -0,0 +1,42 @@ +#!/usr/bin/env python3 +# +# unpatching changes for the CBMC proofs. +# +# Copyright (C) 2019 Amazon.com, Inc. or its affiliates. All Rights Reserved. +# +# Permission is hereby granted, free of charge, to any person obtaining a copy +# of this software and associated documentation files (the "Software"), to deal +# in the Software without restriction, including without limitation the rights +# to use, copy, modify, merge, publish, distribute, sublicense, and/or sell +# copies of the Software, and to permit persons to whom the Software is +# furnished to do so, subject to the following conditions: +# +# The above copyright notice and this permission notice shall be included in all +# copies or substantial portions of the Software. +# +# THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +# IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +# FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +# AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +# LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, +# OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE +# SOFTWARE. + +import subprocess +import os +import sys +from glob import glob + +from patches_constants import PATCHES_DIR + +try: + os.remove(os.path.join(PATCHES_DIR, "patched")) +except FileNotFoundError: + print("Nothing to do here.") + sys.exit(0) +for tmpfile in glob(os.path.join(PATCHES_DIR, "*.patch")): + print("unpatch", tmpfile) + result = subprocess.run(["git", "apply", "-R", "--ignore-space-change", "--ignore-whitespace", tmpfile], + cwd=os.path.join("..", "..", "..", "..")) + if result.returncode: + print("Unpatching failed: {}".format(tmpfile)) |