diff --git a/src/ansi-c/library/cprover_contracts.c b/src/ansi-c/library/cprover_contracts.c index 7aa24f07148..b3f6032b47e 100644 --- a/src/ansi-c/library/cprover_contracts.c +++ b/src/ansi-c/library/cprover_contracts.c @@ -1206,8 +1206,9 @@ __CPROVER_HIDE:; } if(__VERIFIER_nondet___CPROVER_bool()) { + // make pointer invalid, empty value set and nondet bit pattern __CPROVER_size_t dummy = __VERIFIER_nondet_size(); - *elem = (void *) dummy; + *elem = (void *)dummy; return 0; } void *ptr = __CPROVER_allocate(size, 0); @@ -1265,8 +1266,9 @@ __CPROVER_HIDE:; } if(__VERIFIER_nondet___CPROVER_bool()) { + // make pointer invalid, empty value set and nondet bit pattern __CPROVER_size_t dummy = __VERIFIER_nondet_size(); - *elem = (void *) dummy; + *elem = (void *)dummy; return 0; } void *ptr = __CPROVER_allocate(size, 0); @@ -1370,6 +1372,7 @@ __CPROVER_HIDE:; { if(__VERIFIER_nondet___CPROVER_bool()) { + // make pointer invalid, empty value set and nondet bit pattern __CPROVER_size_t dummy = __VERIFIER_nondet_size(); *ptr = (void *)dummy; return 0;