len0rd/FreeRTOS-Kernel
1
0
Fork 0
mirror of https://github.com/FreeRTOS/FreeRTOS-Kernel.git synced 2025-12-11 22:25:14 -05:00
Code Issues Projects Releases Packages Wiki Activity
3021 commits 3 branches 99 tags 214 MiB
Commit graph

54 commits

Author SHA1 Message Date
Tobias Reinhard
e238d791ab Moved stack predicate and lemmas to separate header. 2022-10-27 12:51:24 -04:00
Tobias Reinhard
2bcdc31ff8 Deleted deprecated version of pointer size axiom. 2022-10-27 12:45:38 -04:00
Tobias Reinhard
2b82220cec Refined stack predicate, validated it and verified pxPortInitialiseStack impl from RP2040 port. 2022-10-27 12:43:10 -04:00
Tobias Reinhard
b5f0b2f74d Added snippet from RP2040 port.c to verification code base to allow verification of contract from portable.h 2022-10-26 10:08:29 -04:00
Tobias Reinhard
8bb4f13ae5 Introduced new type-safe macro for unsigned pdFALSE and pdTRUE. 2022-10-26 09:14:11 -04:00
Tobias Reinhard
a78bc21b26 Simplified proof state in prvInitialiseNewTask. 2022-10-26 08:11:47 -04:00
Tobias Reinhard
40931d229d Justified memset of TCB fields in prvInitialiseNewTask. 
Fields: `pxNewTCB->ucNotifyState` and `pxNewTCB->ulNotifiedValue`
 2022-10-25 16:56:28 -04:00
Tobias Reinhard
8a8f0ab9b1 Proved memory safety of name-writing loop in prvInitialiseNewTask. 2022-10-25 14:57:26 -04:00
Tobias Reinhard
82be7cb23a Temporarily eliminated runtime assertion. 2022-10-25 14:40:50 -04:00
Tobias Reinhard
8b958c7834 Axiomatized knowledge about RP2040 architecture and added tmp workaround for over/underflows. 2022-10-25 14:34:01 -04:00
Tobias Reinhard
06bc0fbb2d Resolved VF reporting type errors for memset call and disproved some overflows and underflows. 2022-10-25 13:58:06 -04:00
Tobias Reinhard
1042ea8cf8 Refined task control block predicate TCB_p such that it can be used to justify memset-ing the stack. 2022-10-25 13:22:10 -04:00
Tobias Reinhard
80134a65ed VeriFast cannot handle casts of side-effectful expressions. 2022-10-25 12:49:33 -04:00
Tobias Reinhard
5a7916bff0 Added predicates to reason about TCB_t and substructures. 2022-10-24 16:17:41 -04:00
Tobias Reinhard
f1a0170309 Initialized memory safety proof for xTaskCreate. 2022-10-24 12:29:55 -04:00
Tobias Reinhard
746c02f34a Specified font size in VF startup script. 2022-10-24 12:26:12 -04:00
Tobias Reinhard
32480e74c4 Resolved VF errors 
- VeriFast does not support nested union definitions. Removed those temporarily.
- VeriFast does not support duplicate function prototypes. Prevented include of unguarded system header file.
 2022-10-22 16:30:03 -04:00
Tobias Reinhard
47e6fa7398 Resolved VF parse errors: const pointers. 2022-10-22 14:02:04 -04:00
Tobias Reinhard
663ea1fb77 Resolved VF parse errors. 
- const pointers
- inline assembler
- statements blocks consisting of multiple elements used in expression contexts, e.g., `({e1 e2;})`
- multiple pointer declarations to user-defined types in single line, i.e., `A *p1, *p2;`
 2022-10-22 13:52:12 -04:00
Tobias Reinhard
55cfee8798 Resolved VF parse error: VF does not support const pointers. 2022-10-22 13:28:40 -04:00
Tobias Reinhard
785723ff45 Replaced asm macros by failing assertion. 2022-10-22 13:25:53 -04:00
Tobias Reinhard
342ab6463c Resolved VF parse error: VF does not support const pointers. 2022-10-22 13:00:58 -04:00
Tobias Reinhard
eeae596776 Replaced asm macro by failing assertion. 2022-10-22 12:39:54 -04:00
Tobias Reinhard
75fa197ac9 Fixed include paths to submodules in preprocessing script. 2022-10-22 12:01:17 -04:00
Tobias Reinhard
ea00b82275 Simplified paths in preprocessing script 2022-10-22 11:56:03 -04:00
Tobias Reinhard
83d8831729 Updated include paths in preprocessing script to ensure that only direct submodules as referenced. 2022-10-22 11:05:09 -04:00
Tobias Reinhard
f11cb629f3 Generalized paths to resources used in preprocessing script. 2022-10-21 17:55:21 -04:00
Tobias Reinhard
d3cfeebca1 Ensured that preprocessing script uses the smp demo submodule. 2022-10-21 17:42:05 -04:00
Tobias Reinhard
47aa491e31 Ensured that preprocessing script uses the pico sdk submodule. 2022-10-21 17:37:32 -04:00
Tobias Reinhard
81bb9d6b1b Delete inline directives 2022-10-21 12:31:19 -04:00
Tobias Reinhard
6af1321b43 VF rewrite: Delete attributes. 2022-10-21 12:27:58 -04:00
Tobias Reinhard
da0c8ffb76 Replaced problematic system headers by VeriFast headers. 2022-10-21 11:44:53 -04:00
Tobias Reinhard
dfce64bd18 Dump preprocessed tasks.c file. 2022-10-21 11:18:28 -04:00
Tobias Reinhard
23539193c0 Rewrite script: Deleted fixed-sized array typedefs from preprocessed file. 2022-10-21 11:03:34 -04:00
Tobias Reinhard
2c493715f4 Configured preprocessing script to process tasks.c file with verifast config. 2022-10-21 10:56:47 -04:00
Tobias Reinhard
6000cbd3bd Reordered include directives. 2022-10-21 10:22:52 -04:00
Tobias Reinhard
e9302f35ac Moved pragma rewrites to vf_rewrites.sh. 2022-10-14 16:41:48 -04:00
Tobias Reinhard
8ca47345d4 Added script to rewrite preprocessed source file into a format VeriFast understands. 2022-10-14 16:19:50 -04:00
Tobias Reinhard
95440b41be Added preprocessing log directory to .gitignore. 2022-10-14 15:25:17 -04:00
Tobias Reinhard
cf9b1e9aae Preprocessing script replaces comments out line/file pragmas. 2022-10-14 15:22:57 -04:00
Tobias Reinhard
24130f5334 Added VF startup script for preprocessed tasks.c. 
The script preprocesses task.c according to the RP2040 configuration and launches verifast.
 2022-10-14 13:37:30 -04:00
Tobias Reinhard
7d029778bf Added scripts to build kernel and to preprocess tasks.c. 
The scripts use the demo configuration for RP2040.
 2022-10-14 13:23:37 -04:00
Tobias Reinhard
d7fff36a2b Update SMP demo submodule. 2022-10-14 13:10:53 -04:00
Tobias Reinhard
a1a16c7dba Dumped new version of pico sdk submodule. 2022-10-13 10:02:31 -04:00
Tobias Reinhard
21f9a95a10 Fixed proof setup include path 
The include path contained some directories within the SMP demos FreeRTOS source tree (which is the official unaltered FreeRTOS repo). Updated the include path such that it points to our forked version of the FreeRTOS kernel repo.
 2022-10-13 09:48:11 -04:00
Tobias Reinhard
c71025fda0 Added minimal example for VF bug involving testing for macro defines in headers. 2022-10-13 09:16:54 -04:00
Tobias Reinhard
8ef03612b5 Update pico sdk submodule to resolve VF parse errors. 2022-10-12 11:07:19 -04:00
Tobias Reinhard
497a23d2eb Renamed VERIFAST_PROOF define into VERIFAST. 2022-10-11 15:32:57 -04:00
Tobias Reinhard
7f69232893 Resolved VF parse error in pico sdk's platform.h and deleted stub. 2022-10-11 15:26:00 -04:00
Tobias Reinhard
e652475628 vf start script now now uses pico sdk submodule for includes instead of system-wider pico sdk installation. 2022-10-11 15:14:03 -04:00