len0rd/FreeRTOS-Kernel
1
0
Fork 0
mirror of https://github.com/FreeRTOS/FreeRTOS-Kernel.git synced 2025-10-17 02:07:48 -04:00
Code Issues Projects Releases Packages Wiki Activity

Sync with a:FR (#75)

Browse source 
* AFR sync

* AFR sync: CBMC

* AFR sync: CBMC: remove .bak files

* AFR sync: CBMC: more cleanup

* Corrected CBMC proofs

* Corrected CBMC patches

* Corrected CBMC patches-1

* Corrected CBMC patches-2

* remove .bak files (3)

Co-authored-by: Yuhui Zheng <10982575+yuhui-zheng@users.noreply.github.com>
This commit is contained in:
Aniruddha Kanhere 2020-05-28 10:11:58 -07:00 • committed by GitHub
parent 6557291e54
commit cb7edd2323
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
99 changed files with 6475 additions and 4241 deletions
Download patch file Download diff file Expand all files Collapse all files

149
FreeRTOS/Test/CBMC/include/cbmc.h
View file

@ -1,67 +1,100 @@
/*
* CBMC models a pointer as an object id and an offset into that
* object. The top bits of a pointer encode the object id and the
* remaining bits encode the offset. This means there is a bound on
* the maximum offset into an object in CBMC, and hence a bound on the
* size of objects in CBMC.
*/
#define CBMC_BITS 7
#define CBMC_MAX_OBJECT_SIZE (0xFFFFFFFF >> CBMC_BITS)
/* Standard includes. */
#include <stdint.h>
#include <stdio.h>
enum CBMC_LOOP_CONDITION { CBMC_LOOP_BREAK, CBMC_LOOP_CONTINUE, CBMC_LOOP_RETURN };
/* FreeRTOS includes. */
#include "FreeRTOS.h"
#include "task.h"
#include "semphr.h"
// CBMC specification: capture old value for precondition /
// postcondition checking
#define OLDVAL(var) _old_ ## var
#define SAVE_OLDVAL(var,typ) const typ OLDVAL(var) = var
// CBMC specification: capture old value for values passed by
// reference in function abstractions
#define OBJ(var) (*var)
#define OLDOBJ(var) _oldobj_ ## var
#define SAVE_OLDOBJ(var,typ) const typ OLDOBJ(var) = OBJ(var)
// CBMC debugging: printfs for expressions
#define __CPROVER_printf(var) { uint32_t ValueOf_ ## var = (uint32_t) var; }
#define __CPROVER_printf2(str,exp) { uint32_t ValueOf_ ## str = (uint32_t) (exp); }
// CBMC debugging: printfs for pointer expressions
#define __CPROVER_printf_ptr(var) { uint8_t *ValueOf_ ## var = (uint8_t *) var; }
#define __CPROVER_printf2_ptr(str,exp) { uint8_t *ValueOf_ ## str = (uint8_t *) (exp); }
/* FreeRTOS+TCP includes. */
#include "FreeRTOS_IP.h"
#include "FreeRTOS_Sockets.h"
#include "FreeRTOS_IP_Private.h"
#include "FreeRTOS_UDP_IP.h"
#include "FreeRTOS_DNS.h"
#include "FreeRTOS_DHCP.h"
#include "NetworkBufferManagement.h"
#include "NetworkInterface.h"
/*
* An assertion that pvPortMalloc returns NULL when asked to allocate 0 bytes.
* This assertion is used in some of the Task proofs.
*/
#define __CPROVER_assert_zero_allocation() \
__CPROVER_assert( pvPortMalloc(0) == NULL, \
"pvPortMalloc allows zero-allocated memory.")
* CBMC models a pointer as an object id and an offset into that
* object. The top bits of a pointer encode the object id and the
* remaining bits encode the offset. This means there is a bound on
* the maximum offset into an object in CBMC, and hence a bound on the
* size of objects in CBMC.
*/
#define CBMC_BITS 7
#define CBMC_MAX_OBJECT_SIZE ( 0xFFFFFFFF >> ( CBMC_BITS + 1 ) )
/*
* A stub for pvPortMalloc that nondeterministically chooses to return
* either NULL or an allocation of the requested space. The stub is
* guaranteed to return NULL when asked to allocate 0 bytes.
* This stub is used in some of the Task proofs.
*/
void *pvPortMalloc( size_t xWantedSize )
{
if ( xWantedSize == 0 )
{
return NULL;
}
return nondet_bool() ? malloc( xWantedSize ) : NULL;
}
void vPortFree( void *pv )
{
(void)pv;
free(pv);
}
#define IMPLIES( a, b ) ( !( a ) || ( b ) )
BaseType_t nondet_basetype();
UBaseType_t nondet_ubasetype();
TickType_t nondet_ticktype();
int32_t nondet_int32();
uint32_t nondet_uint32();
size_t nondet_sizet();
#define nondet_BaseType() nondet_basetype()
void * safeMalloc( size_t size );
enum CBMC_LOOP_CONDITION
{
CBMC_LOOP_BREAK, CBMC_LOOP_CONTINUE, CBMC_LOOP_RETURN
};
/* CBMC specification: capture old value for precondition and */
/* postcondition checking */
#define OLDVAL( var ) _old_ ## var
#define SAVE_OLDVAL( var, typ ) const typ OLDVAL( var ) = var
/* CBMC specification: capture old value for values passed by */
/* reference in function abstractions */
#define OBJ( var ) ( * var )
#define OLDOBJ( var ) _oldobj_ ## var
#define SAVE_OLDOBJ( var, typ ) const typ OLDOBJ( var ) = OBJ( var )
/* CBMC debugging: printfs for expressions */
#define __CPROVER_printf( var ) { uint32_t ValueOf_ ## var = ( uint32_t ) var; }
#define __CPROVER_printf2( str, exp ) { uint32_t ValueOf_ ## str = ( uint32_t ) ( exp ); }
/* CBMC debugging: printfs for pointer expressions */
#define __CPROVER_printf_ptr( var ) { uint8_t * ValueOf_ ## var = ( uint8_t * ) var; }
#define __CPROVER_printf2_ptr( str, exp ) { uint8_t * ValueOf_ ## str = ( uint8_t * ) ( exp ); }
/*
* An assertion that pvPortMalloc returns NULL when asked to allocate 0 bytes.
* This assertion is used in some of the TaskPool proofs.
*/
#define __CPROVER_assert_zero_allocation() \
__CPROVER_assert( pvPortMalloc( 0 ) == NULL, \
"pvPortMalloc allows zero-allocated memory." )
/*
* A stub for pvPortMalloc that nondeterministically chooses to return
* either NULL or an allocation of the requested space. The stub is
* guaranteed to return NULL when asked to allocate 0 bytes.
* This stub is used in some of the TaskPool proofs.
*/
void * pvPortMalloc( size_t xWantedSize )
{
if( xWantedSize == 0 )
{
return NULL;
}
return nondet_bool() ? malloc( xWantedSize ) : NULL;
}
void vPortFree( void * pv )
{
( void ) pv;
free( pv );
}