Description
CBMC version: 556b432
Operating system: Mac OS 10.15.7
Test case:
#include <assert.h>
#include <stdlib.h>
static int adder(const int *a, const int *b)
{
return (*a + *b);
}
int main()
{
int x = 1024;
int (*local_adder)(const int *, const int *) = adder;
while(x > 0)
__CPROVER_loop_invariant(1 == 1)
{
x += local_adder(&x, &x); // loop detection fails
//x += adder(&x, &x); // works fine
}
}Exact command line resulting in the issue:
$ goto-cc test.c -o test.gb
$ goto-instrument --enforce-all-contracts test.gb test.2.gb
$ cbmc test.2.gbWhat behaviour did you expect:
The loop invariant would be used and unwinding wouldn't be necessary.
What happened instead:
The loop invariant is not used because the loop in main is not recognized.
Note that if we use adder in place of local_adder within the loop, then the loop is detected and the loop invariant is processed as expected.
Additional context:
If we use adder in place of local_adder above, i.e. call the function directly as opposed to using a function pointer, then loop is detected and invariant is processed as expected.
The following instrumentation code:
for(auto &goto_function : goto_model.goto_functions.function_map) {
natural_loops_mutablet natural_loops(goto_function.second.body);
log.warning() << goto_function.first.c_str() << " has "
<< natural_loops.loop_map.size() << " loops."
<< messaget::eom;
}produces the following output when using local_adder function pointer
Reading GOTO program from 'test.gb'
main has 0 loops.
adder has 0 loops.
__CPROVER__start has 0 loops.
__CPROVER_initialize has 0 loops.
Writing GOTO program to 'test.2.gb'
and produces the following output when using adder directly
Reading GOTO program from 'test.gb'
main has 1 loops.
adder has 0 loops.
__CPROVER__start has 0 loops.
__CPROVER_initialize has 0 loops.
Writing GOTO program to 'test.2.gb'