-
Notifications
You must be signed in to change notification settings - Fork 277
Closed
Labels
Code ContractsFunction and loop contractsFunction and loop contractsawsBugs or features of importance to AWS CBMC usersBugs or features of importance to AWS CBMC usersbug
Description
CBMC version: 5.67.0
Operating system: N/A
For the following program:
int my_f(int x, ...)
{
__builtin_va_list list;
__builtin_va_start(list, x);
int value;
unsigned i;
for(i=0; i<x; i++)
__CPROVER_loop_invariant (
list == __CPROVER_loop_entry(list) + i && (value == 10 || i == 0)
)
{
value=__builtin_va_arg(list, int);
}
return value;
}
int main()
{
assert(my_f(1, 10)==10);
}
CBMC fails to prove that the invariant preserves.
I suppose the cause of failure is that __builtin_va_arg(p, int) is statically rewritten to va_args[j] where va_args is the build-in array of arguments. However, after havocing, p becomes a nondet pointer; hence __builtin_va_arg(p, int) cannot be correctly rewritten (and will be rewritten to symex::invalid_object!0#0 as an example).
To resolve the issue, we could rewrite __builtin_va_arg(p, int) to
- check if p is the same object as va_args: assert(same_object(p,va_args))
- check if the offset of p is valid: assert(offset(p) < object_size(va_args))
- substitute __builtin_va_arg(p, int) with (int)(*p)
Metadata
Metadata
Assignees
Labels
Code ContractsFunction and loop contractsFunction and loop contractsawsBugs or features of importance to AWS CBMC usersBugs or features of importance to AWS CBMC usersbug