Add support for var variable declarations (#3821)

Author: wadoon

key.core/src/main/java/de/uka/ilkd/key/java/loader/JP2KeYConverter.java

@@ -2158,7 +2158,8 @@ public Object visit(ReceiverParameter n, Void arg) {
 
     @Override
     public Object visit(VarType n, Void arg) {
-        return getKeYJavaType(n.resolve());
+        var kjt = getKeYJavaType(n.resolve());
+        return new TypeRef(kjt);
     }
 
     @Override

key.core/src/main/java/de/uka/ilkd/key/java/loader/JavaParserFactory.java

@@ -16,10 +16,13 @@
 import com.github.javaparser.JavaParser;
 import com.github.javaparser.ParseResult;
 import com.github.javaparser.ParserConfiguration;
+import com.github.javaparser.Processor;
 import com.github.javaparser.ast.CompilationUnit;
+import com.github.javaparser.ast.Node;
 import com.github.javaparser.ast.body.TypeDeclaration;
 import com.github.javaparser.ast.key.sv.KeyContextStatementBlock;
 import com.github.javaparser.ast.stmt.BlockStmt;
+import com.github.javaparser.ast.validator.postprocessors.Java10PostProcessor;
 import com.github.javaparser.resolution.Navigator;
 import com.github.javaparser.resolution.TypeSolver;
 import com.github.javaparser.resolution.declarations.ResolvedReferenceTypeDeclaration;
@@ -95,6 +98,14 @@ private ParserConfiguration getConfiguration() {
             config.setStoreTokens(true);
         }
         config.setLanguageLevel(ParserConfiguration.LanguageLevel.RAW);
+        config.getProcessors().add(() -> new Processor() {
+            @Override
+            public void postProcess(ParseResult<? extends Node> result,
+                    ParserConfiguration configuration) {
+                var pp = new Java10PostProcessor();
+                pp.postProcess(result, configuration);
+            }
+        });
         config.setSymbolResolver(getSymbolSolver());
         return config;
     }

key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProofCollections.java

@@ -652,6 +652,7 @@ public static ProofCollection automaticJavaDL() throws IOException {
         g.provable("../../key.core/src/test/resources/testcase/classpath/classpath.key");
         g.notprovable("heap/inconsistent_represents/MyClass_m.key");
         g.notprovable("heap/inconsistent_represents/MyClass_n.key");
+        g.provable("standard_key/java_dl/typeInference.key");
 
 
         g = c.group("FOL");

key.ui/examples/standard_key/java_dl/typeInference.key

@@ -0,0 +1,19 @@
+\settings {
+    "Strategy": {
+        "options" : {
+            "QUERYAXIOM_OPTIONS_KEY" : "QUERYAXIOM_ON",
+            "QUERY_NEW_OPTIONS_KEY" : "QUERY_ON"
+        }
+    }
+}
+
+\javaSource "typeInference_java/";
+
+\programVariables {
+    int _a;
+    int _b;
+}
+
+\problem {
+    _a + _b + 3 = TypeInference.m(_a, _b)
+}

key.ui/examples/standard_key/java_dl/typeInference_java/TypeInference.java

@@ -0,0 +1,7 @@
+class TypeInference {
+    static int m(int a, int b) {
+        var x = a + 1;
+        final var y = b + 2;
+        return x + y;
+    }
+}