diff --git a/Test/VeriFast/tasks/vTaskSwitchContext/diff.sh b/Test/VeriFast/tasks/vTaskSwitchContext/diff.sh index ac5c63c46..d80d3bf20 100755 --- a/Test/VeriFast/tasks/vTaskSwitchContext/diff.sh +++ b/Test/VeriFast/tasks/vTaskSwitchContext/diff.sh @@ -37,8 +37,6 @@ PP_OUT_DIR=`pp_out_dir $REPO_BASE_DIR` PP_PROD_TASKS_C=`pp_prod_tasks_c $REPO_BASE_DIR` PP_VF_TASKS_C=`pp_vf_tasks_c $REPO_BASE_DIR` -DIFF_REPORT=`diff_report $REPO_BASE_DIR` - ensure_output_dirs_exist $REPO_BASE_DIR echo preprocessing production version of 'tasks.c' @@ -52,8 +50,7 @@ $PP $VF_TASKS_C $PP_VF_TASKS_C \ $REPO_BASE_DIR $VF_PROOF_BASE_DIR -echo Computing diff. Report written to: -echo \"$DIFF_REPORT\" +echo Computing diff: +echo -git diff --no-index --ignore-all-space $PP_PROD_TASKS_C $PP_VF_TASKS_C \ -> "$DIFF_REPORT" \ No newline at end of file +git diff --no-index --ignore-all-space $PP_PROD_TASKS_C $PP_VF_TASKS_C diff --git a/Test/VeriFast/tasks/vTaskSwitchContext/paths.sh b/Test/VeriFast/tasks/vTaskSwitchContext/paths.sh index 42498376b..45824ecf2 100755 --- a/Test/VeriFast/tasks/vTaskSwitchContext/paths.sh +++ b/Test/VeriFast/tasks/vTaskSwitchContext/paths.sh @@ -13,7 +13,7 @@ function vf_proof_base_dir() { # of the original files. # # Expected arguments: -# $1 : Absolute path to the repository's base +# $1 : Absolute path to the repository's base function vf_proof_mod_src_dir() { REPO_BASE_DIR="$1" VF_PROOF_DIR=`vf_proof_base_dir $REPO_BASE_DIR` @@ -26,7 +26,7 @@ function vf_proof_mod_src_dir() { # of the original files. # # Expected arguments: -# $1 : Absolute path to the repository's base +# $1 : Absolute path to the repository's base function vf_proof_mod_header_dir() { REPO_BASE_DIR="$1" VF_PROOF_DIR=`vf_proof_base_dir $REPO_BASE_DIR` @@ -38,7 +38,7 @@ function vf_proof_mod_header_dir() { # the setup of the VeriFast proofs. # # Expected arguments: -# $1 : Absolute path to the repository's base +# $1 : Absolute path to the repository's base function vf_proof_setup_dir() { REPO_BASE_DIR="$1" VF_PROOF_DIR=`vf_proof_base_dir $REPO_BASE_DIR` @@ -46,11 +46,11 @@ function vf_proof_setup_dir() { echo "$VF_PROOF_DIR/proof_setup" } -# Returns the absolute path to the directory containing all lemmas and +# Returns the absolute path to the directory containing all lemmas and # definitions used written for the VeriFast proofs. # # Expected arguments: -# $1 : Absolute path to the repository's base +# $1 : Absolute path to the repository's base function vf_proof_dir() { REPO_BASE_DIR="$1" VF_PROOF_DIR=`vf_proof_base_dir $REPO_BASE_DIR` @@ -62,7 +62,7 @@ function vf_proof_dir() { # proof annotations. # # Expected arguments: -# $1 : Absolute path to the repository's base +# $1 : Absolute path to the repository's base function vf_annotated_tasks_c() { REPO_BASE_DIR="$1" VF_MOD_SRC_DIR=`vf_proof_mod_src_dir $REPO_BASE_DIR` @@ -73,18 +73,18 @@ function vf_annotated_tasks_c() { # Returns the absolute path to the directory the unmodified FreeRTOS headers. # # Expected arguments: -# $1 : Absolute path to the repository's base +# $1 : Absolute path to the repository's base function prod_header_dir() { REPO_BASE_DIR="$1" echo "$REPO_BASE_DIR/include" } -# Returns the absolute path to the directory the unmodified FreeRTOS source +# Returns the absolute path to the directory the unmodified FreeRTOS source # files. # # Expected arguments: -# $1 : Absolute path to the repository's base +# $1 : Absolute path to the repository's base function prod_src_dir() { REPO_BASE_DIR="$1" @@ -94,7 +94,7 @@ function prod_src_dir() { # Returns the absolute path to the unmodified version of `tasks.c`. # # Expected arguments: -# $1 : Absolute path to the repository's base +# $1 : Absolute path to the repository's base function prod_tasks_c() { REPO_BASE_DIR="$1" PROD_SRC_DIR=`prod_src_dir $REPO_BASE_DIR` @@ -106,7 +106,7 @@ function prod_tasks_c() { # Returns the absolute path to the directory containing the preprocessing scripts. # # Expected arguments: -# $1 : Absolute path to the repository's base +# $1 : Absolute path to the repository's base function pp_script_dir() { REPO_BASE_DIR="$1" VF_PROOF_DIR=`vf_proof_base_dir $REPO_BASE_DIR` @@ -117,7 +117,7 @@ function pp_script_dir() { # Returns the absolute path to the preprocesor's output direcotry. # # Expected arguments: -# $1 : Absolute path to the repository's base +# $1 : Absolute path to the repository's base function pp_out_dir() { REPO_BASE_DIR="$1" VF_PROOF_DIR=`vf_proof_base_dir $REPO_BASE_DIR` @@ -128,7 +128,7 @@ function pp_out_dir() { # Returns the absolute path to the preprocesor's log direcotry. # # Expected arguments: -# $1 : Absolute path to the repository's base +# $1 : Absolute path to the repository's base function pp_log_dir() { REPO_BASE_DIR="$1" VF_PROOF_DIR=`vf_proof_base_dir $REPO_BASE_DIR` @@ -136,12 +136,12 @@ function pp_log_dir() { echo "$VF_PROOF_DIR/pp_log" } -# Returns the absolute path to the preprocessed version of `tasks.c` containing -# the VeriFast proof annotations. This is the file that is processed by +# Returns the absolute path to the preprocessed version of `tasks.c` containing +# the VeriFast proof annotations. This is the file that is processed by # VeriFast. # # Expected arguments: -# $1 : Absolute path to the repository's base +# $1 : Absolute path to the repository's base function pp_vf_tasks_c() { REPO_BASE_DIR="$1" PP_OUT_DIR=`pp_out_dir $REPO_BASE_DIR` @@ -152,7 +152,7 @@ function pp_vf_tasks_c() { # Returns the absolute path to the preprocessed unmodified version of `tasks.c`. # # Expected arguments: -# $1 : Absolute path to the repository's base +# $1 : Absolute path to the repository's base function pp_prod_tasks_c() { REPO_BASE_DIR="$1" PP_OUT_DIR=`pp_out_dir $REPO_BASE_DIR` @@ -163,7 +163,7 @@ function pp_prod_tasks_c() { # Returns the absolute path to the pico sdk. # # Expected arguments: -# $1 : Absolute path to the repository's base +# $1 : Absolute path to the repository's base function pico_sdk_dir() { REPO_BASE_DIR="$1" VF_PROOF_DIR=`vf_proof_base_dir $REPO_BASE_DIR` @@ -174,7 +174,7 @@ function pico_sdk_dir() { # Returns the absolute path to the smp_demo_dir. # # Expected arguments: -# $1 : Absolute path to the repository's base +# $1 : Absolute path to the repository's base function smp_demo_dir() { REPO_BASE_DIR="$1" VF_PROOF_DIR=`vf_proof_base_dir $REPO_BASE_DIR` @@ -186,7 +186,7 @@ function smp_demo_dir() { # Returns the absolute path to directory where the statistic reports are stored. # # Expected arguments: -# $1 : Absolute path to the repository's base +# $1 : Absolute path to the repository's base function stats_dir() { REPO_BASE_DIR="$1" VF_PROOF_DIR=`vf_proof_base_dir $REPO_BASE_DIR` @@ -194,29 +194,18 @@ function stats_dir() { echo "$VF_PROOF_DIR/stats" } -# Returns the absolute path to diff report. -# -# Expected arguments: -# $1 : Absolute path to the repository's base -function diff_report() { - REPO_BASE_DIR="$1" - STATS_DIR=`stats_dir $REPO_BASE_DIR` - - echo "$STATS_DIR/diff_report.txt" -} - # Ensures that all potentially relevant output direcories exist. # # Expected arguments: -# $1 : Absolute path to the repository's base +# $1 : Absolute path to the repository's base function ensure_output_dirs_exist() { REPO_BASE_DIR="$1" PP_OUT_DIR=`pp_out_dir $REPO_BASE_DIR` STATS_DIR=`stats_dir $REPO_BASE_DIR` PP_LOG_DIR=`pp_log_dir $REPO_BASE_DIR` - + if [ ! -d "$PP_OUT_DIR" ]; then mkdir "$PP_OUT_DIR" fi @@ -227,6 +216,3 @@ function ensure_output_dirs_exist() { mkdir "$PP_LOG_DIR" fi } - - -