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

Moved pragma rewrites to vf_rewrites.sh.

Browse source
This commit is contained in:
Tobias Reinhard 2022-10-14 16:41:48 -04:00
parent 8ca47345d4
commit e9302f35ac
2 changed files with 29 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

9
verification/verifast/custom_build_scripts_RP2040/preprocess_tasks_c.sh
View file

@ -8,7 +8,6 @@ DEMO_DIR="$PP_SCRIPT_WD/../FreeRTOS/Demo/CORTEX_M0+_RP2040/"
TIMESTAMP=`date +'%y_%m_%d--%H_%M'`
LOG_PP_OUT_DIR="$PP_SCRIPT_WD/log_preprocessed_files"
LOG_PP_TASK_C="$LOG_PP_OUT_DIR/tasks--pp--$TIMESTAMP.c"
LOG_PP_TASK_C_PRAGMA_COMMENTS="$LOG_PP_OUT_DIR/tasks--pp--pragma_comments--$TIMESTAMP.c"
LOG_VF_RW_TASK_C="$LOG_PP_OUT_DIR/tasks--vf_rw--$TIMESTAMP.c"
@ -30,15 +29,9 @@ echo "\n\nPreprocessed output with pragmas written to:"
echo $LOG_PP_TASK_C
sed 's|^#|// &|g' $LOG_PP_TASK_C > $LOG_PP_TASK_C_PRAGMA_COMMENTS
echo "\n\nPreprocessed output with pragma comments written to:"
echo $LOG_PP_TASK_C_PRAGMA_COMMENTS
echo "\n\nApplying VeriFast rewrites. Result written to:"
echo $LOG_VF_RW_TASK_C
cp "$LOG_PP_TASK_C_PRAGMA_COMMENTS" "$LOG_VF_RW_TASK_C"
cp "$LOG_PP_TASK_C" "$LOG_VF_RW_TASK_C"
./vf_rewrite.sh "$LOG_VF_RW_TASK_C"

30
verification/verifast/custom_build_scripts_RP2040/vf_rewrite.sh
View file

@ -4,9 +4,31 @@ VF_RW_WD=`pwd`
SOURCE_FILE="$1"
BACKUP_IDX=0
echo "VF RW: 'long unsigned int' -> 'unsinged long int'"
# IMPORTANT:
# None of the provided regexes must contain the unescaped character '|'
#
# $1 : sed 'find' regex
# $2 : sed 'replace' regex
rewrite()
{
FIND_REGEX=$1
REPLACE_REGEX=$2
echo "VF RW: \"$FIND_REGEX\" -> \"$REPLACE_REGEX\""
echo "backup : $VF_RW_WD/$SOURCE_FILE.backup-$BACKUP_IDX"
echo backup index $BACKUP_IDX
sed -i."backup-$BACKUP_IDX" 's|long unsigned int|unsigned long int|g' $SOURCE_FILE
sed -i."backup-$BACKUP_IDX" "s|$FIND_REGEX|$REPLACE_REGEX|g" $SOURCE_FILE
((BACKUP_IDX=BACKUP_IDX+1))
echo backup index $BACKUP_IDX
echo "\n"
}
echo "Commenting out line/file pragmas"
rewrite "^#" "// &"
rewrite "long unsigned int" "unsigned long int"
#echo "VF RW: 'long unsigned int' -> 'unsinged long int'"
#echo "backup : $VF_RW_WD/$SOURCE_FILE.backup-$BACKUP_IDX"
#echo backup index $BACKUP_IDX
#sed -i."backup-$BACKUP_IDX" 's|long unsigned int|unsigned long int|g' $SOURCE_FILE
#((BACKUP_IDX=BACKUP_IDX+1))
#echo backup index $BACKUP_IDX