FreeRTOS-Kernel/FreeRTOS-Plus/Test/CBMC/patches
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)
2020-09-17 17:16:33 -07:00
..
.gitattributes Move CBMC proofs to FreeRTOS+ directory (#64) 2020-05-05 09:57:18 -07:00
.gitignore Move CBMC proofs to FreeRTOS+ directory (#64) 2020-05-05 09:57:18 -07:00
0005-remove-static-from-prvCopyDataToQueue.patch Move CBMC proofs to FreeRTOS+ directory (#64) 2020-05-05 09:57:18 -07:00
0005-Remove-volatile-qualifier-from-tasks-variables.patch Move CBMC proofs to FreeRTOS+ directory (#64) 2020-05-05 09:57:18 -07:00
0006-Remove-static-from-prvNotifyQueueSetContainer.patch Move CBMC proofs to FreeRTOS+ directory (#64) 2020-05-05 09:57:18 -07:00
0007-Remove-static-from-prvUnlockQueue.patch Move CBMC proofs to FreeRTOS+ directory (#64) 2020-05-05 09:57:18 -07:00
__init__.py Move CBMC proofs to FreeRTOS+ directory (#64) 2020-05-05 09:57:18 -07:00
compute_patch.py Move CBMC proofs to FreeRTOS+ directory (#64) 2020-05-05 09:57:18 -07:00
FreeRTOSConfig.h Sync back V10.4.1 (#282) 2020-09-17 17:16:33 -07:00
FreeRTOSIPConfig.h Sync back V10.4.1 (#282) 2020-09-17 17:16:33 -07:00
Makefile Move CBMC proofs to FreeRTOS+ directory (#64) 2020-05-05 09:57:18 -07:00
patch.py Move CBMC proofs to FreeRTOS+ directory (#64) 2020-05-05 09:57:18 -07:00
patches_constants.py Move CBMC proofs to FreeRTOS+ directory (#64) 2020-05-05 09:57:18 -07:00
README.md Move CBMC proofs to FreeRTOS+ directory (#64) 2020-05-05 09:57:18 -07:00
unpatch.py Move CBMC proofs to FreeRTOS+ directory (#64) 2020-05-05 09:57:18 -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.