File tree Expand file tree Collapse file tree 1 file changed +5
-2
lines changed
Expand file tree Collapse file tree 1 file changed +5
-2
lines changed Original file line number Diff line number Diff line change @@ -1206,8 +1206,9 @@ __CPROVER_HIDE:;
12061206 }
12071207 if (__VERIFIER_nondet___CPROVER_bool ())
12081208 {
1209+ // make pointer invalid, empty value set and nondet bit pattern
12091210 __CPROVER_size_t dummy = __VERIFIER_nondet_size ();
1210- * elem = (void * ) dummy ;
1211+ * elem = (void * )dummy ;
12111212 return 0 ;
12121213 }
12131214 void * ptr = __CPROVER_allocate (size , 0 );
@@ -1265,8 +1266,9 @@ __CPROVER_HIDE:;
12651266 }
12661267 if (__VERIFIER_nondet___CPROVER_bool ())
12671268 {
1269+ // make pointer invalid, empty value set and nondet bit pattern
12681270 __CPROVER_size_t dummy = __VERIFIER_nondet_size ();
1269- * elem = (void * ) dummy ;
1271+ * elem = (void * )dummy ;
12701272 return 0 ;
12711273 }
12721274 void * ptr = __CPROVER_allocate (size , 0 );
@@ -1370,6 +1372,7 @@ __CPROVER_HIDE:;
13701372 {
13711373 if (__VERIFIER_nondet___CPROVER_bool ())
13721374 {
1375+ // make pointer invalid, empty value set and nondet bit pattern
13731376 __CPROVER_size_t dummy = __VERIFIER_nondet_size ();
13741377 * ptr = (void * )dummy ;
13751378 return 0 ;
You can’t perform that action at this time.
0 commit comments