Merge branch 'diffblue:develop' into develop

Author: yvizel

CHANGELOG

@@ -1,3 +1,27 @@
+# CBMC 6.4.0
+
+This release improves upon automated assigns-clause inference for loop invariants, which should make manually adding assigns clauses to loops less frequent.
+
+## What's Changed
+* [CONTRACTS] Support alias of member pointers in loop assigns inference by @qinheping in https://github.com/diffblue/cbmc/pull/8486
+* [CONTRACTS] Detect loop locals with goto_rw in DFCC by @qinheping in https://github.com/diffblue/cbmc/pull/8489
+* [CONTRACTS] DFCC loop assigns infererence with functions inlined by @qinheping in https://github.com/diffblue/cbmc/pull/8490
+
+## Bug Fixes
+* SMT2: implement range type by @kroening in https://github.com/diffblue/cbmc/pull/8466
+* Man pages: improve wording of unwinding-related options by @tautschnig in https://github.com/diffblue/cbmc/pull/8471
+* `format_type` can now format `range_typet` by @kroening in https://github.com/diffblue/cbmc/pull/8473
+* Contracts: document use of __CPROVER_loop_entry with arrays by @tautschnig in https://github.com/diffblue/cbmc/pull/8470
+* `bitvector_typet`: set width from mp_integer by @kroening in https://github.com/diffblue/cbmc/pull/8477
+* CI: add macos-14 (macOS on M1) job by @tautschnig in https://github.com/diffblue/cbmc/pull/8382
+* Remove macos-12 CI job by @tautschnig in https://github.com/diffblue/cbmc/pull/8482
+* [CONTRACTS] Support alias of member pointers in loop assigns inference by @qinheping in https://github.com/diffblue/cbmc/pull/8486
+* zero extension expression by @kroening in https://github.com/diffblue/cbmc/pull/8442
+* [CONTRACTS] Detect loop locals with goto_rw in DFCC by @qinheping in https://github.com/diffblue/cbmc/pull/8489
+* [CONTRACTS] DFCC loop assigns infererence with functions inlined by @qinheping in https://github.com/diffblue/cbmc/pull/8490
+
+**Full Changelog**: https://github.com/diffblue/cbmc/compare/cbmc-6.3.1...cbmc-6.4.0
+
 # CBMC 6.3.1
 
 This patch release addresses build failures on Apple Silicon (via PR #8461).

regression/cbmc/Pointer_difference2/test.desc

@@ -5,11 +5,11 @@ main.c
 ^\[main.pointer.1\] line 8 same object violation in array - other_array: FAILURE$
 ^\[main.assertion.2\] line 11 undefined behavior: FAILURE$
 ^\[main.assertion.3\] line 13 undefined behavior: FAILURE$
-^\[main.assertion.7\] line 26 end plus 2 is nondet: FAILURE$
+^\[main.assertion.7\] line 26 end plus 2 is nondet: (UNKNOWN|FAILURE)$
 ^\[main.pointer_arithmetic.\d+\] line 26 pointer relation: pointer outside object bounds in p: FAILURE$
-^\[main.assertion.8\] line 28 end plus 2 is nondet: FAILURE$
+^\[main.assertion.8\] line 28 end plus 2 is nondet: (UNKNOWN|FAILURE)$
 ^\[main.pointer_arithmetic.\d+\] line 28 pointer relation: pointer outside object bounds in p: FAILURE$
-^\*\* 9 of \d+ failed
+^\*\* [789] of \d+ failed
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$

regression/contracts-dfcc/dont_skip_cprover_prefixed_vars_fail/main.c

@@ -1,8 +1,11 @@
 void foo()
 {
-  int nondet_var;
-  int __VERIFIER_var;
-  int __CPROVER_var;
+  // Initialize them with `nondet_int` to avoid them being ignored by DFCC.
+  // DFCC ignores variables that are not read/written to outside the loop
+  // or in the loop contracts.
+  int nondet_var = nondet_int();
+  int __VERIFIER_var = nondet_int();
+  int __CPROVER_var = nondet_int();
   for(int i = 10; i > 0; i--)
     // clang-format off
   __CPROVER_assigns(i)

regression/contracts-dfcc/dont_skip_cprover_prefixed_vars_pass/main.c

@@ -1,8 +1,11 @@
 void foo()
 {
-  int nondet_var;
-  int __VERIFIER_var;
-  int __CPROVER_var;
+  // Initialize them with `nondet_int` to avoid them being ignored by DFCC.
+  // DFCC ignores variables that are not read/written to outside the loop
+  // or in the loop contracts.
+  int nondet_var = nondet_int();
+  int __VERIFIER_var = nondet_int();
+  int __CPROVER_var = nondet_int();
   for(int i = 10; i > 0; i--)
     // clang-format off
   __CPROVER_assigns(i,nondet_var, __VERIFIER_var, __CPROVER_var)

regression/contracts-dfcc/invar_havoc_dynamic_array_const_idx/main.c

@@ -10,7 +10,7 @@ void main()
   data[4] = 0;
 
   for(unsigned i = 0; i < SIZE; i++)
-    __CPROVER_loop_invariant(i <= SIZE)
+    __CPROVER_assigns(data[1], i) __CPROVER_loop_invariant(i <= SIZE)
     {
       data[1] = i;
     }

regression/contracts-dfcc/invar_loop-entry_check/main.c

@@ -12,7 +12,7 @@ void main()
   x1 = &z1;
 
   while(y1 > 0)
-    __CPROVER_loop_invariant(*x1 == __CPROVER_loop_entry(*x1))
+    __CPROVER_loop_invariant(y1 >= 0 && *x1 == __CPROVER_loop_entry(*x1))
     {
       --y1;
       *x1 = *x1 + 1;
@@ -24,7 +24,7 @@ void main()
   x2 = z2;
 
   while(y2 > 0)
-    __CPROVER_loop_invariant(x2 == __CPROVER_loop_entry(x2))
+    __CPROVER_loop_invariant(y2 >= 0 && x2 == __CPROVER_loop_entry(x2))
     {
       --y2;
       x2 = x2 + 1;
@@ -34,11 +34,12 @@ void main()
 
   int y3;
   s s0, s1, *s2 = &s0;
+  s0.n = malloc(sizeof(int));
   s2->n = malloc(sizeof(int));
   s1.n = s2->n;
 
   while(y3 > 0)
-    __CPROVER_loop_invariant(s2->n == __CPROVER_loop_entry(s2->n))
+    __CPROVER_loop_invariant(y3 >= 0 && s2->n == __CPROVER_loop_entry(s2->n))
     {
       --y3;
       s0.n = s0.n + 1;

regression/contracts-dfcc/invar_loop-entry_check/test.desc

@@ -11,10 +11,10 @@ main.c
 ^\[main.loop_invariant_base.\d+] line 26 Check invariant before entry for loop .*: SUCCESS$
 ^\[main.loop_invariant_step.\d+] line 26 Check invariant after step for loop .*: SUCCESS$
 ^\[main.loop_step_unwinding.\d+] line 26 Check step was unwound for loop .*: SUCCESS$
-^\[main.loop_assigns.\d+] line 40 Check assigns clause inclusion for loop .*: SUCCESS$
-^\[main.loop_invariant_base.\d+] line 40 Check invariant before entry for loop .*: SUCCESS$
-^\[main.loop_invariant_step.\d+] line 40 Check invariant after step for loop .*: SUCCESS$
-^\[main.loop_step_unwinding.\d+] line 40 Check step was unwound for loop .*: SUCCESS$
+^\[main.loop_assigns.\d+] line 41 Check assigns clause inclusion for loop .*: SUCCESS$
+^\[main.loop_invariant_base.\d+] line 41 Check invariant before entry for loop .*: SUCCESS$
+^\[main.loop_invariant_step.\d+] line 41 Check invariant after step for loop .*: SUCCESS$
+^\[main.loop_step_unwinding.\d+] line 41 Check step was unwound for loop .*: SUCCESS$
 ^\[main\.assertion\.\d+\] .* assertion \*x1 == z1: SUCCESS$
 ^\[main\.assertion\.\d+\] .* assertion x2 == z2: SUCCESS$
 ^\[main.assigns.\d+\] .* Check that y1 is assignable: SUCCESS$

regression/contracts-dfcc/invar_loop-entry_fail/main.c

@@ -6,7 +6,7 @@ void main()
   x = z;
 
   while(y > 0)
-    __CPROVER_loop_invariant(x == __CPROVER_loop_entry(x))
+    __CPROVER_loop_invariant(y >= 0 && x == __CPROVER_loop_entry(x))
     {
       --y;
       x = x + 1;

regression/contracts-dfcc/loop_assigns_inference-01/test.desc

@@ -1,18 +1,18 @@
-KNOWNBUG
+CORE dfcc-only
 main.c
---dfcc main --apply-loop-contracts
+--dfcc main --apply-loop-contracts _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[body_1.assigns.\d+\] .* Check that j is assignable: SUCCESS$
 ^\[body_2.assigns.\d+\] .* Check that \*i is assignable: SUCCESS$
 ^\[body_3.assigns.\d+\] .* Check that \*i is assignable: SUCCESS$
 ^\[incr.assigns.\d+\] .* Check that \*i is assignable: SUCCESS$
-^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$
-^\[main.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main.loop_invariant_base.\d+\] line \d+ Check invariant before entry for loop .*: SUCCESS$
+^\[main.loop_invariant_step.\d+\] line \d+ Check invariant after step for loop .*: SUCCESS$
+^\[main.loop_step_unwinding.\d+\] line \d+ Check step was unwound for loop .*: SUCCESS$
 ^\[main.assertion.\d+\] .* assertion j == 9: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 --
 This test checks loop locals are correctly removed during assigns inference so
 that the assign clause is correctly inferred.
-This test failed when using dfcc for loop contracts.

regression/contracts-dfcc/loop_assigns_inference-03/main.c

@@ -7,7 +7,7 @@ void main()
   int b[SIZE];
   for(unsigned i = 0; i < SIZE; i++)
     // clang-format off
-    __CPROVER_loop_invariant(i <= SIZE)
+    __CPROVER_loop_invariant((i == 0 || b[0] == 1) && i <= SIZE)
     // clang-format on
     {
       b[i] = 1;