__CPROVER_object_slice and __CPROVER_object_from are used in the loop specification and have some problems. #6979
Description
CBMC version: remi-delmas-3000:contracts-object-slice
Merged Link: CONTRACTS: Support object slices in assigns clauses
Operating system: Ubuntu 20.04
I found that cbmc started to support assigns of a specific length. And I saw a example to use it.
So I want to use the '__CPROVER_object_slice' in my code, but I found a problem if it used in the loop contracts.
file: test1.c
1 struct st
2 {
3 int a;
4 char arr1[10];
5 int b;
6 char arr2[10];
7 int c;
8 };
9
10 void foo(struct st *s)
11 {
12 for (int i = 0; i < 10; i++)
13 __CPROVER_assigns(i, __CPROVER_object_slice(s->arr1, 5))
14 __CPROVER_loop_invariant(0 <= i && i <= 10)
15 __CPROVER_decreases(10 - i)
16 {
17 s->arr1[i] = 0;
18 }
19 for (int i = 0; i < 10; i++)
20 __CPROVER_assigns(i, __CPROVER_object_from(s->arr2 + 5))
21 __CPROVER_loop_invariant(0 <= i && i <= 10)
22 __CPROVER_decreases(10 - i)
23 {
24 s->arr2[i] = 0;
25 }
26 }
27
28 int main()
29 {
30 struct st s;
31
32 foo(&s);
33
34 return 0;
35 }
commands:
goto-cc -o foo1.goto test1.c --function foo
goto-instrument --apply-loop-contracts foo1.goto foo-checking-contracts.goto
cbmc foo-checking-contracts.goto --function foo
Are __CPROVER_object_slice and __CPROVER_object_from currently only supported in the function specification? Or is there something wrong with my writing? @remi-delmas-3000