summaryrefslogtreecommitdiff
path: root/FreeRTOS/Test/VeriFast
Commit message (Collapse)AuthorAgeFilesLines
* [AUTO][RELEASE]: Bump file header version to "202212.00"jasonpcarroll2022-12-1028-28/+28
|
* [AUTO][RELEASE]: Bump file header version to "202211.00"jasonpcarroll2022-12-0128-28/+28
|
* Update VeriFast proofs (#836)Nathan Chong2022-10-2731-1859/+1872
| | | | | | | | | | | | | | | | | | | | | | | | | * 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>
* Update uncrustify configuration and improve CI setup (see ↵swaldhoer2022-02-048-213/+213
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | FreeRTOS/FreeRTOS-Kernel/pull/445) (#782) * pin uncrustify version and update configuration file * Update AbortDelay.c * Update BlockQ.c * Update MessageBufferDemo.c * Update QPeek.c * Update StaticAllocation.c * Update integer.c * Update recmutex.c * Update create.c * Update prvCopyDataToQueue.c * Update prvUnlockQueue.c * Update vQueueDelete.c * Update xQueueGenericSend.c * Update xQueueGenericSendFromISR.c * Update xQueuePeek.c * Update xQueueReceive.c * Update IntSemTest.c * Update dynamic.c * Update lexicon.txt Co-authored-by: alfred gedeon <28123637+alfred2g@users.noreply.github.com>
* Apply release changes to main branch (#759)johnrhen2021-12-2328-28/+28
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | * Update History.txt and README.md for December release (#744) * Update History.txt and README.md for release * Bump mbedtls submodule to v2.28.0 (#745) * Patch project files for mbedtls (#751) * Apply group 1 patches * Apply patches for group 2 * Update project files for mbedTLS new version Signed-off-by: Gaurav Aggarwal <aggarg@amazon.com> * Fix warnings in projects Signed-off-by: Gaurav Aggarwal <aggarg@amazon.com> * Fix warnings in HTTP_S3_Download demo Signed-off-by: Gaurav Aggarwal <aggarg@amazon.com> Co-authored-by: Gaurav Aggarwal <aggarg@amazon.com> * Update changelog and history for corePKCS11 update (#752) * Update submodule pointer and manifest.yml for corePKCS11 (#754) * Update readme and history.txt to show that Sigv4 is a newly added library (#756) * Revert update to v143 of VS toolset (#757) * [AUTO][RELEASE]: Bump file header version to "202112.00" * Update file headers to satisfy core checks Co-authored-by: Muneeb Ahmed <54290492+muneebahmed10@users.noreply.github.com> Co-authored-by: Gaurav Aggarwal <aggarg@amazon.com> Co-authored-by: johnrhen <johnrhen@users.noreply.github.com>
* [AUTO][RELEASE]: Bump file header version to "202111.00"aggarg2021-11-1328-28/+28
|
* [AUTO][RELEASE]: Bump file header version to "202107.00"tianmc12021-07-2428-28/+28
|
* Add uncrustify github workflow (#659)alfred gedeon2021-07-2224-1689/+1796
| | | | | | | | | | | | | | | | | | | | | | | * Add uncrustify github workflow * Fix exclusion pattern * fix find expression * exclude uncrustify files * Uncrustify common demo and test files * exlude white space checking files * Fix EOL whitespace checker * Remove whitespaces from EOL * Fix space at EOL * Fix find spaces at EOL Co-authored-by: Archit Aggarwal <architag@amazon.com>
* Merge FreeRTOS 202104.00 to main (#585)Archit Aggarwal2021-04-2928-56/+56
|
* Minor VeriFast proof changes to match V10.4.3 (#519)Nathan Chong2021-02-2529-33/+148
| | | | | * Minor changes for V10.4.3 * Update license
* [AUTO][RELEASE]: Bump file header version to "202012.00"Joseph Julicher2020-12-1528-28/+28
|
* Syntactic proof changes to track 10.4.1 changes (#322)Nathan Chong2020-10-066-17/+19
| | | All changes restricted to comments/formatting.
* List proofs and signoff (#194)Nathan Chong2020-08-2716-59/+1737
|
* Prove buffer lemmas (#124)Nathan Chong2020-07-2126-1768/+2027
| | | | | | | | | | | | | * 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>
* Add VeriFast kernel queue proofs (#117)Nathan Chong2020-07-0230-0/+3700