[wadoon]

Intended Change

This PR adds support for the simple form of the instanceof pattern types that came in Java 16: <expr> instanceof <Type> <var>.

Please consult: JLS 6.3.1 for the binding rules.

Plan

• Add AST and translation support
• Add first rules
• Make the rules parseable
• Discuss flow analysis as varcond.
• Add the more complex rules for while, for, do.
• Example
• Git history cleanup

Type of pull request

• New feature (non-breaking change which adds functionality)
• There are changes to the (Java) code
• There are changes to the taclet rule base

Ensuring quality

• I made sure that introduced/changed code is well documented (javadoc and inline comments).
• I made sure that new/changed end-user features are well documented (https://github.com/KeYProject/key-docs).
• I added new test case(s) for new functionality.

[wadoon]

State of PR 3976 zu instanceof:

• added varcond `isBindingExpr(#expression, #posBinding, #negBindings) (true iff one of the bindings is not empty)
• added varcond alwaysAbnormallyTerminates(#stmts) (true iff #stmts are never reaches the natural end, e.g., if(x) { assert false; }) under-approximation
• added rule: ifElseUnfoldPattern, ifUnfoldPatternUnreachable, ifElseUnfoldPattern
• General-Idea: if(#bnse) #slist1 else #slist2 ~~~~~> boolean #boolv; {#boolv = #bnse} if(#bnse) { #posBinding; #slist1} else {#negBinding; #slist2}
• added rules for #boolv = #nse instanceof #T #id which does not match.

Todo:

• forbid \ifElseUnfold for binding expressions

[unp1]

Hi,

• added rules for #boolv = #nse instanceof #T #id which does not match.

The rule matches for me in the example below:

 /*@ normal_behavior
      @ requires obj != null;
      @ ensures \result instanceof String;
      @*/
    public static Object getString(Object obj) {
        return "ha";
    }

    /*@ normal_behavior
      @ requires obj != null;
      @ ensures \result;
      @*/
    public static boolean isString(Object obj) {
        boolean result = getString(obj) instanceof String id;
        return result;
    }

I added the example and a minor fix (replacewith of the instance_eval_id taclet)