本文整理汇总了C++中ASSUME函数的典型用法代码示例。如果您正苦于以下问题：C++ ASSUME函数的具体用法？C++ ASSUME怎么用？C++ ASSUME使用的例子？那么恭喜您, 这里精选的函数代码示例或许可以为您提供帮助。
在下文中一共展示了ASSUME函数的20个代码示例，这些例子默认根据受欢迎程度排序。您可以为喜欢或者感觉有用的代码点赞，您的评价将有助于我们的系统推荐出更棒的C++代码示例。
示例1: main
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;
}
开发者ID:wei-wang-523，项目名称:cascade，代码行数:26，代码来源:ex47.c
示例2: main
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;
}
开发者ID:ArtisticCoding，项目名称:T2，代码行数:25，代码来源:ex18.c
示例3: randomIdx
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;
}
开发者ID:wei-wang-523，项目名称:cascade，代码行数:7，代码来源:ex43.c
示例4: main
/* 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;
}
开发者ID:ArtisticCoding，项目名称:T2，代码行数:31，代码来源:inf6.c
示例5: main
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;
}
开发者ID:wei-wang-523，项目名称:cascade，代码行数:25，代码来源:ex18.c
示例6: bufIdxWritten
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_;
}
开发者ID:wei-wang-523，项目名称:cascade，代码行数:8，代码来源:ex43.c
示例7: RemoveByFrameIndex
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;
}
开发者ID:Industrialice，项目名称:StdLib，代码行数:8，代码来源:deprecatedCFramedStore.hpp
示例8: sigset_or
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;
}
开发者ID:andrewguy9，项目名称:kernelpanic，代码行数:9，代码来源:unix_hal.c
示例9: main
int
main(int argc, char *argv[])
{
ASSUME(argc > 0);
ASSUME(argv[argc] == NULL);
printf("Hello world!\n");
return 0;
}
开发者ID:joeljk13，项目名称:C-Libs，代码行数:10，代码来源:main.c
示例10: main
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;
}
开发者ID:wei-wang-523，项目名称:cascade，代码行数:12，代码来源:malloc0_false-valid-deref.c
示例11: __llbmc_main
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;
}
开发者ID:ArtisticCoding，项目名称:T2，代码行数:12，代码来源:ex49.original.c
示例12: main
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;
}
开发者ID:wei-wang-523，项目名称:cascade，代码行数:14，代码来源:inf2.c
示例13: bufWrite
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_;
}
开发者ID:wei-wang-523，项目名称:cascade，代码行数:14，代码来源:ex43.c
示例14: main
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;
}
开发者ID:wei-wang-523，项目名称:cascade，代码行数:14，代码来源:ex5.c
示例15: main
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;
}
开发者ID:wei-wang-523，项目名称:cascade，代码行数:14，代码来源:simpEx10.c
示例16: Remove
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;
}
}
}
开发者ID:Industrialice，项目名称:StdLib，代码行数:15，代码来源:deprecatedCFramedStore.hpp
示例17: Own
void Own( UniquePtr *source )
{
ASSUME( (_ptr != source->_ptr) || (_ptr == 0) );
Deleter( (X *)_ptr );
_ptr = source->_ptr;
source->_ptr = 0;
}
开发者ID:Industrialice，项目名称:StdLib，代码行数:7，代码来源:UniquePtr.hpp
示例18: ASSUME
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;
}
开发者ID:Industrialice，项目名称:StdLib，代码行数:32，代码来源:FileCFILEStream.cpp
示例19: Initialize
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;
}
开发者ID:Industrialice，项目名称:StdLib，代码行数:32，代码来源:MiscWindows.cpp
示例20: ASSUME
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;
}
开发者ID:Industrialice，项目名称:StdLib，代码行数:29，代码来源:Nullable.hpp
注：本文中的ASSUME函数示例整理自Github/MSDocs等源码及文档管理平台，相关代码片段筛选自各路编程大神贡献的开源项目，源码版权归原作者所有，传播和使用请参考对应项目的License；未经允许，请勿转载。 |
客服电话
APP下载
官方微信
请发表评论