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 viperproject/silver#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:

[JonasAlaif]

@marcoeilers could you fix this please. I want to use the labels with invariants feature in Prusti, but doing that is pretty scary with a footgun like this. E.g. see Dios example for how easy it is to be unsound.

[marcoeilers]

I'm keeping this open since it's still unclear what the semantics of labels with invariants that are not loop heads should be.
However, since viperproject/silver#859, labels with invariants that aren't loop head are no longer marked as loop heads in the CFG. As a result, Silicon no longer allows proving false in the example above, and Silicon and Carbon behave identically on all examples I'm aware of.

[marcoeilers]

Oh, never mind, seems like there is a Silver issue to discuss whether such labels should actually be allowed (and what they mean if they are): viperproject/silver#296. So I'll close this, since the clearly wrong behavior in Silicon is fixed now.