Statement contracts with "abrupt" entry

[vprevosto]

ACSL introduces clauses for statement contracts in order to deal with an "abrupt" exit out of the block on which the contract applies through a break, goto, return or exit. In addition, ensures are not necessarily verified in such a case. On the other hand, nothing is said about the validity of the contract if the block is entered via a jump to an arbitrary statement, as in the following example:

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

What can we say about such a contract?

[maroneze]

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: ;
    }
  }
}

[pbaudin]

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.