Fixed test that triggers the newly added pointer overflow checks

Remi Delmas · Remi Delmas · commit e2f4fecb5aeb · 2021-12-03T18:45:18.000Z
diff --git a/regression/contracts/quantifiers-forall-ensures-enforce/main.c b/regression/contracts/quantifiers-forall-ensures-enforce/main.c
@@ -23,7 +23,7 @@ int f1(int *arr, int len)
 int main()
 {
   int len;
-  __CPROVER_assume(0 <= len && len <= MAX_LEN);
+  __CPROVER_assume(0 < len && len <= MAX_LEN);
 
   int *arr = malloc(len * sizeof(int));
   f1(arr, len);

Original file line number	Diff line number	Diff line change
`@@ -23,7 +23,7 @@ int f1(int *arr, int len)`
`23`	`23`	`int main()`
`24`	`24`	`{`
`25`	`25`	`int len;`
`26`		`- __CPROVER_assume(0 <= len && len <= MAX_LEN);`
	`26`	`+ __CPROVER_assume(0 < len && len <= MAX_LEN);`
`27`	`27`
`28`	`28`	`int arr = malloc(len sizeof(int));`
`29`	`29`	`f1(arr, len);`