diff --git a/verification/verifast/preprocessed_files/tasks--pp.c b/verification/verifast/preprocessed_files/tasks--pp.c index d8b060f4e..d7bd2b194 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" /*-----------------------------------------------------------*/ @@ -9975,10 +9975,13 @@ predicate stack_p_2(StackType_t * pxStack, // Used stack cells integers_(pxTopOfStack + 1, sizeof(StackType_t), false, ulUsedCells, _) &*& // Unaligned rest - //unalignedRestOfStack_p((char*) pxStack + freeBytes, ulUsedCells, ulUnalignedBytes); - true; - + //unalignedRestOfStack_p(pxTopOfStack, ulUsedCells, ulUnalignedBytes); + true; // skip unaligned part for now +predicate unalignedRestOfStack_p(StackType_t * pxTopOfStack, + uint32_t ulUsedCells, + uint32_t ulUnalignedBytes) = + chars((char*) pxTopOfStack + sizeof(StackType_t) * (ulUsedCells + 1), ulUnalignedBytes, _); @*/ /*@ @@ -10417,17 +10420,16 @@ StackType_t * pxPortInitialiseStack( StackType_t * pxTopOfStack, ulFreeBytes > 17 * sizeof(StackType_t) &*& pxStack > 0; @*/ -/*@ ensures stack_p_2(pxStack, ulStackDepth, pxTopOfStack, ulFreeBytes, - ulUsedCells, ulUnalignedBytes); +/*@ ensures stack_p_2(pxStack, ulStackDepth, pxTopOfStack - 16, ulFreeBytes - sizeof(StackType_t) * 16, ulUsedCells + 16, ulUnalignedBytes); @*/ { //@ StackType_t* gOldTop = pxTopOfStack; //@ char* gcStack = (char*) pxStack; //@ open stack_p_2(_, _, _, _, _, _); - + //@ assert( (char*) pxTopOfStack == (char*) pxStack + ulFreeBytes - sizeof(StackType_t) ); //@ assert( (char*) pxStack + ulFreeBytes == (char*) pxTopOfStack + sizeof(StackType_t) ); - + // skip stack cell #0 //@ chars_split(gcStack, ulFreeBytes - sizeof(StackType_t)); //@ chars_to_integers_(gOldTop, sizeof(StackType_t), false, 1); @@ -10435,14 +10437,14 @@ StackType_t * pxPortInitialiseStack( StackType_t * pxTopOfStack, /* Simulate the stack frame as it would be created by a context switch * interrupt. */ pxTopOfStack--; /* Offset added to account for the way the MCU uses the stack on entry/exit of interrupts. */ - + // Ensure maintining stack invariant //@ close stack_p_2(pxStack, ulStackDepth, pxTopOfStack, ulFreeBytes - sizeof(StackType_t) * 1, ulUsedCells + 1, ulUnalignedBytes); //@ open stack_p_2(pxStack, _, _, _, _, _); - + //@ assert( (char*) pxTopOfStack == (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 2) ); //@ assert( (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 1) == (char*) pxTopOfStack + sizeof(StackType_t) ); - + // make stack cell #1 available //@ chars_split(gcStack, ulFreeBytes - (sizeof(StackType_t) * 2)); //@ chars_to_integers_(gOldTop-1, sizeof(StackType_t), false, 1); @@ -10450,14 +10452,14 @@ StackType_t * pxPortInitialiseStack( StackType_t * pxTopOfStack, *pxTopOfStack = ( 0x01000000 ); /* xPSR */ //@ close integers_(gOldTop-1, sizeof(StackType_t), false, ulUsedCells+2, _); pxTopOfStack--; - + // Ensure maintining stack invariant //@ close stack_p_2(pxStack, ulStackDepth, pxTopOfStack, ulFreeBytes - sizeof(StackType_t) * 2, ulUsedCells + 2, ulUnalignedBytes); //@ open stack_p_2(pxStack, _, _, _, _, _); - + //@ assert( (char*) pxTopOfStack == (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 3) ); //@ assert( (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 2) == (char*) pxTopOfStack + sizeof(StackType_t) ); - + // prevent overflow //@ ptr_range(pxCode); // make stack cell #2 available @@ -10467,14 +10469,14 @@ StackType_t * pxPortInitialiseStack( StackType_t * pxTopOfStack, *pxTopOfStack = ( StackType_t ) pxCode; /* PC */ //@ close integers_(gOldTop-2, sizeof(StackType_t), false, ulUsedCells+3, _); pxTopOfStack--; - + // Ensure maintining stack invariant //@ close stack_p_2(pxStack, ulStackDepth, pxTopOfStack, ulFreeBytes - sizeof(StackType_t) * 3, ulUsedCells + 3, ulUnalignedBytes); //@ open stack_p_2(pxStack, _, _, _, _, _); - + //@ assert( (char*) pxTopOfStack == (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 4) ); //@ assert( (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 3) == (char*) pxTopOfStack + sizeof(StackType_t) ); - + // prevent underflow //@ ptr_range(prvTaskExitError); // make stack cell #3 available @@ -10483,40 +10485,49 @@ StackType_t * pxPortInitialiseStack( StackType_t * pxTopOfStack, //@ integers__join(gOldTop-3); *pxTopOfStack = ( StackType_t ) prvTaskExitError; /* LR */ //@ close integers_(gOldTop-3, sizeof(StackType_t), false, ulUsedCells+4, _); - + pxTopOfStack -= 5; /* R12, R3, R2 and R1. */ - + + // jump to stack cell #7 + //@ chars_split(gcStack, ulFreeBytes - (sizeof(StackType_t) * 8)); + //@ chars_to_integers_(gOldTop-7, sizeof(StackType_t), false, 4); + //@ integers__join(gOldTop-7); + // Ensure maintining stack invariant //@ close stack_p_2(pxStack, ulStackDepth, pxTopOfStack, ulFreeBytes - sizeof(StackType_t) * 8, ulUsedCells + 8, ulUnalignedBytes); //@ open stack_p_2(pxStack, _, _, _, _, _); - + //@ assert( (char*) pxTopOfStack == (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 9) ); //@ assert( (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 8) == (char*) pxTopOfStack + sizeof(StackType_t) ); - + // prevent overflow //@ ptr_range(pvParameters); + // make stack cell #8 available //@ chars_split(gcStack, ulFreeBytes - (sizeof(StackType_t) * 9)); - //@ chars_to_integers_(gOldTop-8, sizeof(StackType_t), false, 5); + //@ chars_to_integers_(gOldTop-8, sizeof(StackType_t), false, 1); //@ integers__join(gOldTop-8); *pxTopOfStack = ( StackType_t ) pvParameters; /* R0 */ //@ close integers_(gOldTop-8, sizeof(StackType_t), false, ulUsedCells+9, _); - - + + // Ensure maintining stack invariant + //@ close stack_p_2(pxStack, ulStackDepth, pxTopOfStack-1, ulFreeBytes - sizeof(StackType_t) * 9, ulUsedCells + 9, ulUnalignedBytes); + //@ open stack_p_2(pxStack, _, _, _, _, _); + + // skip stack cells #9 - #15, leave #16 unused - //@ chars_split(gcStack, ulFreeBytes - (sizeof(StackType_t) * 17)); - //@ chars_to_integers_(gOldTop-16, sizeof(StackType_t), false, 8); - //@ integers__join(gOldTop-16); + //@ chars_split(gcStack, ulFreeBytes - (sizeof(StackType_t) * 16)); + //@ chars_to_integers_(gOldTop-15, sizeof(StackType_t), false, 7); + //@ integers__join(gOldTop-15); pxTopOfStack -= 8; /* R11..R4. */ - + + // Ensure maintining stack invariant + //@ close stack_p_2(pxStack, ulStackDepth, pxTopOfStack, ulFreeBytes - sizeof(StackType_t) * 16, ulUsedCells + 16, ulUnalignedBytes); + //@ assert( stack_p_2(pxStack, ulStackDepth, gOldTop-16, ulFreeBytes - sizeof(StackType_t) * 16, ulUsedCells + 16, ulUnalignedBytes) ); + //@ assert( (char*) pxTopOfStack == (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 17) ); //@ assert( (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 16) == (char*) pxTopOfStack + sizeof(StackType_t) ); - - - - - //@close stack_p_2(pxStack, ulStackDepth, pxTopOfStack, ulFreeBytes - (sizeof(StackType_t) * 16), ulUsedCells, ulUnalignedBytes); - + return pxTopOfStack; } // # 66 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" 2 diff --git a/verification/verifast/proof/snippets/rp2040_port_c_snippets.c b/verification/verifast/proof/snippets/rp2040_port_c_snippets.c index 6c2789141..030e9e318 100644 --- a/verification/verifast/proof/snippets/rp2040_port_c_snippets.c +++ b/verification/verifast/proof/snippets/rp2040_port_c_snippets.c @@ -117,17 +117,16 @@ StackType_t * pxPortInitialiseStack( StackType_t * pxTopOfStack, ulFreeBytes > 17 * sizeof(StackType_t) &*& pxStack > 0; @*/ -/*@ ensures stack_p_2(pxStack, ulStackDepth, pxTopOfStack, ulFreeBytes, - ulUsedCells, ulUnalignedBytes); +/*@ ensures stack_p_2(pxStack, ulStackDepth, pxTopOfStack - 16, ulFreeBytes - sizeof(StackType_t) * 16, ulUsedCells + 16, ulUnalignedBytes); @*/ { //@ StackType_t* gOldTop = pxTopOfStack; //@ char* gcStack = (char*) pxStack; //@ open stack_p_2(_, _, _, _, _, _); - + //@ assert( (char*) pxTopOfStack == (char*) pxStack + ulFreeBytes - sizeof(StackType_t) ); //@ assert( (char*) pxStack + ulFreeBytes == (char*) pxTopOfStack + sizeof(StackType_t) ); - + // skip stack cell #0 //@ chars_split(gcStack, ulFreeBytes - sizeof(StackType_t)); //@ chars_to_integers_(gOldTop, sizeof(StackType_t), false, 1); @@ -135,14 +134,14 @@ StackType_t * pxPortInitialiseStack( StackType_t * pxTopOfStack, /* Simulate the stack frame as it would be created by a context switch * interrupt. */ pxTopOfStack--; /* Offset added to account for the way the MCU uses the stack on entry/exit of interrupts. */ - + // Ensure maintining stack invariant //@ close stack_p_2(pxStack, ulStackDepth, pxTopOfStack, ulFreeBytes - sizeof(StackType_t) * 1, ulUsedCells + 1, ulUnalignedBytes); //@ open stack_p_2(pxStack, _, _, _, _, _); - + //@ assert( (char*) pxTopOfStack == (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 2) ); //@ assert( (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 1) == (char*) pxTopOfStack + sizeof(StackType_t) ); - + // make stack cell #1 available //@ chars_split(gcStack, ulFreeBytes - (sizeof(StackType_t) * 2)); //@ chars_to_integers_(gOldTop-1, sizeof(StackType_t), false, 1); @@ -150,14 +149,14 @@ StackType_t * pxPortInitialiseStack( StackType_t * pxTopOfStack, *pxTopOfStack = ( 0x01000000 ); /* xPSR */ //@ close integers_(gOldTop-1, sizeof(StackType_t), false, ulUsedCells+2, _); pxTopOfStack--; - + // Ensure maintining stack invariant //@ close stack_p_2(pxStack, ulStackDepth, pxTopOfStack, ulFreeBytes - sizeof(StackType_t) * 2, ulUsedCells + 2, ulUnalignedBytes); //@ open stack_p_2(pxStack, _, _, _, _, _); - + //@ assert( (char*) pxTopOfStack == (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 3) ); //@ assert( (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 2) == (char*) pxTopOfStack + sizeof(StackType_t) ); - + // prevent overflow //@ ptr_range(pxCode); // make stack cell #2 available @@ -167,14 +166,14 @@ StackType_t * pxPortInitialiseStack( StackType_t * pxTopOfStack, *pxTopOfStack = ( StackType_t ) pxCode; /* PC */ //@ close integers_(gOldTop-2, sizeof(StackType_t), false, ulUsedCells+3, _); pxTopOfStack--; - + // Ensure maintining stack invariant //@ close stack_p_2(pxStack, ulStackDepth, pxTopOfStack, ulFreeBytes - sizeof(StackType_t) * 3, ulUsedCells + 3, ulUnalignedBytes); //@ open stack_p_2(pxStack, _, _, _, _, _); - + //@ assert( (char*) pxTopOfStack == (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 4) ); //@ assert( (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 3) == (char*) pxTopOfStack + sizeof(StackType_t) ); - + // prevent underflow //@ ptr_range(prvTaskExitError); // make stack cell #3 available @@ -183,39 +182,48 @@ StackType_t * pxPortInitialiseStack( StackType_t * pxTopOfStack, //@ integers__join(gOldTop-3); *pxTopOfStack = ( StackType_t ) prvTaskExitError; /* LR */ //@ close integers_(gOldTop-3, sizeof(StackType_t), false, ulUsedCells+4, _); - + pxTopOfStack -= 5; /* R12, R3, R2 and R1. */ + // jump to stack cell #7 + //@ chars_split(gcStack, ulFreeBytes - (sizeof(StackType_t) * 8)); + //@ chars_to_integers_(gOldTop-7, sizeof(StackType_t), false, 4); + //@ integers__join(gOldTop-7); + // Ensure maintining stack invariant //@ close stack_p_2(pxStack, ulStackDepth, pxTopOfStack, ulFreeBytes - sizeof(StackType_t) * 8, ulUsedCells + 8, ulUnalignedBytes); //@ open stack_p_2(pxStack, _, _, _, _, _); - + //@ assert( (char*) pxTopOfStack == (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 9) ); //@ assert( (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 8) == (char*) pxTopOfStack + sizeof(StackType_t) ); - + // prevent overflow //@ ptr_range(pvParameters); + // make stack cell #8 available //@ chars_split(gcStack, ulFreeBytes - (sizeof(StackType_t) * 9)); - //@ chars_to_integers_(gOldTop-8, sizeof(StackType_t), false, 5); + //@ chars_to_integers_(gOldTop-8, sizeof(StackType_t), false, 1); //@ integers__join(gOldTop-8); *pxTopOfStack = ( StackType_t ) pvParameters; /* R0 */ //@ close integers_(gOldTop-8, sizeof(StackType_t), false, ulUsedCells+9, _); - + // Ensure maintining stack invariant + //@ close stack_p_2(pxStack, ulStackDepth, pxTopOfStack-1, ulFreeBytes - sizeof(StackType_t) * 9, ulUsedCells + 9, ulUnalignedBytes); + //@ open stack_p_2(pxStack, _, _, _, _, _); + + // skip stack cells #9 - #15, leave #16 unused - //@ chars_split(gcStack, ulFreeBytes - (sizeof(StackType_t) * 17)); - //@ chars_to_integers_(gOldTop-16, sizeof(StackType_t), false, 8); - //@ integers__join(gOldTop-16); + //@ chars_split(gcStack, ulFreeBytes - (sizeof(StackType_t) * 16)); + //@ chars_to_integers_(gOldTop-15, sizeof(StackType_t), false, 7); + //@ integers__join(gOldTop-15); pxTopOfStack -= 8; /* R11..R4. */ + // Ensure maintining stack invariant + //@ close stack_p_2(pxStack, ulStackDepth, pxTopOfStack, ulFreeBytes - sizeof(StackType_t) * 16, ulUsedCells + 16, ulUnalignedBytes); + //@ assert( stack_p_2(pxStack, ulStackDepth, gOldTop-16, ulFreeBytes - sizeof(StackType_t) * 16, ulUsedCells + 16, ulUnalignedBytes) ); + //@ assert( (char*) pxTopOfStack == (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 17) ); //@ assert( (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 16) == (char*) pxTopOfStack + sizeof(StackType_t) ); - - - - - //@close stack_p_2(pxStack, ulStackDepth, pxTopOfStack, ulFreeBytes - (sizeof(StackType_t) * 16), ulUsedCells, ulUnalignedBytes); - + return pxTopOfStack; } \ No newline at end of file