Open
Description
CBMC version: 5.90.0 (cbmc-5.90.0-21-g6590981c4a
Operating system: MacOS 14.6.1
Exact command line resulting in the issue:
This is the file used:
#include <stdio.h>
#include <stdlib.h>
int main()
{
int rows=3;
int cols = 3;
int* arr = malloc(rows * cols * sizeof(int));
int *idx = &arr[0];
for(int i=0; i<rows; i++)
// __CPROVER_assigns(i,idx, *idx) //uncomment this line to make *idx unassignable
__CPROVER_loop_invariant(0 <= i && i <= rows)
__CPROVER_loop_invariant(idx == &arr[0]+i*rows)
__CPROVER_loop_invariant(rows==3 && cols==3)
{
*idx=i;
idx+=cols;
}
return 1;
}
These are the commands run
goto-cc tmp.c
goto-instrument --apply-loop-contracts a.out prcp.o
cbmc prcp.o
What behaviour did you expect:
I expect i, idx and *idx to be assignable (which they are, according to the results obtained using the inferred loop assigns statement). I also would not expect adding an explicit __CPROVER_assigns statement, which includes the same set of variables, to change the result.
What happened instead:
If you run the commands on the file above, 15 properties pass, including two that say:
[main.assigns.3] line 21 Check that *idx is assignable: SUCCESS
[main.assigns.6] line 21 Check that *idx is assignable: SUCCESS
If you add the __CPROVER_assigns statement, one of the check *idx is assignable properties fails:
[main.assigns.4] line 21 Check that *idx is assignable: SUCCESS
[main.assigns.7] line 21 Check that *idx is assignable: FAILURE
Metadata
Assignees
Labels
No labels