FreeRTOS-Kernel/FreeRTOS/Test/VeriFast/include/proof
Nathan Chong 4f87f485d5
Update VeriFast proofs (#836)
* Undo syntax changes preventing VeriFast parsing

* Update proofs inline with source changes

Outstanding:
  - xQueueGenericReset return code
  - Not using prvIncrementQueueTxLock or prvIncrementQueueRxLock macros

* Remove git hash check

* Document new changes between proven code and implementation

* Update copyright header

* VeriFast proofs: turn off uncrustify checks

Uncrustify requires formatting of comments that is at odds with VeriFast's
proof annotations, which are contained within comments.

* Update ci.yml

Co-authored-by: Joseph Julicher <jjulicher@mac.com>
Co-authored-by: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
2022-10-27 14:54:38 -07:00
..
common.gh Update VeriFast proofs (#836) 2022-10-27 14:54:38 -07:00
list.h Update VeriFast proofs (#836) 2022-10-27 14:54:38 -07:00
queue.h Update VeriFast proofs (#836) 2022-10-27 14:54:38 -07:00
queuecontracts.h Update VeriFast proofs (#836) 2022-10-27 14:54:38 -07:00