diff --git a/Test/VeriFast/tasks/vTaskSwitchContext/preprocessing_scripts/prepare_file_for_VeriFast.sh b/Test/VeriFast/tasks/vTaskSwitchContext/preprocessing_scripts/prepare_file_for_VeriFast.sh index b71310f01..397d3f8e0 100755 --- a/Test/VeriFast/tasks/vTaskSwitchContext/preprocessing_scripts/prepare_file_for_VeriFast.sh +++ b/Test/VeriFast/tasks/vTaskSwitchContext/preprocessing_scripts/prepare_file_for_VeriFast.sh @@ -2,9 +2,12 @@ ps -o comm= -p $$ # This script expects the following command line arguments: -# $1 : Absolute path to the root dir of this repository -# $2 : Absolute path to the root of the directory containing the VeriFast proofs -# $3 : Absolute path to the VeriFast directory +# $1 : Absolute path to the source file that should be prepared for VeriFast. +# $2 : Absolute path to which the result shall be written. +# $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" OUT_FILE="$2" @@ -13,18 +16,6 @@ REPO_BASE_DIR="$4" VF_PROOF_BASE_DIR="$5" 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. . "$VF_PROOF_BASE_DIR/paths.sh" @@ -43,12 +34,12 @@ fi # 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'. "$PP_SCRIPT_DIR/preprocess_file_for_verification.sh" $SRC_FILE \ $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" "$PP_SCRIPT_DIR/vf_rewrite.sh" "$FILE_RW_LOG" -cp "$FILE_RW_LOG" "$OUT_FILE" \ No newline at end of file +cp "$FILE_RW_LOG" "$OUT_FILE" diff --git a/Test/VeriFast/tasks/vTaskSwitchContext/preprocessing_scripts/preprocess_file_for_verification.sh b/Test/VeriFast/tasks/vTaskSwitchContext/preprocessing_scripts/preprocess_file_for_verification.sh index 86580feb1..a056731f5 100755 --- a/Test/VeriFast/tasks/vTaskSwitchContext/preprocessing_scripts/preprocess_file_for_verification.sh +++ b/Test/VeriFast/tasks/vTaskSwitchContext/preprocessing_scripts/preprocess_file_for_verification.sh @@ -1,8 +1,8 @@ #!/bin/bash -# This script preprocesses an given source file annotated with VeriFast proof -# steps. Include paths are configured to fit 'tasks.c', but it might also be +# 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 # useful for other source files. The preprocessor is configured to include the # proper proof files from VeriFast's standard library and to also include # source code guarded by 'VERIFAST' defines. @@ -23,18 +23,6 @@ REPO_BASE_DIR="$4" VF_PROOF_BASE_DIR="$5" 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. @@ -59,4 +47,4 @@ ${PICO_INCLUDE_FLAGS[@]} \ -I`prod_header_dir $REPO_BASE_DIR` \ \ -c "$SRC_FILE" \ -1>"$OUT_FILE" 2>"$ERR_FILE" \ No newline at end of file +1>"$OUT_FILE" 2>"$ERR_FILE" diff --git a/Test/VeriFast/tasks/vTaskSwitchContext/preprocessing_scripts/vf_rewrite.sh b/Test/VeriFast/tasks/vTaskSwitchContext/preprocessing_scripts/vf_rewrite.sh index 8408ab8b1..40ee596c0 100755 --- a/Test/VeriFast/tasks/vTaskSwitchContext/preprocessing_scripts/vf_rewrite.sh +++ b/Test/VeriFast/tasks/vTaskSwitchContext/preprocessing_scripts/vf_rewrite.sh @@ -2,7 +2,7 @@ ps -o comm= -p $$ # This script rewrites a given source in-pace such that the result can be # 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 # deleted. # @@ -33,12 +33,18 @@ echo "Commenting out line/file pragmas" rewrite "^#" "// &" 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" echo "Delete fixed-sized array typedefs" +echo "Reported issue 339:" +echo "https://github.com/verifast/verifast/issues/339" rewrite "typedef .*\[[0-9]*\];" "" echo "Delete attributes" +echo "Reported issue 340:" +echo "https://github.com/verifast/verifast/issues/340" rewrite "__attribute__(([_a-z]*))" "" # Note: `\s` or `:space:` not work on MacOs. rewrite "__attribute__( ( [_a-z]* ) )" "" @@ -57,4 +63,3 @@ rewrite "const [*]" "*" echo "Uncomment special includes to allow VeriFast proofs to refer to config macros" rewrite "//VF_include #include" "#include" rewrite "//VF_macro #" "#" -