@ -1,29 +1,31 @@
/*
* FreeRTOS memory safety proofs with CBMC .
* Copyright ( C ) 2019 Amazon . com , Inc . or its affiliates . All Rights Reserved .
* FreeRTOS V202104 .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
*/
/*
* FreeRTOS memory safety proofs with CBMC .
*/
# include "cbmc.h"
@ -50,7 +52,7 @@ StackType_t *pxTimerTaskStack;
* ` pxCurrentTCB ` allocation is allowed to fail . The global variables above
* this comment are used in the stubbed functions ` vApplicationGetIdleTaskMemory `
* and ` vApplicationGetTimerTaskMemory ` ( at the end of this file ) and buffer allocation
* must be succes ful for the proof to have no errors
* must be succes s ful for the proof to have no errors
*/
BaseType_t xPrepareTasks ( void )
{
@ -88,7 +90,7 @@ BaseType_t xPrepareTasks( void )
}
/*
* The buffers used here have been succes fully allocated before ( global variables )
* The buffers used here have been succes s fully allocated before ( global variables )
*/
void vApplicationGetIdleTaskMemory ( StaticTask_t * * ppxIdleTaskTCBBuffer ,
StackType_t * * ppxIdleTaskStackBuffer ,
@ -100,7 +102,7 @@ void vApplicationGetIdleTaskMemory( StaticTask_t ** ppxIdleTaskTCBBuffer,
}
/*
* The buffers used here have been succes fully allocated before ( global variables )
* The buffers used here have been succes s fully allocated before ( global variables )
*/
void vApplicationGetTimerTaskMemory ( StaticTask_t * * ppxTimerTaskTCBBuffer , StackType_t * * ppxTimerTaskStackBuffer , uint32_t * pulTimerTaskStackSize )
{