FreeRTOS-Kernel/FreeRTOS/Test/CBMC/patches
Cobus van Eeden c6f4284b76
Update kernel submodule pointer to version 47338393f (#456)
* Update kernel submodule pointer to version 47338393f

* Fix patches.

Co-authored-by: Carl Lundin <lundinc@amazon.com>
2020-12-08 15:44:14 -08:00
..
.gitattributes Copying CBMC proofs from aws/amazon-freertos repo ./tools/cbmc to this repo ./FreeRTOS/Test/CBMC as is. 2020-03-31 14:21:53 -07:00
.gitignore Copying CBMC proofs from aws/amazon-freertos repo ./tools/cbmc to this repo ./FreeRTOS/Test/CBMC as is. 2020-03-31 14:21:53 -07:00
0005-remove-static-from-prvCopyDataToQueue.patch Updating queue.c patches for CBMC proofs (#216) 2020-08-26 13:07:15 -07:00
0005-Remove-volatile-qualifier-from-tasks-variables.patch Move forward Kernel submodule pointer (#218) 2020-08-26 23:50:09 -07:00
0006-Remove-static-from-prvNotifyQueueSetContainer.patch Move forward Kernel submodule pointer (#218) 2020-08-26 23:50:09 -07:00
0007-Remove-static-from-prvUnlockQueue.patch Copying CBMC proofs from aws/amazon-freertos repo ./tools/cbmc to this repo ./FreeRTOS/Test/CBMC as is. 2020-03-31 14:21:53 -07:00
0009-Remove-overflow-asserts-from-xQueueGenericCreate.patch Update kernel submodule pointer to version 47338393f (#456) 2020-12-08 15:44:14 -08:00
__init__.py Adding FreeRTOS+TCP CBMC proofs to FreeRTOS/FreeRTOS (#56) 2020-04-21 15:40:08 -07:00
compute_patch.py Adding FreeRTOS+TCP CBMC proofs to FreeRTOS/FreeRTOS (#56) 2020-04-21 15:40:08 -07:00
FreeRTOSConfig.h [AUTO][RELEASE]: Bump file header version to "202011.00" 2020-11-10 14:45:34 -08:00
FreeRTOSIPConfig.h [AUTO][RELEASE]: Bump file header version to "202011.00" 2020-11-10 14:45:34 -08:00
Makefile Adding FreeRTOS+TCP CBMC proofs to FreeRTOS/FreeRTOS (#56) 2020-04-21 15:40:08 -07:00
patch.py Adding FreeRTOS+TCP CBMC proofs to FreeRTOS/FreeRTOS (#56) 2020-04-21 15:40:08 -07:00
patches_constants.py Adding FreeRTOS+TCP CBMC proofs to FreeRTOS/FreeRTOS (#56) 2020-04-21 15:40:08 -07:00
README.md Copying CBMC proofs from aws/amazon-freertos repo ./tools/cbmc to this repo ./FreeRTOS/Test/CBMC as is. 2020-03-31 14:21:53 -07:00
unpatch.py Adding FreeRTOS+TCP CBMC proofs to FreeRTOS/FreeRTOS (#56) 2020-04-21 15:40:08 -07:00

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.