diff --git a/FreeRTOS/Source b/FreeRTOS/Source index 95433d0284..b08c19f745 160000 --- a/FreeRTOS/Source +++ b/FreeRTOS/Source @@ -1 +1 @@ -Subproject commit 95433d02848af0d274648ae4cdd846f6eff76dde +Subproject commit b08c19f74560dc8885eaf04c47483817d28e13e2 diff --git a/FreeRTOS/Test/CBMC/patches/0005-Remove-volatile-qualifier-from-tasks-variables.patch b/FreeRTOS/Test/CBMC/patches/0005-Remove-volatile-qualifier-from-tasks-variables.patch index 7eb4870a07..58fcae48dd 100644 --- a/FreeRTOS/Test/CBMC/patches/0005-Remove-volatile-qualifier-from-tasks-variables.patch +++ b/FreeRTOS/Test/CBMC/patches/0005-Remove-volatile-qualifier-from-tasks-variables.patch @@ -40,21 +40,20 @@ Here, `uxPendedTicks` could return any value, making it impossible to unwind (or unroll) this loop in CBMC. Therefore, we require `uxPendedTicks` to behave as a regular variable so that the loop can be unwound. ---- diff --git a/FreeRTOS/Source/tasks.c b/FreeRTOS/Source/tasks.c -index ff657733..8b57d198 100644 +index c7be57cb2..9f76465d5 100644 --- a/FreeRTOS/Source/tasks.c +++ b/FreeRTOS/Source/tasks.c -@@ -335,7 +335,7 @@ typedef tskTCB TCB_t; +@@ -296,7 +296,7 @@ typedef struct tskTaskControlBlock /* The old naming convention is used to - /*lint -save -e956 A manual analysis and inspection has been used to determine - * which static variables must be declared volatile. */ --PRIVILEGED_DATA TCB_t * volatile pxCurrentTCB = NULL; -+PRIVILEGED_DATA TCB_t * pxCurrentTCB = NULL; - - /* Lists for ready and blocked tasks. -------------------- - * xDelayedTaskList1 and xDelayedTaskList2 could be move to function scople but -@@ -344,8 +344,8 @@ PRIVILEGED_DATA TCB_t * volatile pxCurrentTCB = NULL; + #if ( configUSE_NEWLIB_REENTRANT == 1 ) + /* Allocate a Newlib reent structure that is specific to this task. +- * Note Newlib support has been included by popular demand, but is not ++ Note Newlib support has been included by popular demand, but is not + * used by the FreeRTOS maintainers themselves. FreeRTOS is not + * responsible for resulting newlib operation. User must be familiar with + * newlib and must provide system-wide implementations of the necessary +@@ -343,8 +343,8 @@ PRIVILEGED_DATA TCB_t * volatile pxCurrentTCB = NULL; PRIVILEGED_DATA static List_t pxReadyTasksLists[ configMAX_PRIORITIES ]; /*< Prioritised ready tasks. */ PRIVILEGED_DATA static List_t xDelayedTaskList1; /*< Delayed tasks. */ PRIVILEGED_DATA static List_t xDelayedTaskList2; /*< Delayed tasks (two lists are used - one for delays that have overflowed the current tick count. */ @@ -65,7 +64,7 @@ index ff657733..8b57d198 100644 PRIVILEGED_DATA static List_t xPendingReadyList; /*< Tasks that have been readied while the scheduler was suspended. They will be moved to the ready list when the scheduler is resumed. */ #if ( INCLUDE_vTaskDelete == 1 ) -@@ -372,7 +372,7 @@ PRIVILEGED_DATA static volatile UBaseType_t uxCurrentNumberOfTasks = ( UBaseType +@@ -371,7 +371,7 @@ PRIVILEGED_DATA static volatile UBaseType_t uxCurrentNumberOfTasks = ( UBaseType PRIVILEGED_DATA static volatile TickType_t xTickCount = ( TickType_t ) configINITIAL_TICK_COUNT; PRIVILEGED_DATA static volatile UBaseType_t uxTopReadyPriority = tskIDLE_PRIORITY; PRIVILEGED_DATA static volatile BaseType_t xSchedulerRunning = pdFALSE; diff --git a/FreeRTOS/Test/CBMC/proofs/Task/TaskCreate/TaskCreate_harness.c b/FreeRTOS/Test/CBMC/proofs/Task/TaskCreate/TaskCreate_harness.c index d86a276396..6331c785bd 100644 --- a/FreeRTOS/Test/CBMC/proofs/Task/TaskCreate/TaskCreate_harness.c +++ b/FreeRTOS/Test/CBMC/proofs/Task/TaskCreate/TaskCreate_harness.c @@ -1,29 +1,27 @@ /* - * FreeRTOS memory safety proofs with CBMC. - * Copyright (C) 2019 Amazon.com, Inc. or its affiliates. All Rights Reserved. + * FreeRTOS V202012.00 + * Copyright (C) 2020 Amazon.com, Inc. or its affiliates. All Rights Reserved. * - * 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: + * 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 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. + * 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 * - * http://aws.amazon.com/freertos - * http://www.FreeRTOS.org */ #include @@ -44,9 +42,11 @@ void harness() char * pcName; configSTACK_DEPTH_TYPE usStackDepth = STACK_DEPTH; void * pvParameters; - UBaseType_t uxPriority; TaskHandle_t * pxCreatedTask; + UBaseType_t uxPriority; + __CPROVER_assume( uxPriority < configMAX_PRIORITIES ); + vNondetSetCurrentTCB(); vSetGlobalVariables(); vPrepareTaskLists();