Assignable free

[flo2702]

This branch implements assignable_free clauses, which akin to ensures_free allow you to specify frame conditions that the caller can assume but the callee does not have to prove. See #3185.

assignable_free clauses are implemented for functional method contracts, functional block/loop contracts, and loop invariants.

Semantics

Consider the following example.

/*@ public normal_behavior
  @ ensures field == 21; */
void foo() {
  field = 21;
  bar();
}

/*@ public normal_behavior
  @ ensures true; 
  @ assignable \nothing;
  @ assignable_free field; */
void bar() {
  field = 42;
}

Both contracts are provable: The proof obligation for bar() must show that only field is modified, but then when bar() is called from foo(), foo() assumes that bar() modifies \nothing.

In general, the caller assumes that the callee only modifies the locations mentioned in its assignable clause(s), while the callee must prove that it only modifies the locations in the union of its assignable and assignable_free clauses.

[github-actions]

Thank you for your contribution.

The test artifacts are available on Artiweb.
The newest artifact is here.

[codecov]

Codecov Report

Merging #3188 (91abedd) into main (c482269) will increase coverage by 0.01%.
The diff coverage is 45.81%.

@@             Coverage Diff              @@
##               main    #3188      +/-   ##
============================================
+ Coverage     37.59%   37.61%   +0.01%     
- Complexity    16684    16709      +25     
============================================
  Files          2043     2043              
  Lines        125713   125902     +189     
  Branches      21106    21138      +32     
============================================
+ Hits          47257    47353      +96     
- Misses        72693    72770      +77     
- Partials       5763     5779      +16     

Impacted Files	Coverage Δ
...ilkd/key/proof/init/FunctionalBlockContractPO.java	0.00% <0.00%> (ø)
.../ilkd/key/proof/init/FunctionalLoopContractPO.java	0.00% <0.00%> (ø)
...e/uka/ilkd/key/rule/AbstractLoopInvariantRule.java	5.11% <0.00%> (-0.25%)	⬇️
...de/uka/ilkd/key/rule/LoopContractInternalRule.java	9.47% <0.00%> (-0.21%)	⬇️
...va/de/uka/ilkd/key/speclang/AuxiliaryContract.java	45.73% <ø> (ø)
...ava/de/uka/ilkd/key/speclang/LoopContractImpl.java	0.00% <0.00%> (ø)
...lkd/key/speclang/dl/translation/DLSpecFactory.java	0.00% <ø> (ø)
...va/de/uka/ilkd/key/speclang/BlockContractImpl.java	28.88% <29.41%> (-2.07%)	⬇️
.../key/proof/init/FunctionalOperationContractPO.java	54.76% <30.00%> (-3.23%)	⬇️
.../key/speclang/FunctionalOperationContractImpl.java	42.54% <36.36%> (-0.04%)	⬇️
... and 14 more

... and 1 file with indirect coverage changes

📣 We’re building smart automated test selection to slash your CI/CD build times. Learn more

[mattulbrich]

Rather a large addition to the code. Thanks for your efforts.