Correct assigns contract for lopp in ctcc() function. Proof now OK.

rod-chapman · rod-chapman · commit b412c3f879d9 · 2024-06-14T12:20:22.000+01:00
Signed-off-by: Rod Chapman &lt;rodchap@amazon.com&gt;
diff --git a/arrays/ar.c b/arrays/ar.c
@@ -207,7 +207,7 @@ int ctcc(uint8_t *dst, const uint8_t *src, uint32_t len, uint8_t dont)
     __CPROVER_assert(mask == (dont == 0 ? 0xff : 0x00), "prove mask set correctly");
 
     for (size_t i = 0; i < len; i++)
-    __CPROVER_assigns(i, dst)
+    __CPROVER_assigns(i, __CPROVER_object_whole(dst))
     __CPROVER_loop_invariant(i <= len)
     __CPROVER_loop_invariant(__CPROVER_forall { size_t j; (0 <= j && j < i) ==> dst[j] == (dont == 0 ? src[j] : __CPROVER_loop_entry(dst)[j]) })
     {

Original file line number	Diff line number	Diff line change
`@@ -207,7 +207,7 @@ int ctcc(uint8_t dst, const uint8_t src, uint32_t len, uint8_t dont)`
`207`	`207`	`__CPROVER_assert(mask == (dont == 0 ? 0xff : 0x00), "prove mask set correctly");`
`208`	`208`
`209`	`209`	`for (size_t i = 0; i < len; i++)`
`210`		`- __CPROVER_assigns(i, dst)`
	`210`	`+ __CPROVER_assigns(i, __CPROVER_object_whole(dst))`
`211`	`211`	`__CPROVER_loop_invariant(i <= len)`
`212`	`212`	`__CPROVER_loop_invariant(__CPROVER_forall { size_t j; (0 <= j && j < i) ==> dst[j] == (dont == 0 ? src[j] : __CPROVER_loop_entry(dst)[j]) })`
`213`	`213`	`{`