Label with invariant potentially incorrectly handled

[gauravpartha]

Currently, the following code verifies:

method testLabel(x: Ref)
  requires acc(x.f)
{
  label dummy
    invariant acc(x.f, 1/2)

  assert acc(x.f)
  assert false
}

The semantics of labels with invariants that are not loop heads is not clear, so it's not completely clear to what extent this is an issue (see the on-going discussion at https://github.com/viperproject/silver/issues/296). However, there is currently a test in the test suite that exhibits the same problem and for which Carbon does not verify it (because it should not verify in my opinion): method test03 in https://github.com/viperproject/silver/blob/master/src/test/resources/all/invariants/loops1.vpr (lh1 is not a loop head and Silicon can prove false right after it)

[mschwerhoff]

For documentation purposes, this is the current CFG: