wip

key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/adt/SeqPut.java

@@ -0,0 +1,50 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package de.uka.ilkd.key.java.ast.expression.operator.adt;
+
+import de.uka.ilkd.key.java.Services;
+import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType;
+import de.uka.ilkd.key.java.ast.abstraction.PrimitiveType;
+import de.uka.ilkd.key.java.ast.expression.Operator;
+import de.uka.ilkd.key.java.ast.reference.ExecutionContext;
+import de.uka.ilkd.key.java.visitor.Visitor;
+
+import org.key_project.util.ExtList;
+
+public class SeqPut extends Operator {
+
+    public SeqPut(ExtList children) {
+        super(children);
+    }
+
+
+    @Override
+    public int getPrecedence() {
+        return 0;
+    }
+
+
+    @Override
+    public int getNotation() {
+        return PREFIX;
+    }
+
+
+    @Override
+    public void visit(Visitor v) {
+        v.performActionOnSeqPut(this);
+    }
+
+
+    @Override
+    public int getArity() {
+        return 3;
+    }
+
+
+    @Override
+    public KeYJavaType getKeYJavaType(Services javaServ, ExecutionContext ec) {
+        return javaServ.getJavaInfo().getKeYJavaType(PrimitiveType.JAVA_SEQ);
+    }
+}

key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/SetStatement.java

@@ -0,0 +1,78 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package de.uka.ilkd.key.java.ast.statement;
+
+import de.uka.ilkd.key.java.ast.PositionInfo;
+import de.uka.ilkd.key.java.ast.ProgramElement;
+import de.uka.ilkd.key.java.visitor.Visitor;
+import de.uka.ilkd.key.nparser.KeyAst.SetStatementContext;
+
+
+
+/**
+ * JML set statement
+ *
+ * @author Julian Wiesler
+ */
+public class SetStatement extends JavaStatement {
+
+    /**
+     * The target of the assignment as a term. Either a heap access for a ghost field
+     * or a ghost variable.
+     */
+    public static int INDEX_TARGET = 0;
+
+    /**
+     * The value of the assignment as a term.
+     */
+    public static int INDEX_VALUE = 1;
+
+    /**
+     * The parser context of the statement produced during parsing.
+     */
+    private final SetStatementContext context;
+
+    /** Constructor used in recoderext */
+    public SetStatement(SetStatementContext context, PositionInfo positionInfo) {
+        super(positionInfo);
+        this.context = context;
+    }
+
+    /** Constructor used when cloning */
+    public SetStatement(SetStatement copyFrom) {
+        this(copyFrom.context, copyFrom.getPositionInfo());
+    }
+
+
+    /**
+     * Removes the attached parser context from this set statement
+     *
+     * @return the parser context that was attached
+     */
+    public SetStatementContext getParserContext() {
+        return context;
+    }
+
+
+    /** {@inheritDoc} */
+    @Override
+    public void visit(Visitor v) {
+        v.performActionOnSetStatement(this);
+    }
+
+    @Override
+    public int getChildCount() {
+        return 0;
+    }
+
+    @Override
+    public ProgramElement getChildAt(int index) {
+        throw new IndexOutOfBoundsException("SetStatement has no program children");
+    }
+
+    @Override
+    protected int computeHashCode() {
+        return System.identityHashCode(this);
+    }
+}

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

@@ -1356,7 +1356,9 @@ public Object visit(ImportDeclaration n, Void arg) {
 
     @Override
     public Object visit(Modifier n, Void arg) {
-        var pi=createPositionInfo(n);var c=createComments(n);var k=n.getKeyword();return switch(k){case PUBLIC->new Public(pi,c);case PROTECTED->new Protected(pi,c);case PRIVATE->new Private(pi,c);case ABSTRACT->new Abstract(pi,c);case STATIC->new Static(pi,c);case FINAL->new Final(pi,c);case TRANSIENT->new Transient(pi,c);case VOLATILE->new Volatile(pi,c);case SYNCHRONIZED->new Synchronized(pi,c);case NATIVE->new Native(pi,c);case STRICTFP->new StrictFp(pi,c);case GHOST->new Ghost(pi,c);case MODEL->new Model(pi,c);case TWO_STATE->new TwoState(pi,c);case NO_STATE->new NoState(pi,c);default->{reportUnsupportedElement(n);yield null;}};
+        var pi=createPositionInfo(n);var c=createComments(n);var k=n.getKeyword();return switch(k){case PUBLIC->new Public(pi,c);case PROTECTED->new Protected(pi,c);case PRIVATE->new Private(pi,c);case ABSTRACT->new Abstract(pi,c);case STATIC->new Static(pi,c);case FINAL->new Final(pi,c);case TRANSIENT->new Transient(pi,c);case VOLATILE->new Volatile(pi,c);case SYNCHRONIZED->new Synchronized(pi,c);case NATIVE->new Native(pi,c);case STRICTFP->new StrictFp(pi,c);
+            case GHOST->new Ghost(pi,c);
+            case MODEL->new Model(pi,c);case TWO_STATE->new TwoState(pi,c);case NO_STATE->new NoState(pi,c);default->{reportUnsupportedElement(n);yield null;}};
     }
 
 

key.core/src/main/java/de/uka/ilkd/key/ldt/HeapLDT.java

@@ -98,13 +98,13 @@ public HeapLDT(TermServices services) {
         anon = addFunction(services, "anon");
         memset = addFunction(services, "memset");
         arr = addFunction(services, "arr");
-        created = addFunction(services, "java.lang.Object::<created>");
-        initialized = addFunction(services, "java.lang.Object::<initialized>");
-        classPrepared = addSortDependingFunction(services, "<classPrepared>");
-        classInitialized = addSortDependingFunction(services, "<classInitialized>");
+        created = addFunction(services, "java.lang.Object::#$created");
+        initialized = addFunction(services, "java.lang.Object::#$initialized");
+        classPrepared = addSortDependingFunction(services, "#$classPrepared");
+        classInitialized = addSortDependingFunction(services, "#$classInitialized");
         classInitializationInProgress =
-            addSortDependingFunction(services, "<classInitializationInProgress>");
-        classErroneous = addSortDependingFunction(services, "<classErroneous>");
+            addSortDependingFunction(services, "#$classInitializationInProgress");
+        classErroneous = addSortDependingFunction(services, "#$classErroneous");
         length = addFunction(services, "length");
         nullFunc = addFunction(services, "null");
         acc = addFunction(services, "acc");

key.core/src/main/java/de/uka/ilkd/key/proof/init/ProblemInitializer.java

@@ -163,8 +163,8 @@ private void readLDTIncludes(Includes in, InitConfig initConfig) throws ProofInp
 
         int i = 0;
         reportStatus("Read LDT Includes", in.getIncludes().size());
-        for (String name : in.getLDTIncludes()) {
 
+        for (String name : in.getLDTIncludes()) {
             keyFile[i] =
                 new KeYFile(name, in.get(name), progMon, initConfig.getProfile(), fileRepo);
             i++;

key.core/src/main/java/de/uka/ilkd/key/proof/io/KeYFile.java

@@ -352,6 +352,7 @@ protected ProblemFinder getProblemFinder() {
      * initial configuration
      */
     public Collection<PositionedString> readSorts() {
+        LOGGER.debug("Activate Sorts of {}", file);
         KeyAst.File ctx = getParseContext();
         KeyIO io = new KeyIO(initConfig.getServices(), initConfig.namespaces());
         io.evalDeclarations(ctx);
@@ -373,6 +374,7 @@ public List<PositionedString> readFuncAndPred() {
         if (file == null) {
             return null;
         }
+        LOGGER.debug("Activate functions and predicates of {}", file);
         KeyAst.File ctx = getParseContext();
         KeyIO io = new KeyIO(initConfig.getServices(), initConfig.namespaces());
         io.evalFuncAndPred(ctx);
@@ -387,6 +389,7 @@ public List<PositionedString> readFuncAndPred() {
      * @return list of issues that occurred during parsing the taclets
      */
     public List<BuildingIssue> readRules() {
+        LOGGER.debug("Activate rules of {}", file);
         KeyAst.File ctx = getParseContext();
         TacletPBuilder visitor = new TacletPBuilder(initConfig.getServices(),
             initConfig.namespaces(), initConfig.getTaclet2Builder());

key.core/src/main/resources/de/uka/ilkd/key/proof/rules/String.key

@@ -1,8 +1,3 @@
-\functions {
-  Seq strContent(java.lang.String);
-  java.lang.String strPool(Seq);
-}
-
 /*
  * Program Rules for Strings
  */

key.core/src/main/resources/de/uka/ilkd/key/proof/rules/ldt.key

@@ -23,6 +23,7 @@
     permission,
     reach,
     seq,
+    stringDef,
     map,
     freeADT,
     wellfound,

key.core/src/main/resources/de/uka/ilkd/key/proof/rules/stringDef.key

@@ -0,0 +1,8 @@
+\sorts {
+	java.lang.String \extends java.lang.Object;
+}
+
+\functions {
+  Seq strContent(java.lang.String);
+  java.lang.String strPool(Seq);
+}

key.core/src/test/java/de/uka/ilkd/key/speclang/SetStatementTest.java

@@ -68,8 +68,7 @@ public class SetStatementTest {
     @BeforeEach
     public synchronized void setUp() {
         if (javaInfo == null) {
-            javaInfo =
-                HelperClassForTests.parse(new File(TEST_FILE)).getFirstProof().getJavaInfo();
+            javaInfo = HelperClassForTests.parse(new File(TEST_FILE)).getFirstProof().getJavaInfo();
             services = javaInfo.getServices();
             testClassType = javaInfo.getKeYJavaType("testPackage.TestClass");
         }