diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/adt/SeqPut.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/adt/SeqPut.java new file mode 100644 index 00000000000..5c535cdaf44 --- /dev/null +++ b/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); + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/SetStatement.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/SetStatement.java new file mode 100644 index 00000000000..3ab88075bb0 --- /dev/null +++ b/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); + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/loader/JP2KeYConverter.java b/key.core/src/main/java/de/uka/ilkd/key/java/loader/JP2KeYConverter.java index 6044caf6cbd..fac68f9cf5c 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/loader/JP2KeYConverter.java +++ b/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;}}; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/ldt/HeapLDT.java b/key.core/src/main/java/de/uka/ilkd/key/ldt/HeapLDT.java index 2cebba1bcb4..c15e09b58a1 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/ldt/HeapLDT.java +++ b/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::"); - initialized = addFunction(services, "java.lang.Object::"); - classPrepared = addSortDependingFunction(services, ""); - classInitialized = addSortDependingFunction(services, ""); + 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, ""); - classErroneous = addSortDependingFunction(services, ""); + addSortDependingFunction(services, "#$classInitializationInProgress"); + classErroneous = addSortDependingFunction(services, "#$classErroneous"); length = addFunction(services, "length"); nullFunc = addFunction(services, "null"); acc = addFunction(services, "acc"); diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/ProblemInitializer.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/ProblemInitializer.java index 628fcc372ef..ffec8abb9cf 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/ProblemInitializer.java +++ b/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++; diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/io/KeYFile.java b/key.core/src/main/java/de/uka/ilkd/key/proof/io/KeYFile.java index 4183ce52604..58bfc815ab7 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/io/KeYFile.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/io/KeYFile.java @@ -352,6 +352,7 @@ protected ProblemFinder getProblemFinder() { * initial configuration */ public Collection 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 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 readFuncAndPred() { * @return list of issues that occurred during parsing the taclets */ public List readRules() { + LOGGER.debug("Activate rules of {}", file); KeyAst.File ctx = getParseContext(); TacletPBuilder visitor = new TacletPBuilder(initConfig.getServices(), initConfig.namespaces(), initConfig.getTaclet2Builder()); diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/String.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/String.key index e845b8c4ad6..c35d5e89ca3 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/String.key +++ b/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 */ diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/ldt.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/ldt.key index e18a4e1721b..9f5e389c649 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/ldt.key +++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/ldt.key @@ -23,6 +23,7 @@ permission, reach, seq, + stringDef, map, freeADT, wellfound, diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/stringDef.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/stringDef.key new file mode 100644 index 00000000000..aa43ea9c7c6 --- /dev/null +++ b/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); +} diff --git a/key.core/src/test/java/de/uka/ilkd/key/speclang/SetStatementTest.java b/key.core/src/test/java/de/uka/ilkd/key/speclang/SetStatementTest.java index 88caedb1306..18236aaeb05 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/speclang/SetStatementTest.java +++ b/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"); }