len0rd/FreeRTOS-Kernel
1
0
Fork 0
mirror of https://github.com/FreeRTOS/FreeRTOS-Kernel.git synced 2025-12-15 08:05:15 -05:00
Code Issues Projects Releases Packages Wiki Activity
3097 commits 3 branches 99 tags 215 MiB
Commit graph

3097 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
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
Tobias Reinhard
21457b6611 Added missing include flag in vf start script. 2022-10-11 15:10:20 -04:00
Tobias Reinhard
80651ca320 Switched submodules to verifast branch. 2022-10-11 14:50:43 -04:00
Tobias Reinhard
eec276d0a3 Replaced Pico SDK submodule by fork. 2022-10-11 14:39:57 -04:00
Tobias Reinhard
5995eb2ac4 Added Pico SDK repo as submodule. 2022-10-11 14:34:41 -04:00
Tobias Reinhard
bcde498313 Added FreeRTOS-SMP-Demos repo as submodule. 2022-10-11 14:32:14 -04:00
Tobias Reinhard
0c3f65d8ad Setup environment for VeriFast proof and start script for vfide. 2022-10-11 12:20:41 -04:00
Tobias Reinhard
143e76755e Added FreeRTOS-SMP-Demos repo as submodule. 2022-10-11 11:54:32 -04:00
Tobias Reinhard
b3af566a7d Added .DS_Store files to .gitignore. 2022-10-11 11:54:15 -04:00
Graham Sanderson
13f034eb74
RP2040: Fix compiler warning and comment (#509) 
Co-authored-by: graham sanderson <graham.sanderson@raspeberryi.com>
 2022-06-24 17:23:51 +05:30
Gaurav-Aggarwal-AWS
b3918c7f38
Remove ThirdParty from core checker in smp branch (#512) 
Signed-off-by: Gaurav Aggarwal <aggarg@amazon.com>
 2022-06-24 17:22:15 +05:30
graham sanderson
b87dfa3e97 RP2040: Allow FreeRTOS to be added to the parent CMake project post initialization of the Pico SDK 2022-06-23 11:32:40 -07:00
Sudeep Mohanty
2eff037080
Update prvYieldCore() compile warning for single core targets (#505) 
When configNUM_CORES is 1, prvYieldCore() generates an array subscript
outofbound error (-Warray-bounds) when compiled with GCC with space
optimization enabled (-Os).

This commit updates the code flow in prvYieldCore() to compile out
the part where yield is needed on the other core which is unnecessary
for single-core targets.
 2022-06-22 10:03:44 +05:30
Graham Sanderson
45dd83a8e3
Fix RP2040 assertion due to yield spin lock info being wrongly shared between multiple cores (#501) 
Co-authored-by: graham sanderson <graham.sanderson@raspeberryi.com>
 2022-06-09 10:59:35 -07:00