diff options
Diffstat (limited to 'FreeRTOS/Test/VeriFast/scripts/generate_diff_files.sh')
-rwxr-xr-x | FreeRTOS/Test/VeriFast/scripts/generate_diff_files.sh | 47 |
1 files changed, 47 insertions, 0 deletions
diff --git a/FreeRTOS/Test/VeriFast/scripts/generate_diff_files.sh b/FreeRTOS/Test/VeriFast/scripts/generate_diff_files.sh new file mode 100755 index 000000000..55f9cfbd2 --- /dev/null +++ b/FreeRTOS/Test/VeriFast/scripts/generate_diff_files.sh @@ -0,0 +1,47 @@ +#!/bin/bash -eu + +FUNCS=( + prvCopyDataFromQueue + prvCopyDataToQueue + prvInitialiseNewQueue + prvIsQueueEmpty + prvIsQueueFull + prvUnlockQueue + uxQueueMessagesWaiting + uxQueueSpacesAvailable + vQueueDelete + xQueueGenericCreate + xQueueGenericReset + xQueueGenericSend + xQueueGenericSendFromISR + xQueueIsQueueEmptyFromISR + xQueueIsQueueFullFromISR + xQueuePeek + xQueuePeekFromISR + xQueueReceive + xQueueReceiveFromISR +) + +if [ ! -d "FreeRTOS-Kernel" ]; then + git clone https://github.com/FreeRTOS/FreeRTOS-Kernel.git +fi +pushd FreeRTOS-Kernel > /dev/null +rm -rf tags generated +ctags --excmd=number queue.c +mkdir generated +for f in ${FUNCS[@]}; do + ../extract.py tags $f > generated/$f.c +done +popd > /dev/null +echo "created: FreeRTOS-Kernel/generated" + +ln -fs ../queue . +pushd queue > /dev/null +rm -rf tags generated +ctags --excmd=number *.c +mkdir generated +for f in ${FUNCS[@]}; do + ../scripts/extract.py tags $f > generated/$f.c +done +popd > /dev/null +echo "created: queue/generated" |