File tree 1 file changed +5
-2
lines changed
1 file changed +5
-2
lines changed Original file line number Diff line number Diff line change @@ -1206,8 +1206,9 @@ __CPROVER_HIDE:;
1206
1206
}
1207
1207
if (__VERIFIER_nondet___CPROVER_bool ())
1208
1208
{
1209
+ // make pointer invalid, empty value set and nondet bit pattern
1209
1210
__CPROVER_size_t dummy = __VERIFIER_nondet_size ();
1210
- * elem = (void * ) dummy ;
1211
+ * elem = (void * )dummy ;
1211
1212
return 0 ;
1212
1213
}
1213
1214
void * ptr = __CPROVER_allocate (size , 0 );
@@ -1265,8 +1266,9 @@ __CPROVER_HIDE:;
1265
1266
}
1266
1267
if (__VERIFIER_nondet___CPROVER_bool ())
1267
1268
{
1269
+ // make pointer invalid, empty value set and nondet bit pattern
1268
1270
__CPROVER_size_t dummy = __VERIFIER_nondet_size ();
1269
- * elem = (void * ) dummy ;
1271
+ * elem = (void * )dummy ;
1270
1272
return 0 ;
1271
1273
}
1272
1274
void * ptr = __CPROVER_allocate (size , 0 );
@@ -1370,6 +1372,7 @@ __CPROVER_HIDE:;
1370
1372
{
1371
1373
if (__VERIFIER_nondet___CPROVER_bool ())
1372
1374
{
1375
+ // make pointer invalid, empty value set and nondet bit pattern
1373
1376
__CPROVER_size_t dummy = __VERIFIER_nondet_size ();
1374
1377
* ptr = (void * )dummy ;
1375
1378
return 0 ;
You can’t perform that action at this time.
0 commit comments