自学教程：C++ ASSUME函数代码示例

int main(int h, int w, int k){		DIST **lut; // lookup table, 2D array of structures	DIST *array;	int x, y;		ASSUME(h > 0);	ASSUME(w > 0);	ASSUME(k < h * w && k > 0);	//   fSft__assume(k > 0 && k < h*w);		lut = (DIST**)malloc(sizeof(DIST*)*h);	ASSERT(valid(&lut[0]));	lut[0] = (DIST*)malloc(sizeof(DIST)*h*w);	for (y=0; y<h; y++) {		ASSERT(valid(&lut[0]) && valid(&lut[y]));		lut[y] = lut[0] + w*y;	}	array = lut[0];	//    fSfT_assert(array[k] == lut[k/w][k%w]);	ASSERT(array[k] == lut[k/w][k%w]);	free(lut[0]);	free(lut);		return 1;}

int main(){   int * a;   int i,j;   int k = __NONDET__();   if ( k <= 0 || k > 100) return -1;      a= malloc( k * sizeof(int));   ASSUME(a != NULL);   ASSUME(k >= 100);      for (i =0 ; i != k; i++)      if (a[i] <= 1) break;   i--;      for (j = 0; j < i; ++j)      a[j] = a[i];      return 0;}

idx_t randomIdx(const buf_t *buf_) {	ASSUME(buf_ != NULL);	idx_t idx = __VERIFIER_nondet_int();	ASSUME(0 <= idx);	ASSUME(idx < buf_->maxNumData);	return idx;}

/* int __llbmc_main(int a, int b) { */int main(int a, int b) {    int status = 0, as, bs, flag=0;    if(a > 0) {        status = 0;    }    else {        status = 1;    }	    if(status == 1) {        ASSUME(b > 0);    }    else {        ASSUME(b <= 0);    }    if(a > 0)        as = 0;    else        as = 1;    if(b > 0)        bs = 0;    else        bs = 1;    if (bs == as) flag = 1;    ASSERT(flag == 0);    return 0;}

int main(){   int * a;   int i,j;   int k = __VERIFIER_nondet_int();   if ( k <= 0 )      return -1;   a= malloc( k * sizeof(int));   ASSUME(a);   ASSUME(k >= 100);      for (i =0 ; i != k; i++)      if (a[i] <= 1)     	  break;   i--;      for (j = 0; j < i; ++j)      a[j] = a[i];      return 0;}

bool_t bufIdxWritten(const buf_t *buf_, idx_t idx_) {	ASSUME(buf_ != NULL );	ASSUME(0 <= idx_ );	ASSUME(idx_ < buf_->maxNumData);	return buf_->dataWriteEvidence[idx_] >= 0 &&    buf_->dataWriteEvidence[idx_] < buf_->numData &&    buf_->dataIdx[buf_->dataWriteEvidence[idx_]] == idx_;}

 void RemoveByFrameIndex( uiw frame, uiw index ) {     ASSUME( frame < _o_frames.Size() && index < t_frameSize );     ASSUME( !_IsFree( &_o_frames[ frame ].p_mem[ index ] ) );     _o_frames[ frame ].p_mem[ index ].~X();     _SetFree( &_o_frames[ frame ].p_mem[ index ] );     --_o_frames[ frame ].used; }

sigset_t sigset_or(sigset_t a, sigset_t b) {	int status;	sigset_t result;	status = sigemptyset(&result);	ASSUME(status, 0);	status = sigorset(&result, &a, &b);	ASSUME(status, 0);	return result;}

intmain(int argc, char *argv[]){    ASSUME(argc > 0);    ASSUME(argv[argc] == NULL);    printf("Hello world!/n");    return 0;}

int * main (int x){	ASSUME(x >= 0);		int * a = (int *) malloc( x * sizeof(int));	int i = 0;	a[i] = __VERIFIER_nondet_int();	i = __VERIFIER_nondet_int();		ASSUME(i >= 0 && i < x);		return a;}

int __llbmc_main( int n){    int i, sum=0;    ASSUME( n >= 0);    ASSUME(n <= 1000);    for (i=0; i < n; ++i)        sum = sum +i;    ASSERT(sum >= 0);    return 0;}

int main(int a, int b){	st_t * st1, * st2;	ASSUME(a> 0);	ASSUME(b > 0);		st1 = st_alloc(a,b);		st2 = st_alloc(-b,-a);			st_compact(st1,st2);	return 1;	}

void bufWrite(buf_t *buf_, idx_t idx_, data_t val_) {	ASSUME(buf_!=NULL);	ASSUME(0 <= idx_);	ASSUME(idx_ < buf_->maxNumData);	idx_t writeDataTo = buf_->dataWriteEvidence[idx_];	if (!bufIdxWritten(buf_, idx_)) {		ASSERT(buf_->numData < buf_->maxNumData);		buf_->dataIdx[buf_->numData] = idx_;		buf_->dataWriteEvidence[idx_] = buf_->numData;		writeDataTo = buf_->numData;		buf_->numData++;	}	buf_->data[writeDataTo] = val_;}

int main(){	int a[20];	ASSUME(x >= 0);	ASSUME(y >= 0);	ASSUME(x< 9);	ASSUME(y < 10);		if (x * y - x*x >= 50){		x=x+1;	}		a[x]=1;	return 1;}

int main(Addr *addr, Buffer *buf){	addr = (Addr *)malloc(sizeof(Addr));	buf = (Buffer *)malloc(sizeof(Buffer));	ASSUME(addr->len >= 0 && addr->len < 16);	ASSUME(addr->len <= 16);    for(int idx =0; idx < addr->len; idx++) {    addr->dat[idx-1] = 'c';  }  free(addr);  free(buf);  return 0;}

 void Remove( X *p_val ) {     for( uiw frame = 0; ; ++frame )     {         ASSUME( frame < _o_frames.Size() );         if( p_val >= _o_frames[ frame ].p_mem && p_val <= _o_frames[ frame ].p_mem + t_frameSize - 1 )         {             ASSUME( !_IsFree( p_val ) );             p_val->~X();             _SetFree( p_val );             --_o_frames[ frame ].used;             break;         }     } }

 void Own( UniquePtr *source ) {     ASSUME( (_ptr != source->_ptr) || (_ptr == 0) );     Deleter( (X *)_ptr );     _ptr = source->_ptr;     source->_ptr = 0; }

bln FileCFILEStream::SizeSet( ui64 newSize, CError *error ){	ASSUME( IsOpened() );		DSA( error, Error::UnknownError() );	newSize += _offsetToStart;	i64 currentOffset = ftell( (FILE *)_file );	if( currentOffset == -1 )	{		return false;	}	if( fseek( (FILE *)_file, newSize, SEEK_SET ) != 0 )	{		return false;	}	if( fputc( '/0', (FILE *)_file ) != 0 )	{		return false;	}	if( fseek( (FILE *)_file, currentOffset, SEEK_SET ) != 0 )	{		return false;	}	DSA( error, Error::Ok() );	return true;}

		void Initialize()		{			SYSTEM_INFO sysinfo;			::GetSystemInfo( &sysinfo );			_memPageSize = sysinfo.dwPageSize;			_cpuCoresCount = sysinfo.dwNumberOfProcessors;			LARGE_INTEGER o_freq;			BOOL freqRes = ::QueryPerformanceFrequency( &o_freq );			ASSUME( freqRes );			_freqMultSec32 = 1.f / o_freq.QuadPart;			_freqMultSec64 = 1.0 / o_freq.QuadPart;			_freqMultMSec32 = 1000.f / o_freq.QuadPart;			_freqMultMSec64 = 1000.0 / o_freq.QuadPart;			_freqMultUSec32 = 1000000.f / o_freq.QuadPart;			_freqMultUSec64 = 1000000.0 / o_freq.QuadPart;			_freqSec32 = (f32)o_freq.QuadPart;			_freqSec64 = (f64)o_freq.QuadPart;			_freqMSec32 = (f32)o_freq.QuadPart * 1000.f;			_freqMSec64 = (f64)o_freq.QuadPart * 1000.0;			_freqUSec32 = (f32)o_freq.QuadPart * 1000000.f;			_freqUSec64 = (f64)o_freq.QuadPart * 1000000.0;			_freqDivU64 = o_freq.QuadPart;		}

	Nullable &operator = ( Nullable &&source )	{		ASSUME( this != &source );		if( this->_is_null == source._is_null )		{			if( this->_is_null == false )			{				ToRef() = std::move( *(X *)&source._object );			}		}		else		{			if( this->_is_null == false )			{				this->ToRef().~X();			}			else			{				new (&this->_object) X( std::move( *(X *)&source._object ) );			}			this->_is_null = source._is_null;		}		source->_is_null = true;		return *this;	}

TimeMoment TimeMoment::CreateCurrent(){	LARGE_INTEGER current;	BOOL result = QueryPerformanceCounter( &current );	ASSUME( result );	return current;}

/* int __llbmc_main(int n){ */int main(int n){   int alen;     int * x;   ASSUME( n > 0);   ASSUME (n <= (1 << 20));   array = (foo_t *) malloc(n * sizeof(foo_t));   memset(array,0, sizeof(foo_t)* n);   /*-- check     Length(array) * sizeof(*array) >= sizeof(foo_t) * n          --*/      return 1;}

TIME HalGetTime(){        struct timeval sysTime;        ASSUME(gettimeofday(&sysTime, NULL), 0);        return HalTimeDelta(&HalStartupTime, &sysTime);}

    X &Enumerate( uiw *p_frame, uiw *p_index )    {        ASSUME( p_frame && p_index );        for( ; ; )        {            uiw frame = *p_frame;            uiw index = *p_index;            ++*p_index;            if( *p_index == t_frameSize )            {                *p_index = 0;                ++*p_frame;            }            if( frame == _o_frames.Size() )            {                *p_frame = uiw_max;                return _o_frames[ 0 ].p_mem[ 0 ];            }            if( !_IsFree( &_o_frames[ frame ].p_mem[ index ] ) )            {                return _o_frames[ frame ].p_mem[ index ];            }        }    }

CMutex::CMutex( ui32 spinCount /* = 0 */ ){    pthread_mutexattr_t attr;    int result = pthread_mutexattr_init( &attr );    ASSUME( result == 0 );    result = pthread_mutexattr_settype( &attr, PTHREAD_MUTEX_RECURSIVE );    ASSUME( result == 0 );    result = pthread_mutex_init( &_handle, &attr );    ASSUME( result == 0 );    result = pthread_mutexattr_destroy( &attr );    ASSUME( result == 0 );}

NOINLINE VirtualMem::PageMode::PageMode_t VirtualMem::VM_ProtectGet( const void *p_mem, uiw size, CError *po_error ){    MEMORY_BASIC_INFORMATION o_mbi;    PageMode::PageMode_t mode = PageMode::Error;    CError error = Error::Ok();    size = Funcs::RoundUIUpToStep( size, VM_PageSize() );    SIZE_T infSize = ::VirtualQuery( p_mem, &o_mbi, sizeof(o_mbi) );    if( !infSize )    {		error = Error::UnknownError();        goto toExit;    }    if( o_mbi.RegionSize < size )    {        error = Error_InconsistentProtection();        goto toExit;    }    for( ui32 index = 0; index < COUNTOF( ca_PageProtectMapping ); ++index )    {        if( ca_PageProtectMapping[ index ] == o_mbi.Protect )        {            mode = (PageMode::PageMode_t)index;            break;        }    }    ASSUME( mode != PageMode::Error );toExit:    DSA( po_error, error );    return mode;}