#include "cbmc.h"

/****************************************************************
* Model a malloc that can fail (CBMC malloc does not fail) and
* check that CBMC can model an object of the requested size.
****************************************************************/

void * safeMalloc( size_t size )
{
    __CPROVER_assert( size < CBMC_MAX_OBJECT_SIZE, "safeMalloc size too big" );
    return nondet_bool() ? NULL : malloc( size );
}