len0rd/FreeRTOS-Kernel
1
0
Fork 0
mirror of https://github.com/FreeRTOS/FreeRTOS-Kernel.git synced 2025-12-11 14:15:12 -05:00
Code Issues Projects Releases Packages Wiki Activity

Updated documentation of preprocessing scripts and deleted comments.

Browse source
This commit is contained in:
Tobias Reinhard 2022-12-31 09:55:39 -05:00
parent 1b0869dac0
commit 9df86117b8
3 changed files with 19 additions and 35 deletions
Download patch file Download diff file Expand all files Collapse all files

27
Test/VeriFast/tasks/vTaskSwitchContext/preprocessing_scripts/prepare_file_for_VeriFast.sh
View file

@ -2,9 +2,12 @@
ps -o comm= -p $$ ps -o comm= -p $$
# This script expects the following command line arguments: # This script expects the following command line arguments:
# $1 : Absolute path to the root dir of this repository # $1 : Absolute path to the source file that should be prepared for VeriFast.
# $2 : Absolute path to the root of the directory containing the VeriFast proofs # $2 : Absolute path to which the result shall be written.
# $3 : Absolute path to the VeriFast directory # $3 : Absolute path under which preprocessor error shall be logged.
# $4 : Absolute path to the root dir of this repository
# $5 : Absolute path to the root of the directory containing the VeriFast proofs
# $6 : Absolute path to the VeriFast directory
SRC_FILE="$1" SRC_FILE="$1"
OUT_FILE="$2" OUT_FILE="$2"
@ -13,18 +16,6 @@ REPO_BASE_DIR="$4"
VF_PROOF_BASE_DIR="$5" VF_PROOF_BASE_DIR="$5"
VF_DIR="$6" VF_DIR="$6"
echo SRC_FILE
echo "$1"
echo OUT_FILE
echo "$2"
echo FILE_PP_ERR_LOG
echo "$3"
echo REPO_BASE_DIR
echo "$4"
echo VF_PROOF_BASE_DIR
echo "$5"
echo VF_DIR
echo "$6"
# Load functions used to compute paths. # Load functions used to compute paths.
. "$VF_PROOF_BASE_DIR/paths.sh" . "$VF_PROOF_BASE_DIR/paths.sh"
@ -43,12 +34,12 @@ fi
# Preprocessing the source file # Preprocessing the source file
# Output is written to '$FILE_PP_LOG' and error report is written to # Output is written to '$FILE_PP_LOG' and error report is written to
# '$FILE_PP_ERR_LOG'. # '$FILE_PP_ERR_LOG'.
"$PP_SCRIPT_DIR/preprocess_file_for_verification.sh" $SRC_FILE \ "$PP_SCRIPT_DIR/preprocess_file_for_verification.sh" $SRC_FILE \
$FILE_PP_LOG $FILE_PP_ERR_LOG \ $FILE_PP_LOG $FILE_PP_ERR_LOG \
$REPO_BASE_DIR $VF_PROOF_BASE_DIR $VF_DIR $REPO_BASE_DIR $VF_PROOF_BASE_DIR $VF_DIR
cp "$FILE_PP_LOG" "$FILE_RW_LOG" cp "$FILE_PP_LOG" "$FILE_RW_LOG"
"$PP_SCRIPT_DIR/vf_rewrite.sh" "$FILE_RW_LOG" "$PP_SCRIPT_DIR/vf_rewrite.sh" "$FILE_RW_LOG"
cp "$FILE_RW_LOG" "$OUT_FILE" cp "$FILE_RW_LOG" "$OUT_FILE"

18
Test/VeriFast/tasks/vTaskSwitchContext/preprocessing_scripts/preprocess_file_for_verification.sh
View file

@ -1,8 +1,8 @@
#!/bin/bash #!/bin/bash
# This script preprocesses an given source file annotated with VeriFast proof # This script preprocesses a given source file annotated with VeriFast proof
# steps. Include paths are configured to fit 'tasks.c', but it might also be # steps. Include paths are configured to fit 'tasks.c', but it might also be
# useful for other source files. The preprocessor is configured to include the # useful for other source files. The preprocessor is configured to include the
# proper proof files from VeriFast's standard library and to also include # proper proof files from VeriFast's standard library and to also include
# source code guarded by 'VERIFAST' defines. # source code guarded by 'VERIFAST' defines.
@ -23,18 +23,6 @@ REPO_BASE_DIR="$4"
VF_PROOF_BASE_DIR="$5" VF_PROOF_BASE_DIR="$5"
VF_DIR="$6" VF_DIR="$6"
echo SRC_FILE
echo "$1"
echo OUT_FILE
echo "$2"
echo ERR_FILE
echo "$3"
echo REPO_BASE_DIR
echo "$4"
echo VF_PROOF_BASE_DIR
echo "$5"
echo VF_DIR
echo "$6"
# Load functions used to compute paths. # Load functions used to compute paths.
@ -59,4 +47,4 @@ ${PICO_INCLUDE_FLAGS[@]} \
-I`prod_header_dir $REPO_BASE_DIR` \ -I`prod_header_dir $REPO_BASE_DIR` \
\ \
-c "$SRC_FILE" \ -c "$SRC_FILE" \
1>"$OUT_FILE" 2>"$ERR_FILE" 1>"$OUT_FILE" 2>"$ERR_FILE"

9
Test/VeriFast/tasks/vTaskSwitchContext/preprocessing_scripts/vf_rewrite.sh
View file

@ -2,7 +2,7 @@ ps -o comm= -p $$
# This script rewrites a given source in-pace such that the result can be # This script rewrites a given source in-pace such that the result can be
# processed by VeriFast. Each rewrite below concerns a specific construct # processed by VeriFast. Each rewrite below concerns a specific construct
# VeriFast cannot handle. When VeriFast will be extended to handle a # VeriFast cannot handle. When VeriFast will be extended to handle a
# problematic construct we encountered, the corresponding rewirte below can be # problematic construct we encountered, the corresponding rewirte below can be
# deleted. # deleted.
# #
@ -33,12 +33,18 @@ echo "Commenting out line/file pragmas"
rewrite "^#" "// &" rewrite "^#" "// &"
echo "Fixing order of 'long', 'unsigned'" echo "Fixing order of 'long', 'unsigned'"
echo "Reported issue 338:"
echo "https://github.com/verifast/verifast/issues/338"
rewrite "long unsigned int" "unsigned long int" rewrite "long unsigned int" "unsigned long int"
echo "Delete fixed-sized array typedefs" echo "Delete fixed-sized array typedefs"
echo "Reported issue 339:"
echo "https://github.com/verifast/verifast/issues/339"
rewrite "typedef .*\[[0-9]*\];" "" rewrite "typedef .*\[[0-9]*\];" ""
echo "Delete attributes" echo "Delete attributes"
echo "Reported issue 340:"
echo "https://github.com/verifast/verifast/issues/340"
rewrite "__attribute__(([_a-z]*))" "" rewrite "__attribute__(([_a-z]*))" ""
# Note: `\s` or `:space:` not work on MacOs. # Note: `\s` or `:space:` not work on MacOs.
rewrite "__attribute__( ( [_a-z]* ) )" "" rewrite "__attribute__( ( [_a-z]* ) )" ""
@ -57,4 +63,3 @@ rewrite "const [*]" "*"
echo "Uncomment special includes to allow VeriFast proofs to refer to config macros" echo "Uncomment special includes to allow VeriFast proofs to refer to config macros"
rewrite "//VF_include #include" "#include" rewrite "//VF_include #include" "#include"
rewrite "//VF_macro #" "#" rewrite "//VF_macro #" "#"