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

Stored pp script args in diff script in variables to improve readability.

Browse source
This commit is contained in:
Tobias Reinhard 2022-12-12 08:26:42 -05:00
parent f56d20b543
commit 2ae20ff48d
1 changed files with 20 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

34
Test/VeriFast/tasks/vTaskSwitchContext/diff.sh
View file

@ -18,24 +18,30 @@ VF_PROOF_BASE_DIR=`vf_proof_base_dir $REPO_BASE_DIR`
. "$PREFIX/paths.sh" . "$PREFIX/paths.sh"
VF_PROOF_DIR=`vf_proof_base_dir $REPO_BASE_DIR` VF_PROOF_DIR=`vf_proof_base_dir $REPO_BASE_DIR`
PP_SCRIPT_DIR=`pp_script_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`
# Unpreprocessed verions of tasks.c
PROD_TASKS_C=`prod_tasks_c $REPO_BASE_DIR`
VF_TASKS_C=`vf_annotated_tasks_c $REPO_BASE_DIR`
# Preprocessed versions of tasks.c
PP_PROD_TASKS_C=`pp_prod_tasks_c $REPO_BASE_DIR`
PP_VF_TASKS_C=`pp_vf_tasks_c $REPO_BASE_DIR`
echo PP_SCRIPT_DIR:
echo $PP_SCRIPT_DIR
echo preprocessing production version of 'tasks.c' echo preprocessing production version of 'tasks.c'
"$PP_SCRIPT_DIR/preprocess_file_for_diff.sh" \ $PP $PROD_TASKS_C $PP_PROD_TASKS_C \
`prod_tasks_c $REPO_BASE_DIR` \ "$LOG_DIR/err1.txt" \
`pp_prod_tasks_c $REPO_BASE_DIR` \ $REPO_BASE_DIR $VF_PROOF_BASE_DIR
"`pp_log_dir $REPO_BASE_DIR`/err1.txt" \
$REPO_BASE_DIR \
$VF_PROOF_BASE_DIR
echo preprocessing verified version of 'tasks.c' echo preprocessing verified version of 'tasks.c'
"$PP_SCRIPT_DIR/preprocess_file_for_diff.sh" \ $PP $VF_TASKS_C $PP_VF_TASKS_C \
`vf_annotated_tasks_c $REPO_BASE_DIR` \ "$LOG_DIR/err2.txt" \
`pp_vf_tasks_c $REPO_BASE_DIR` \ $REPO_BASE_DIR $VF_PROOF_BASE_DIR
"`pp_log_dir $REPO_BASE_DIR`/err2.txt" \
$REPO_BASE_DIR \
$VF_PROOF_BASE_DIR
# pp script args # pp script args
# SRC_FILE="$1" # SRC_FILE="$1"
@ -50,4 +56,4 @@ printf "\n\n\n"
echo Diff: echo Diff:
echo ----------------------------------------------------- echo -----------------------------------------------------
echo echo
git diff --no-index "`pp_log_dir $REPO_BASE_DIR`/err1.txt" `pp_vf_tasks_c $REPO_BASE_DIR` git diff --no-index --ignore-all-space $PP_PROD_TASKS_C $PP_VF_TASKS_C