Documented scripts.

Test/VeriFast/tasks/vTaskSwitchContext/custom_build_scripts_RP2040/pp_flags.sh

@@ -1,5 +1,13 @@
 #!/bin/bash
 
+# This script defines common command line arguments for the preprocessor.
+
+# This script expects the following arguments:
+# $1 : Absolute path to the base directory of this repository.
+# $2 : Absolute path to the VeriFast proof directory.
+# $3 : Absolute path to the VeriFast installation directory.
+
+
 REPO_BASE_DIR="$1"
 VF_PROOF_BASE_DIR="$2"
 VF_DIR="$3"

Test/VeriFast/tasks/vTaskSwitchContext/custom_build_scripts_RP2040/preprocess_file_for_diff.sh

@@ -1,4 +1,19 @@
 #!/bin/bash
+
+
+# This script preprocesses a given source file. Include paths are configured to
+# fit 'tasks.c', but it might also be useful for other source files. 
+# The preprocessor is configured such that `diff`-ing results produced by this
+# script (from different versions of the same file) yields useful results.
+#
+# This script expects the following arguments:
+# $1 : Absolute path to the source file to be preprocessed.
+# $2 : Absolute path of the preprocessor's output file.
+# $3 : Absolute path to which the error report will be written.
+# $4 : Absolute path to the base directory of this repository.
+# $5 : Absolute path to the VeriFast proof directory.
+
+
 SRC_FILE="$1"
 OUT_FILE="$2"
 ERR_FILE="$3"
@@ -6,17 +21,6 @@ REPO_BASE_DIR="$4"
 VF_PROOF_BASE_DIR="$5"
 
 
-echo SRC_FILE:
-echo $SRC_FILE
-echo OUT_FILE:
-echo $OUT_FILE
-echo ERR_FILE:
-echo $ERR_FILE
-echo REPO_BASE_DIR:
-echo $REPO_BASE_DIR
-echo VF_PROOF_BASE_DIR:
-echo $VF_PROOF_BASE_DIR
-
 # Load functions used to compute paths.
 . "$VF_PROOF_BASE_DIR/paths.sh"
 

Test/VeriFast/tasks/vTaskSwitchContext/custom_build_scripts_RP2040/preprocess_file_for_verification.sh

@@ -1,4 +1,21 @@
 #!/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 
+# 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.
+#
+# This script expects the following arguments:
+# $1 : Absolute path to the source file to be preprocessed.
+# $2 : Absolute path of the preprocessor's output file.
+# $3 : Absolute path to which the error report will be written.
+# $4 : Absolute path to the base directory of this repository.
+# $5 : Absolute path to the VeriFast proof directory.
+# $6 : Absolute path to the VeriFast installation directory.
+
+
 SRC_FILE="$1"
 OUT_FILE="$2"
 ERR_FILE="$3"
@@ -14,12 +31,6 @@ VF_DIR="$6"
 . "`pp_script_dir $REPO_BASE_DIR`/pp_flags.sh" "$REPO_BASE_DIR" "$VF_PROOF_BASE_DIR" "$VF_DIR"
 
 
-# Flags to SKIP expensive proofs:
-# - VERIFAST_SKIP_BITVECTOR_PROOF__STACK_ALIGNMENT
-
-
-
-
 # Relevant clang flags:
 # -E : Run preprocessor
 # -C : Include comments in output

Test/VeriFast/tasks/vTaskSwitchContext/diff.sh

@@ -1,23 +1,28 @@
 #!/bin/bash
 
 
+# This script produces a diff between two versions of 'tasks.c':
+# (i) The production version of the source file and (ii) the verified version.
+# The diff is computed from the preprocessed version of both files which include
+# all code relevant to the proof. That is, that any change in a file required
+# by the VeriFast proof will shot up in the diff.
+# The diff report will be written to 'stats/diff_report.txt' directory.
+#
+# This script expects the following arguments:
+# $1 : Absolute path to the base directory of this repository.
+
 
 # Relative or absolute path to the directory this script and `paths.sh` reside in.
 PREFIX=`dirname $0`
 # Absolute path to the base of this repository.
 REPO_BASE_DIR="$1"
 
+
 # Load functions used to compute paths.
 . "$PREFIX/paths.sh"
 
+
 VF_PROOF_BASE_DIR=`vf_proof_base_dir $REPO_BASE_DIR`
-
-
-
-# Load functions used to compute paths.
-. "$PREFIX/paths.sh"
-
-VF_PROOF_DIR=`vf_proof_base_dir $REPO_BASE_DIR`
 PP_SCRIPT_DIR=`pp_script_dir $REPO_BASE_DIR`
 PP="$PP_SCRIPT_DIR/preprocess_file_for_diff.sh"
 LOG_DIR=`pp_log_dir $REPO_BASE_DIR`
@@ -55,16 +60,8 @@ $PP $VF_TASKS_C $PP_VF_TASKS_C \
     "$LOG_DIR/pp_vf_tasks_c_error_report.txt" \
     $REPO_BASE_DIR $VF_PROOF_BASE_DIR
 
-# pp script args
-# SRC_FILE="$1"
-# OUT_FILE="$2"
-# ERR_FILE="$3"
-# REPO_BASE_DIR="$4"
-# VF_PROOF_BASE_DIR="$5"
 
-
-
-echo Computing diff. Output written to:
+echo Computing diff. Report written to:
 echo \"$DIFF_REPORT\"
 
 git diff --no-index --ignore-all-space $PP_PROD_TASKS_C $PP_VF_TASKS_C \

Test/VeriFast/tasks/vTaskSwitchContext/start-vfide--preprocessed.sh

@@ -1,9 +1,4 @@
-# This script must be run from the directory in which it resides,
-# i.e., `FreeRTOS-Kernel/verification/verifast`.
-
-# This script expects the following command line arguments:
-# $1 : Absolute path to the VeriFast directory
-
+#!/bin/bash
 
 # Relative or absolute path to the directory this script and `paths.sh` reside in.
 PREFIX=`dirname $0`