Skip to content

Conversation

@nchong-at-aws
Copy link
Contributor

Description

VeriFast is a deductive verification tool. This PR adds VeriFast proofs for the kernel queue data structure. The proofs give assurance of memory safety, thread safety and function correctness.

Test Steps

See VeriFast/README.md

Related Issue

None

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

@cobusve cobusve requested a review from yuhui-zheng July 2, 2020 19:45
@cobusve cobusve merged commit 529c481 into FreeRTOS:master Jul 2, 2020
AniruddhaKanhere added a commit that referenced this pull request Jul 28, 2020
* Fixed Imports for Infineon XMC1100 Board (#88)

Co-authored-by: RichardBarry <[email protected]>

* FreeRTOS+TCP : add memory statistics and dump packets, v3 (#83)

* FreeRTOS+TCP : add memory statistics and dump packets, v3

* Two changes as requested by Aniruddha

Co-authored-by: Hein Tibosch <[email protected]>
Co-authored-by: Aniruddha Kanhere <[email protected]>

* Folder structure change + Fix broken Projects (#103)

* Update folder structure

* Correct project files

* Move test folder

* Some changes after Yuki's comments

* Add checks in FreeRTOS_Socket.c (#104)

* Add fail-safes to FreeRTOS_Socket.c

* Use all 'pd' errors

* Correction after Hein's comments

* Correction after Hein's comments v2

* Changes after Hein's comments

* Update after Gary's comments

* Add VeriFast kernel queue proofs (#117)

* Remove unnecessary semicolon from the linker file (#121)

This was creating problem with the onboard LPCLink debug probe.

Signed-off-by: Gaurav Aggarwal <[email protected]>

* Add Full TCP test suite - not using secure sockets (#131)

* Add Full-TCP suite

* delete unnecessary files

* Change after Joshua's comments

* Add changes from 2225-2227 amazon-FreeRTOS (#134)

* FreeRTOS+TCP Adding the combined driver for SAM4E and SAME70 v2 (#78)

* Adding a combined +TCP driver for SAM4E and SAME70

* Changes after review from Aniruddha

Co-authored-by: Hein Tibosch <[email protected]>
Co-authored-by: Aniruddha Kanhere <[email protected]>

* Prove buffer lemmas (#124)

* 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 <[email protected]>

* Sync with +TCP amazon-FreeRTOS (#158)

* DNS.c commit

* IP.c commit

* Add various source & header files

* Add Uncrustify file used for Kernel. (#163)

* Add Atmel Studio projects for ATMega4809 and AVR128DA48 (#159)

* Added explicit cast to allow roll over and avoid integer promotion during cycles counters comparison in recmutex.c.

* Fixed type mismatch between declaration and definition of function xAreSemaphoreTasksStillRunning( void ).

* Added Atmel Studio demo projects for ATMega4809 and AVR128DA48.

* Per https://www.freertos.org/upgrading-to-FreeRTOS-V8.html, I'm updating portBASE_TYPE to BaseType_t.

Signed-off-by: Yuhui Zheng <[email protected]>

* Update register test for ATmega4809
- to cover r28, r29, r31.
- call public API taskYIELD() instead of portYIELD().

* Update ATmega4809 readme.md to include info for serial port setup, and minor wording fix.

Co-authored-by: Alexandru Niculae - M17336 <[email protected]>

Co-authored-by: S.Burch <[email protected]>
Co-authored-by: RichardBarry <[email protected]>
Co-authored-by: Hein Tibosch <[email protected]>
Co-authored-by: Hein Tibosch <[email protected]>
Co-authored-by: Nathan Chong <[email protected]>
Co-authored-by: Gaurav-Aggarwal-AWS <[email protected]>
Co-authored-by: Yuhui Zheng <[email protected]>
Co-authored-by: Carl Lundin <[email protected]>
Co-authored-by: Alexandru Niculae - M17336 <[email protected]>
Zangetsu112 pushed a commit to Zangetsu112/FreeRTOS-evpp that referenced this pull request Aug 18, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants