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
3014 commits 3 branches 99 tags 214 MiB
Commit graph

3014 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
95049a67c0 Use VeriFast's build-in treatment of malloc and free instead of port-specific implementation. 2022-10-24 12:25:27 -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
e9c9b27ddb Added vscode settings directory to .gitignore. 2022-10-21 11:47:00 -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
ee70a7815d Resolved VF parse error. Deleted functions involving inline assembler. 2022-10-13 12:52:57 -04:00
Tobias Reinhard
997d39d894 Added temporary work-around for VF's define_name bug. 
For bug description, see minimal example `define_name`.
 2022-10-13 12:40:50 -04:00
Tobias Reinhard
8aa7af3fd5 Resolved VF parser error: VF does not support attribute used. 2022-10-13 12:36:18 -04:00
Tobias Reinhard
6129726501 Resolved VF preprocessor error. 
VF's preprocessor cannot handle context-sensitive macro expansion.
 2022-10-13 12:21:36 -04:00
Tobias Reinhard
50c5b21a59 Resolved VF preprocessor error. 
VF's preprocessor cannot handle expansion of `PRIVILEGED_FUNCTION` macro because the normal and the context-free preprocessor consume different numbers of tokens. We resolved this temporarily by deleting the macro.
 2022-10-13 11:34:24 -04:00
Tobias Reinhard
a1a16c7dba Dumped new version of pico sdk submodule. 2022-10-13 10:02:31 -04:00
Tobias Reinhard
f7316a77f0 Added temporary work-around for VF's define_name bug. 
For bug description, see minimal example `define_name`.
 2022-10-13 10:01:34 -04:00
Tobias Reinhard
4431a1f5d6 Resolved VF parse error: VF does not support local static variables. 
Removed problematic function definition for now.
 2022-10-13 09:52:20 -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