From 01c19a2099cd1a3e74fddea57dc5a1a05851e744 Mon Sep 17 00:00:00 2001 From: Tobias Reinhard <16916681+tobireinhard@users.noreply.github.com> Date: Thu, 3 Nov 2022 13:16:10 -0400 Subject: [PATCH] Renamed preprocessed file such that name is legal C identifier. This is necessary for VeriFast to refer to the file as module. --- .../preprocess_tasks_c.sh | 2 +- .../{tasks--pp.c => tasks__pp.c} | 198 +++++++++--------- .../verifast/start-vfide--preprocessed.sh | 2 +- 3 files changed, 101 insertions(+), 101 deletions(-) rename verification/verifast/preprocessed_files/{tasks--pp.c => tasks__pp.c} (99%) diff --git a/verification/verifast/custom_build_scripts_RP2040/preprocess_tasks_c.sh b/verification/verifast/custom_build_scripts_RP2040/preprocess_tasks_c.sh index bb704d43d..445e6ec43 100755 --- a/verification/verifast/custom_build_scripts_RP2040/preprocess_tasks_c.sh +++ b/verification/verifast/custom_build_scripts_RP2040/preprocess_tasks_c.sh @@ -29,7 +29,7 @@ LOG_PP_ERR="$LOG_PP_OUT_DIR/error--$TIMESTAMP.c" LOG_VF_RW_TASK_C="$LOG_PP_OUT_DIR/tasks--vf_rw--$TIMESTAMP.c" PP_OUT_DIR="$VF_PROOF_BASE_DIR/preprocessed_files" -PP_TASK_C="$PP_OUT_DIR/tasks--pp.c" +PP_TASK_C="$PP_OUT_DIR/tasks__pp.c" diff --git a/verification/verifast/preprocessed_files/tasks--pp.c b/verification/verifast/preprocessed_files/tasks__pp.c similarity index 99% rename from verification/verifast/preprocessed_files/tasks--pp.c rename to verification/verifast/preprocessed_files/tasks__pp.c index 9ea6a2c8f..d9c8143b2 100644 --- a/verification/verifast/preprocessed_files/tasks--pp.c +++ b/verification/verifast/preprocessed_files/tasks__pp.c @@ -60,40 +60,40 @@ typedef intptr_t ptrdiff_t; typedef intptr_t ssize_t; // # 5 "/Users/reitobia/programs/verifast-21.04-83-gfae956f7/bin/malloc.h" 2 -/*@ - -// In Standard C, freeing a null pointer is allowed and is a no-op. -lemma_auto void malloc_block_null(); - requires emp; - ensures malloc_block(0, 0); - -lemma void malloc_block_limits(void *array); - requires [?f]malloc_block(array, ?size); - ensures [f]malloc_block(array, size) &*& (void *)0 <= array &*& 0 <= size &*& array + size <= (void *)UINTPTR_MAX; - +/*@ + +// In Standard C, freeing a null pointer is allowed and is a no-op. +lemma_auto void malloc_block_null(); + requires emp; + ensures malloc_block(0, 0); + +lemma void malloc_block_limits(void *array); + requires [?f]malloc_block(array, ?size); + ensures [f]malloc_block(array, size) &*& (void *)0 <= array &*& 0 <= size &*& array + size <= (void *)UINTPTR_MAX; + @*/ void *malloc(size_t size); //@ requires true; - /*@ - ensures - result == 0 ? - emp - : - chars_(result, size, _) &*& malloc_block(result, size) &*& - (char *)0 < result && result + size <= (char *)UINTPTR_MAX; // one-past-end does not overflow + /*@ + ensures + result == 0 ? + emp + : + chars_(result, size, _) &*& malloc_block(result, size) &*& + (char *)0 < result && result + size <= (char *)UINTPTR_MAX; // one-past-end does not overflow @*/ //@ terminates; void *calloc(size_t nmemb, size_t size); //@ requires true; - /*@ - ensures - result == 0 ? - emp - : - chars(result, nmemb * size, ?cs) &*& malloc_block(result, nmemb * size) &*& all_eq(cs, 0) == true &*& - (char *)0 < result && result + nmemb * size <= (char *)UINTPTR_MAX; // one-past-end does not overflow + /*@ + ensures + result == 0 ? + emp + : + chars(result, nmemb * size, ?cs) &*& malloc_block(result, nmemb * size) &*& all_eq(cs, 0) == true &*& + (char *)0 < result && result + nmemb * size <= (char *)UINTPTR_MAX; // one-past-end does not overflow @*/ //@ terminates; @@ -104,16 +104,16 @@ void free(void *array); void *realloc(void *array, size_t newSize); //@ requires malloc_block(array, ?size) &*& chars(array, size, ?cs); - /*@ - ensures - result == 0 ? - malloc_block(array, size) &*& chars(array, size, cs) - : - malloc_block(result, newSize) &*& - newSize <= size ? - chars(result, _, take(newSize, cs)) - : - chars(result, _, cs) &*& chars(result + size, newSize - size, _); + /*@ + ensures + result == 0 ? + malloc_block(array, size) &*& chars(array, size, cs) + : + malloc_block(result, newSize) &*& + newSize <= size ? + chars(result, _, take(newSize, cs)) + : + chars(result, _, cs) &*& chars(result + size, newSize - size, _); @*/ //@ terminates; // # 6 "/Users/reitobia/programs/verifast-21.04-83-gfae956f7/bin/stdlib.h" 2 @@ -158,21 +158,21 @@ void memcpy(void *array, void *array0, size_t count); //@ ensures chars(array, count, cs0) &*& [f]chars(array0, count, cs0); void memmove(void *dest, void *src, size_t count); - /*@ - requires - chars(src, count, ?cs) &*& - dest <= src ? - chars(dest, src - dest, _) - : - chars(src + count, dest - src, _); + /*@ + requires + chars(src, count, ?cs) &*& + dest <= src ? + chars(dest, src - dest, _) + : + chars(src + count, dest - src, _); @*/ - /*@ - ensures - chars(dest, count, cs) &*& - dest <= src ? - chars(dest + count, src - dest, _) - : - chars(src, dest - src, _); + /*@ + ensures + chars(dest, count, cs) &*& + dest <= src ? + chars(dest + count, src - dest, _) + : + chars(src, dest - src, _); @*/ size_t strlen(char *string); @@ -193,15 +193,15 @@ char *memchr(char *array, char c, size_t count); char* strchr(char *str, char c); //@ requires [?f]string(str, ?cs); - /*@ ensures - [f]string(str, cs) &*& - c == 0 ? - result == str + length(cs) - : - result == 0 ? - mem(c, cs) == false - : - mem(c, cs) == true &*& result == str + index_of(c, cs); + /*@ ensures + [f]string(str, cs) &*& + c == 0 ? + result == str + length(cs) + : + result == 0 ? + mem(c, cs) == false + : + mem(c, cs) == true &*& result == str + index_of(c, cs); @*/ void* memset(void *array, char value, size_t size); @@ -548,33 +548,33 @@ typedef void (* TaskFunction_t)( void * ); * must be set in the compiler's include path. */ // # 1 "/Users/reitobia/repos2/FreeRTOS-Kernel/portable/ThirdParty/GCC/RP2040/include/portmacro.h" 1 -/* - * FreeRTOS SMP Kernel V202110.00 - * Copyright (C) 2020 Amazon.com, Inc. or its affiliates. All Rights Reserved. - * Copyright (c) 2021 Raspberry Pi (Trading) Ltd. - * - * SPDX-License-Identifier: MIT AND BSD-3-Clause - * - * Permission is hereby granted, free of charge, to any person obtaining a copy of - * this software and associated documentation files (the "Software"), to deal in - * the Software without restriction, including without limitation the rights to - * use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of - * the Software, and to permit persons to whom the Software is furnished to do so, - * subject to the following conditions: - * - * The above copyright notice and this permission notice shall be included in all - * copies or substantial portions of the Software. - * - * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR - * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS - * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR - * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER - * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN - * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. - * - * https://www.FreeRTOS.org - * https://github.com/FreeRTOS - * +/* + * FreeRTOS SMP Kernel V202110.00 + * Copyright (C) 2020 Amazon.com, Inc. or its affiliates. All Rights Reserved. + * Copyright (c) 2021 Raspberry Pi (Trading) Ltd. + * + * SPDX-License-Identifier: MIT AND BSD-3-Clause + * + * Permission is hereby granted, free of charge, to any person obtaining a copy of + * this software and associated documentation files (the "Software"), to deal in + * the Software without restriction, including without limitation the rights to + * use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of + * the Software, and to permit persons to whom the Software is furnished to do so, + * subject to the following conditions: + * + * The above copyright notice and this permission notice shall be included in all + * copies or substantial portions of the Software. + * + * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS + * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR + * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER + * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN + * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. + * + * https://www.FreeRTOS.org + * https://github.com/FreeRTOS + * */ // # 37 "/Users/reitobia/repos2/FreeRTOS-Kernel/portable/ThirdParty/GCC/RP2040/include/portmacro.h" // # 1 "/Users/reitobia/repos2/FreeRTOS-Kernel/verification/verifast/sdks/pico-sdk/src/common/pico_base/include/pico.h" 1 @@ -4283,14 +4283,14 @@ int spin_lock_claim_unused(bool required); bool spin_lock_is_claimed(uint lock_num); // # 39 "/Users/reitobia/repos2/FreeRTOS-Kernel/portable/ThirdParty/GCC/RP2040/include/portmacro.h" 2 -/*----------------------------------------------------------- - * Port specific definitions. - * - * The settings in this file configure FreeRTOS correctly for the - * given hardware and compiler. - * - * These settings should not be altered. - *----------------------------------------------------------- +/*----------------------------------------------------------- + * Port specific definitions. + * + * The settings in this file configure FreeRTOS correctly for the + * given hardware and compiler. + * + * These settings should not be altered. + *----------------------------------------------------------- */ /* Type definitions. */ @@ -4306,7 +4306,7 @@ bool spin_lock_is_claimed(uint lock_num); typedef uint32_t TickType_t; -/* 32-bit tick type on a 32-bit architecture, so reads of the tick count do +/* 32-bit tick type on a 32-bit architecture, so reads of the tick count do * not need to be guarded with a critical section. */ @@ -4317,13 +4317,13 @@ bool spin_lock_is_claimed(uint lock_num); - /* Reason for rewrite: VeriFast does not support the attriibute `used`. + /* Reason for rewrite: VeriFast does not support the attriibute `used`. */ - /* We have to use PICO_DIVIDER_DISABLE_INTERRUPTS as the source of truth rathern than our config, + /* We have to use PICO_DIVIDER_DISABLE_INTERRUPTS as the source of truth rathern than our config, * as our FreeRTOSConfig.h header cannot be included by ASM code - which is what this affects in the SDK */ @@ -4388,11 +4388,11 @@ bool spin_lock_is_claimed(uint lock_num); - /* Note this is a single method with uxAcquire parameter since we have - * static vars, the method is always called with a compile time constant for + /* Note this is a single method with uxAcquire parameter since we have + * static vars, the method is always called with a compile time constant for * uxAcquire, and the compiler should dothe right thing! */ - /* Reason for rewrite: VeriFast does not support local static variables. + /* Reason for rewrite: VeriFast does not support local static variables. */ // # 226 "/Users/reitobia/repos2/FreeRTOS-Kernel/portable/ThirdParty/GCC/RP2040/include/portmacro.h" /*-----------------------------------------------------------*/ diff --git a/verification/verifast/start-vfide--preprocessed.sh b/verification/verifast/start-vfide--preprocessed.sh index 59c16dfdb..de71a2bf1 100755 --- a/verification/verifast/start-vfide--preprocessed.sh +++ b/verification/verifast/start-vfide--preprocessed.sh @@ -11,7 +11,7 @@ echo Path to vfide binary : "\'$VFIDE\'" START_WD=`pwd` PP_SCRIPT_DIR="$START_WD/custom_build_scripts_RP2040" PP_SCRIPT="./preprocess_tasks_c.sh" -PP_TASK_C="$START_WD/preprocessed_files/tasks--pp.c" +PP_TASK_C="$START_WD/preprocessed_files/tasks__pp.c" FONT_SIZE=16