Validity checks fail for local variables when abstracted loops are executed more than one time

[qinheping]

CBMC version: 5.59.0
Operating system: macOS 12.3.1
Exact command line resulting in the issue:

goto-cc main.c
goto-instrument --apply-loop-contracts a.out b.out
goto-instrument --pointer-check b.out c.out
cbmc c.out

I ran the above command lines on the following c program

static void foo() {
  unsigned i;

  for (i = 0; i < 16; i++)
    __CPROVER_loop_invariant(1 == 1) { int v = 1; }

}


static void bar() {
  unsigned i;

  for (i = 0; i < 16; i++)
    __CPROVER_loop_invariant(1 == 1) { int v = 1; }

}

int main() {
  bar();
  foo();
  foo();
}

The result shows that, although the function foo and bar are exactly the same, the validity check of v failed in the function foo but not in bar. This is the report

** Results:
assign.c function bar
[bar.1] line 13 Check loop invariant before entry: SUCCESS
[bar.2] line 13 Check that loop invariant is preserved: SUCCESS
[bar.3] line 13 Check that loop instrumentation was not truncated: SUCCESS
[bar.assigns.2] line 13 Check that i is valid: SUCCESS
[bar.assigns.3] line 13 Check that i is assignable: SUCCESS
[bar.assigns.1] line 14 Check that v is valid: SUCCESS

assign.c function foo
[foo.1] line 4 Check loop invariant before entry: SUCCESS
[foo.2] line 4 Check that loop invariant is preserved: SUCCESS
[foo.3] line 4 Check that loop instrumentation was not truncated: SUCCESS
[foo.assigns.2] line 4 Check that i is valid: SUCCESS
[foo.assigns.3] line 4 Check that i is assignable: SUCCESS
[foo.assigns.1] line 5 Check that v is valid: FAILURE

The validity check checks if v is a dead object, i.e.,

  !(POINTER_OBJECT(&v) == POINTER_OBJECT(__CPROVER_dead_object))

The check happens before the loop body where v is declared. When the abstracted loop is executed for the first time, v is undeclared and not dead, which is the reason why the check success in bar. At the end of the first abstracted loop, v will be dead and set to be a dead object

        // 49 file assign.c line 5 function foo
        ASSIGN __CPROVER_dead_object := (side_effect statement="nondet" is_nondet_nullable="1" ? cast(address_of(foo::1::1::1::v), empty*) : __CPROVER_dead_object)
        // 50 file assign.c line 5 function foo
        DEAD foo::1::1::1::v

Therefore, at the second time we execute the loop, v is not re-declared yet and is dead, that is why the check failed in foo.

A possible fix is not to check validity of local variables at the beginning of loops. @remi-delmas-3000 Do you have any thoughts

[remi-delmas-3000]

This is fixed by this PR #6947