Statement contracts with "abrupt" entry about acsl HOT 2 OPEN

On a related note, it might be worth clarifying what is meant in Section 1.2, about Statement annotations. It says that, for statement contracts, "Semantic conditions must be checked (no goto going inside, no goto going outside)." From that phrase, it would seem that gotos forfeit the meaning of statement contracts, but in section 2.4.4 it is only said that ensures are not checked when leaving via a goto. So, for symmetry, it might be meaningful to say that requires are not checked when entering via a goto.

Also, here's another example with gotos, where we enter 2 blocks at a time. It's possibly just an extension of the previous example, but it may lead to some more complex cases that it would be better not to forget about.

void f() {
  int x = 0;
  x = 1;
  goto L2;
  /*@ requires x == 1;
      ensures x == 3;
  */
  {
    x = 2;
   L1 :
    /*@ requires x == 0 || x == 2;
        ensures x == 3;
    */
    {
      x = 3;
      goto L3;
     L2: 
      x = 0;
      goto L1;
     L3: ;
    }
  }
}

from acsl.

Assigns clauses have also to be considered.

Notice that they are not considered as the ensures : [section 2.4.4] the locations having their value
modified during the path execution, starting at the beginning of the annotated statement
and leading to a goto jumping out of it, should be part of its assigns clause

The next similar question is what about abrupt loop entry.

from acsl.