1This directory includes patches to FreeRTOS required to run the CBMC proofs. 2 3The patches fall into three classes: 4* First is a refactoring of prvCheckOptions 5* Second is the removal of static attributes from some functions 6* Third is two patches dealing with shortcomings of CBMC that should be removed soon.