mirror of
https://github.com/FreeRTOS/FreeRTOS-Kernel.git
synced 2025-12-12 22:55:07 -05:00
Renamed preprocessed file such that name is legal C identifier.
This is necessary for VeriFast to refer to the file as module.
This commit is contained in:
Tobias Reinhard
parent
e064c380d7
commit
01c19a2099
3 changed files with 101 additions and 101 deletions
|
|
@ -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"
|
||||
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -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"
|
||||
/*-----------------------------------------------------------*/
|
||||
|
|
@ -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
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue