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

Diff script now writes diff to stdout instead of file. Script returns error code if the diff is not empty.

Browse source
This commit is contained in:
Tobias Reinhard 2022-12-22 09:25:24 -05:00
parent 3ca111bbbc
commit 4a7c975cf8
2 changed files with 25 additions and 42 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -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_PROD_TASKS_C=`pp_prod_tasks_c $REPO_BASE_DIR`
PP_VF_TASKS_C=`pp_vf_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 ensure_output_dirs_exist $REPO_BASE_DIR
echo preprocessing production version of 'tasks.c' 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 $REPO_BASE_DIR $VF_PROOF_BASE_DIR
echo Computing diff. Report written to: echo Computing diff:
echo \"$DIFF_REPORT\" echo
git diff --no-index --ignore-all-space $PP_PROD_TASKS_C $PP_VF_TASKS_C \ git diff --no-index --ignore-all-space $PP_PROD_TASKS_C $PP_VF_TASKS_C
> "$DIFF_REPORT"

14
Test/VeriFast/tasks/vTaskSwitchContext/paths.sh
View file

@ -194,17 +194,6 @@ function stats_dir() {
echo "$VF_PROOF_DIR/stats" 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. # Ensures that all potentially relevant output direcories exist.
# #
@ -227,6 +216,3 @@ function ensure_output_dirs_exist() {
mkdir "$PP_LOG_DIR" mkdir "$PP_LOG_DIR"
fi fi
} }