Taclet option for checking overflows (in Java code) does not work

[WolframPfeifer]

Description

In the current version of KeY, the integer semantics with explicit overflow checks as introduced by #3027 are broken on at least 3 levels:

1. The annotation `/*@ code_safe_math */ is ignored and does not change the taclet option (as I expected). However, it is parsed without an error and seems to be simply ignored.
2. After manually setting the taclet option via the menu (and starting the proof again as always), the option for checking overflows is completely ignored, no additional branches for overflow checks are created. Proofs created with intRules:arithmeticSemanticsCheckingOF are exactly identical to those with intRules:arithmeticSemanticsIgnoringOF. In the rule files of key, introduction of the additional branches is guarded by intRules:checkedOverflow, which of course does not exist. Using an undeclared taclet option in any rule file should really throw an error in the GUI!
3. After repairing point 2, the additional branches for overflow checks are generated, but instantly closed, since inRange(...) is always rewritten to true!

Furthermore, there is no documentation of the final solution (description of what has been implemented in #3014 and #3027). The implemented solution deviates from the description in the wiki (https://github.com/KeYProject/key/wiki/Spec-math-modes). We really should have a user-level documentation in key-docs.

I am a bit shocked that such a major point of KeY was apparently not even tested manually and survived for half a year. We really should have unit tests here, e.g. a small proof obligation (in a key file) for each of the options that is only provable if the correct semantics are used.

Reproducible

always

Steps to reproduce

1. Load the following class:

/*@ spec_bigint_math */
/*@ code_safe_math */   // this seems to be ignored by KeY
class Overflow {
  /*@ normal_behavior
    @  ensures \result == x + y;
    @*/
  int add(int x, int y) {
      return x + y;
  }
}

2. Start the proof of the contract.
3. Run the automatic proof search.

The proof is closed instantly, while it should have an additional (unprovable) branch containing the overflow check for +. This is not the case due to point 1 in the above list.

4. Manually set the taclet option for overflow checking via the GUI (workaround for point 1).
5. Reload the file and start the proof.
6. Run the automatic proof search.

Again, the proof is closed. Now it contains the additional branch for overflow checking. However, this branch is closed, which should not be the case, since the specification uses (unbounded) bigints, while the code potentially has an overflow.