Commit bb5d43b8 authored by Alexander Weigl's avatar Alexander Weigl
Browse files

Merge branch 'weigl/kp2' into 'master'

Renovating the KeY Parser

Closes #1558, #991, #1540, #1547, #1528, and #1525

See merge request key/key!278
parents 09f80284 f7b43a54
distributionBase=GRADLE_USER_HOME
distributionPath=wrapper/dists
distributionUrl=https\://services.gradle.org/distributions/gradle-5.4.1-bin.zip
distributionUrl=https\://services.gradle.org/distributions/gradle-6.6-bin.zip
zipStoreBase=GRADLE_USER_HOME
zipStorePath=wrapper/dists
......@@ -86,12 +86,14 @@ import de.uka.ilkd.key.util.HelperClassForTests;
import de.uka.ilkd.key.util.KeYConstants;
import junit.framework.TestCase;
import static org.junit.Assert.*;
/**
* Provides the basic functionality of {@link TestCase}s which tests
* the symbolic execution features.
* @author Martin Hentschel
*/
public abstract class AbstractSymbolicExecutionTestCase extends TestCase {
public abstract class AbstractSymbolicExecutionTestCase {
/**
* <p>
* If this constant is {@code true} a temporary directory is created with
......@@ -2049,15 +2051,15 @@ public abstract class AbstractSymbolicExecutionTestCase extends TestCase {
* @return The original settings which are overwritten.
*/
public static HashMap<String, String> setDefaultTacletOptions() {
HashMap<String,String> original = HelperClassForTests.setDefaultTacletOptions();
// set non modular reasoning
System.out.println(ProofSettings.DEFAULT_SETTINGS);
ChoiceSettings choiceSettings = ProofSettings.DEFAULT_SETTINGS.getChoiceSettings();
System.out.println(choiceSettings);
ImmutableSet<Choice> cs = DefaultImmutableSet.nil();
cs = cs.add(new Choice("noRestriction", "methodExpansion"));
choiceSettings.updateWith(cs);
return original;
HashMap<String, String> original = HelperClassForTests.setDefaultTacletOptions();
// set non modular reasoning
//System.out.println(ProofSettings.DEFAULT_SETTINGS);
ChoiceSettings choiceSettings = ProofSettings.DEFAULT_SETTINGS.getChoiceSettings();
//System.out.println(choiceSettings);
ImmutableSet<Choice> cs = DefaultImmutableSet.nil();
cs = cs.add(new Choice("noRestriction", "methodExpansion"));
choiceSettings.updateWith(cs);
return original;
}
/**
......
......@@ -9,6 +9,8 @@ import de.uka.ilkd.key.symbolic_execution.model.IExecutionNode;
import de.uka.ilkd.key.symbolic_execution.model.IExecutionStart;
import de.uka.ilkd.key.symbolic_execution.model.IExecutionVariable;
import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionEnvironment;
import static org.junit.Assert.*;
import org.junit.Test;
/**
* Tests the conditional values provided by {@link IExecutionNode#getVariables(de.uka.ilkd.key.logic.Term)}.
......@@ -19,7 +21,7 @@ public class TestConditionalVariables extends AbstractSymbolicExecutionTestCase
* Compares the conditional values on the {@code Number} example.
* @throws Exception Occurred Exception.
*/
public void testVariablesUnderMethodReturnCondition() throws Exception {
@Test public void testVariablesUnderMethodReturnCondition() throws Exception {
SymbolicExecutionEnvironment<DefaultUserInterfaceControl> env = doSETTest(testCaseDirectory,
"/set/conditionalVariables/test/Number.java",
"Number",
......
......@@ -30,6 +30,8 @@ import de.uka.ilkd.key.symbolic_execution.ExecutionNodeReader.KeYlessStatement;
import de.uka.ilkd.key.symbolic_execution.model.IExecutionNode;
import de.uka.ilkd.key.symbolic_execution.model.impl.ExecutionStart;
import de.uka.ilkd.key.symbolic_execution.model.impl.TreeSettings;
import static org.junit.Assert.*;
import org.junit.Test;
/**
* Tests for {@link ExecutionNodePreorderIterator}.
......@@ -39,7 +41,7 @@ public class TestExecutionNodePreorderIterator extends TestCase {
/**
* Tests a tree of {@link IExecutionNode}s with three levels after root.
*/
public void testNodesThreeLevel() throws ProofInputException {
@Test public void testNodesThreeLevel() throws ProofInputException {
// Create tree to test
Proof proof = new Proof("target", new InitConfig(new Services(AbstractProfile.getDefaultProfile())));
Node root = appendRoot(proof);
......@@ -84,7 +86,7 @@ public class TestExecutionNodePreorderIterator extends TestCase {
/**
* Tests a tree of {@link IExecutionNode}s with two levels after root.
*/
public void testNodesTwoLevel() throws ProofInputException {
@Test public void testNodesTwoLevel() throws ProofInputException {
// Create tree to test
Proof proof = new Proof("target", new InitConfig(new Services(AbstractProfile.getDefaultProfile())));
Node root = appendRoot(proof);
......@@ -121,7 +123,7 @@ public class TestExecutionNodePreorderIterator extends TestCase {
/**
* Tests a tree of {@link IExecutionNode}s with one level after root.
*/
public void testNodesOneLevel() throws ProofInputException {
@Test public void testNodesOneLevel() throws ProofInputException {
// Create tree to test
Proof proof = new Proof("target", new InitConfig(new Services(AbstractProfile.getDefaultProfile())));
Node root = appendRoot(proof);
......@@ -155,7 +157,7 @@ public class TestExecutionNodePreorderIterator extends TestCase {
/**
* Tests only a root {@link IExecutionNode}.
*/
public void testEmptyRoot() throws ProofInputException {
@Test public void testEmptyRoot() throws ProofInputException {
// Create tree to test
Proof proof = new Proof("target", new InitConfig(new Services(AbstractProfile.getDefaultProfile())));
Node root = appendRoot(proof);
......
......@@ -50,6 +50,10 @@ import de.uka.ilkd.key.symbolic_execution.ExecutionNodeWriter;
import de.uka.ilkd.key.symbolic_execution.model.IExecutionConstraint;
import de.uka.ilkd.key.symbolic_execution.model.IExecutionNode;
import de.uka.ilkd.key.symbolic_execution.model.IExecutionTermination.TerminationKind;
import static org.junit.Assert.*;
import org.junit.Test;
import static org.junit.Assert.*;
import org.junit.Test;
/**
* Tests {@link ExecutionNodeWriter} and {@link ExecutionNodeReader}
......@@ -59,56 +63,56 @@ public class TestExecutionNodeWriterAndReader extends TestCase {
/**
* Tests the reading and writing process without variables and without call stack.
*/
public void testWritingAndReading_withoutVariables_and_withoutCallStack_withReturnValues() throws ProofInputException, ParserConfigurationException, SAXException, IOException {
@Test public void testWritingAndReading_withoutVariables_and_withoutCallStack_withReturnValues() throws ProofInputException, ParserConfigurationException, SAXException, IOException {
doTestWritingAndReading(false, false, true, true);
}
/**
* Tests the reading and writing process without call stack.
*/
public void testWritingAndReading_withoutCallStack_withReturnValues() throws ProofInputException, ParserConfigurationException, SAXException, IOException {
@Test public void testWritingAndReading_withoutCallStack_withReturnValues() throws ProofInputException, ParserConfigurationException, SAXException, IOException {
doTestWritingAndReading(true, false, true, true);
}
/**
* Tests the reading and writing process without variables.
*/
public void testWritingAndReading_withoutVariables_withReturnValues() throws ProofInputException, ParserConfigurationException, SAXException, IOException {
@Test public void testWritingAndReading_withoutVariables_withReturnValues() throws ProofInputException, ParserConfigurationException, SAXException, IOException {
doTestWritingAndReading(false, true, true, true);
}
/**
* Tests the reading and writing process.
*/
public void testWritingAndReading_withReturnValues() throws ProofInputException, ParserConfigurationException, SAXException, IOException {
@Test public void testWritingAndReading_withReturnValues() throws ProofInputException, ParserConfigurationException, SAXException, IOException {
doTestWritingAndReading(true, true, true, true);
}
/**
* Tests the reading and writing process without variables and without call stack.
*/
public void testWritingAndReading_withoutVariables_and_withoutCallStack_noReturnValues() throws ProofInputException, ParserConfigurationException, SAXException, IOException {
@Test public void testWritingAndReading_withoutVariables_and_withoutCallStack_noReturnValues() throws ProofInputException, ParserConfigurationException, SAXException, IOException {
doTestWritingAndReading(false, false, false, true);
}
/**
* Tests the reading and writing process without call stack.
*/
public void testWritingAndReading_withoutCallStack_noReturnValues() throws ProofInputException, ParserConfigurationException, SAXException, IOException {
@Test public void testWritingAndReading_withoutCallStack_noReturnValues() throws ProofInputException, ParserConfigurationException, SAXException, IOException {
doTestWritingAndReading(true, false, false, false);
}
/**
* Tests the reading and writing process without variables.
*/
public void testWritingAndReading_withoutVariables_noReturnValues() throws ProofInputException, ParserConfigurationException, SAXException, IOException {
@Test public void testWritingAndReading_withoutVariables_noReturnValues() throws ProofInputException, ParserConfigurationException, SAXException, IOException {
doTestWritingAndReading(false, true, false, true);
}
/**
* Tests the reading and writing process.
*/
public void testWritingAndReading_noReturnValues() throws ProofInputException, ParserConfigurationException, SAXException, IOException {
@Test public void testWritingAndReading_noReturnValues() throws ProofInputException, ParserConfigurationException, SAXException, IOException {
doTestWritingAndReading(true, true, false, false);
}
......
package de.uka.ilkd.key.symbolic_execution.testcase;
import org.junit.FixMethodOrder;
import org.junit.Test;
import org.junit.runners.MethodSorters;
import de.uka.ilkd.key.symbolic_execution.ExecutionVariableExtractor;
......@@ -14,6 +15,7 @@ public class TestExecutionVariableExtractor extends AbstractSymbolicExecutionTes
/**
* Tests example: /set/variablesEmptyArrayCreationTest
*/
@Test
public void testVariablesEmptyArrayCreationTest() throws Exception {
doSETTestAndDispose(testCaseDirectory,
"/set/variablesEmptyArrayCreationTest/test/EmptyArrayCreationTest.java",
......@@ -41,7 +43,7 @@ public class TestExecutionVariableExtractor extends AbstractSymbolicExecutionTes
/**
* Tests example: /set/variablesNonSimpleArrayCreationTest
*/
public void testVariablesNonSimpleArrayCreationTest() throws Exception {
@Test public void testVariablesNonSimpleArrayCreationTest() throws Exception {
doSETTestAndDispose(testCaseDirectory,
"/set/variablesNonSimpleArrayCreationTest/test/NonSimpleArrayCreationTest.java",
"NonSimpleArrayCreationTest",
......@@ -68,7 +70,7 @@ public class TestExecutionVariableExtractor extends AbstractSymbolicExecutionTes
/**
* Tests example: /set/variablesNonSimpleArrayAssignmentTest
*/
public void testVariablesNonSimpleArrayAssignmentTest() throws Exception {
@Test public void testVariablesNonSimpleArrayAssignmentTest() throws Exception {
doSETTestAndDispose(testCaseDirectory,
"/set/variablesNonSimpleArrayAssignmentTest/test/NonSimpleArrayAssignmentTest.java",
"NonSimpleArrayAssignmentTest",
......@@ -95,7 +97,7 @@ public class TestExecutionVariableExtractor extends AbstractSymbolicExecutionTes
/**
* Tests example: /set/variablesArrayCreationInstanceTest
*/
public void testVariablesArrayCreationInstanceTest() throws Exception {
@Test public void testVariablesArrayCreationInstanceTest() throws Exception {
doSETTestAndDispose(testCaseDirectory,
"/set/variablesArrayCreationInstanceTest/test/ArrayCreationInstanceTest.java",
"ArrayCreationInstanceTest",
......@@ -122,7 +124,7 @@ public class TestExecutionVariableExtractor extends AbstractSymbolicExecutionTes
/**
* Tests example: /set/variablesArrayAssignmentTest
*/
public void testVariablesArrayAssignmentTest() throws Exception {
@Test public void testVariablesArrayAssignmentTest() throws Exception {
doSETTestAndDispose(testCaseDirectory,
"/set/variablesArrayAssignmentTest/test/ArrayAssignmentTest.java",
"ArrayAssignmentTest",
......@@ -149,7 +151,7 @@ public class TestExecutionVariableExtractor extends AbstractSymbolicExecutionTes
/**
* Tests example: /set/variablesArrayCreationTest
*/
public void testVariablesArrayCreationTest() throws Exception {
@Test public void testVariablesArrayCreationTest() throws Exception {
doSETTestAndDispose(testCaseDirectory,
"/set/variablesArrayCreationTest/test/ArrayCreationTest.java",
"ArrayCreationTest",
......@@ -176,7 +178,7 @@ public class TestExecutionVariableExtractor extends AbstractSymbolicExecutionTes
/**
* Tests example: /set/variableVariableMethodContractTest
*/
public void testVariableMethodContractTest() throws Exception {
@Test public void testVariableMethodContractTest() throws Exception {
doSETTest(testCaseDirectory,
"/set/variableVariableMethodContractTest/test/VariableMethodContractTest.java",
"VariableMethodContractTest",
......@@ -203,7 +205,7 @@ public class TestExecutionVariableExtractor extends AbstractSymbolicExecutionTes
/**
* Tests example: /set/variablesConditionalCycle
*/
public void testVariablesConditionalCycle() throws Exception {
@Test public void testVariablesConditionalCycle() throws Exception {
doSETTest(testCaseDirectory,
"/set/variablesConditionalCycle/test/VariablesConditionalCycle.java",
"VariablesConditionalCycle",
......@@ -230,7 +232,7 @@ public class TestExecutionVariableExtractor extends AbstractSymbolicExecutionTes
/**
* Tests example: /set/variablesSimpleCycle
*/
public void testVariablesSimpleCycle() throws Exception {
@Test public void testVariablesSimpleCycle() throws Exception {
doSETTest(testCaseDirectory,
"/set/variablesSimpleCycle/test/VariablesSimpleCycle.java",
"VariablesSimpleCycle",
......@@ -257,7 +259,7 @@ public class TestExecutionVariableExtractor extends AbstractSymbolicExecutionTes
/**
* Tests example: /set/variablesWithQuantifier
*/
public void testVariablesWithQuantifier() throws Exception {
@Test public void testVariablesWithQuantifier() throws Exception {
doSETTest(testCaseDirectory,
"/set/variablesWithQuantifier/test/EnoughInfoReturn.java",
"EnoughInfoReturn",
......@@ -284,7 +286,7 @@ public class TestExecutionVariableExtractor extends AbstractSymbolicExecutionTes
/**
* Tests example: /set/variablesVariableArrayIndex
*/
public void testVariableArrayIndex() throws Exception {
@Test public void testVariableArrayIndex() throws Exception {
doSETTest(testCaseDirectory,
"/set/variablesVariableArrayIndex/test/VariableArrayIndex.java",
"VariableArrayIndex",
......@@ -311,7 +313,7 @@ public class TestExecutionVariableExtractor extends AbstractSymbolicExecutionTes
/**
* Tests example: /set/variablesConditionalValuesTest
*/
public void testVariablesConditionalValuesTest_next() throws Exception {
@Test public void testVariablesConditionalValuesTest_next() throws Exception {
doSETTest(testCaseDirectory,
"/set/variablesConditionalValuesTest/test/ConditionalValuesTest.java",
"ConditionalValuesTest",
......@@ -338,7 +340,7 @@ public class TestExecutionVariableExtractor extends AbstractSymbolicExecutionTes
/**
* Tests example: /set/variablesConditionalValuesTest
*/
public void testVariablesConditionalValuesTest() throws Exception {
@Test public void testVariablesConditionalValuesTest() throws Exception {
doSETTest(testCaseDirectory,
"/set/variablesConditionalValuesTest/test/ConditionalValuesTest.java",
"ConditionalValuesTest",
......@@ -365,7 +367,7 @@ public class TestExecutionVariableExtractor extends AbstractSymbolicExecutionTes
/**
* Tests example: /set/variableVariablesArrayTest
*/
public void testVariableVariablesArrayTest() throws Exception {
@Test public void testVariableVariablesArrayTest() throws Exception {
doSETTest(testCaseDirectory,
"/set/variableVariablesArrayTest/test/VariablesArrayTest.java",
"VariablesArrayTest",
......@@ -392,7 +394,7 @@ public class TestExecutionVariableExtractor extends AbstractSymbolicExecutionTes
/**
* Tests example: /set/variablesLocalVariablesTest
*/
public void testVariablesLocalVariablesTest() throws Exception {
@Test public void testVariablesLocalVariablesTest() throws Exception {
doSETTest(testCaseDirectory,
"/set/variablesLocalVariablesTest/test/LocalVariablesTest.java",
"LocalVariablesTest",
......@@ -419,7 +421,7 @@ public class TestExecutionVariableExtractor extends AbstractSymbolicExecutionTes
/**
* Tests example: /set/variablesUpdateVariablesTest
*/
public void testUpdateVariablesTest() throws Exception {
@Test public void testUpdateVariablesTest() throws Exception {
doSETTest(testCaseDirectory,
"/set/variablesUpdateVariablesTest/test/UpdateVariablesTest.java",
"UpdateVariablesTest",
......
......@@ -19,6 +19,7 @@ import java.util.List;
import javax.xml.parsers.ParserConfigurationException;
import org.junit.Test;
import org.xml.sax.SAXException;
import de.uka.ilkd.key.control.DefaultUserInterfaceControl;
......@@ -30,6 +31,8 @@ import de.uka.ilkd.key.symbolic_execution.model.IExecutionNode;
import de.uka.ilkd.key.symbolic_execution.model.IExecutionVariable;
import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionEnvironment;
import static org.junit.Assert.*;
/**
* This test class makes sure that parallel site proofs are working. It is only
* verified that no exception is thrown and not that correct results are computed.
......@@ -65,7 +68,7 @@ public class TestParallelSiteProofs extends AbstractSymbolicExecutionTestCase {
/**
* Tests parallel site proofs on a proof reconstructed from a *.proof file.
*/
public void testProofFile() throws ProofInputException, IOException, ProblemLoaderException {
@Test public void testProofFile() throws ProofInputException, IOException, ProblemLoaderException {
// Define test settings
String javaPathInkeyRepDirectory = "/set/magic42/test/Magic42.proof";
// Create proof environment for symbolic execution
......
......@@ -37,6 +37,8 @@ import de.uka.ilkd.key.symbolic_execution.SymbolicLayoutReader.KeYlessObject;
import de.uka.ilkd.key.symbolic_execution.SymbolicLayoutReader.KeYlessState;
import de.uka.ilkd.key.symbolic_execution.SymbolicLayoutReader.KeYlessValue;
import de.uka.ilkd.key.symbolic_execution.object_model.ISymbolicLayout;
import static org.junit.Assert.*;
import org.junit.Test;
/**
* Tests {@link SymbolicLayoutWriter} and {@link SymbolicLayoutReader}
......@@ -46,7 +48,7 @@ public class TestSymbolicLayoutWriterAndReader extends TestCase {
/**
* Tests the writing and reading of an {@link ISymbolicLayout}.
*/
public void testWritingAndReading() throws ProofInputException, ParserConfigurationException, SAXException, IOException {
@Test public void testWritingAndReading() throws ProofInputException, ParserConfigurationException, SAXException, IOException {
// Create model
ISymbolicLayout expectedNode = createModel();
// Serialize model to XML string
......
......@@ -2,16 +2,18 @@ package de.uka.ilkd.key.symbolic_execution.testcase;
import junit.framework.TestCase;
import de.uka.ilkd.key.symbolic_execution.TruthValueTracingUtil.TruthValue;
import static org.junit.Assert.*;
import org.junit.Test;
/**
* Tests for {@link TruthValue}.
* @author Martin Hentschel
*/
public class TestTruthValueValue extends TestCase {
public class TestTruthValueValue {
/**
* Tests {@link TruthValue#ifThenElse(TruthValue, TruthValue, TruthValue)}.
*/
public void testIfThenElse() {
@Test public void testIfThenElse() {
// true
assertEquals(TruthValue.TRUE, TruthValue.ifThenElse(TruthValue.TRUE, TruthValue.TRUE, TruthValue.TRUE));
assertEquals(TruthValue.TRUE, TruthValue.ifThenElse(TruthValue.TRUE, TruthValue.TRUE, TruthValue.FALSE));
......@@ -85,7 +87,7 @@ public class TestTruthValueValue extends TestCase {
/**
* Tests {@link TruthValue#eqv(TruthValue, TruthValue)}.
*/
public void testEqv() {
@Test public void testEqv() {
// true
assertEquals(TruthValue.TRUE, TruthValue.eqv(TruthValue.TRUE, TruthValue.TRUE));
assertEquals(TruthValue.FALSE, TruthValue.eqv(TruthValue.TRUE, TruthValue.FALSE));
......@@ -111,7 +113,7 @@ public class TestTruthValueValue extends TestCase {
/**
* Tests {@link TruthValue#and(TruthValue, TruthValue)}.
*/
public void testAnd() {
@Test public void testAnd() {
// true
assertEquals(TruthValue.TRUE, TruthValue.and(TruthValue.TRUE, TruthValue.TRUE));
assertEquals(TruthValue.FALSE, TruthValue.and(TruthValue.TRUE, TruthValue.FALSE));
......@@ -137,7 +139,7 @@ public class TestTruthValueValue extends TestCase {
/**
* Tests {@link TruthValue#or(TruthValue, TruthValue)}.
*/
public void testOr() {
@Test public void testOr() {
// true
assertEquals(TruthValue.TRUE, TruthValue.or(TruthValue.TRUE, TruthValue.TRUE));
assertEquals(TruthValue.TRUE, TruthValue.or(TruthValue.TRUE, TruthValue.FALSE));
......@@ -163,7 +165,7 @@ public class TestTruthValueValue extends TestCase {
/**
* Tests {@link TruthValue#imp(TruthValue, TruthValue)}.
*/
public void testImp() {
@Test public void testImp() {
// true
assertEquals(TruthValue.TRUE, TruthValue.imp(TruthValue.TRUE, TruthValue.TRUE));
assertEquals(TruthValue.FALSE, TruthValue.imp(TruthValue.TRUE, TruthValue.FALSE));
......@@ -189,7 +191,7 @@ public class TestTruthValueValue extends TestCase {
/**
* Tests {@link TruthValue#not(TruthValue)}.
*/
public void testNot() {
@Test public void testNot() {
assertEquals(TruthValue.FALSE, TruthValue.not(TruthValue.TRUE));
assertEquals(TruthValue.TRUE, TruthValue.not(TruthValue.FALSE));
assertEquals(TruthValue.UNKNOWN, TruthValue.not(TruthValue.UNKNOWN));
......
......@@ -27,6 +27,8 @@ import de.uka.ilkd.key.proof.init.ProofInputException;
import de.uka.ilkd.key.proof.io.ProblemLoaderException;
import de.uka.ilkd.key.symbolic_execution.testcase.AbstractSymbolicExecutionTestCase;
import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionEnvironment;
import static org.junit.Assert.*;
import org.junit.Test;
/**
* Tests the {@link FunctionalOperationContractPO} used for symbolic execution.
......@@ -36,7 +38,7 @@ public class TestFunctionalOperationContractPO extends AbstractSymbolicExecution
/**
* Tests the contract of method {@code doubleValue}.
*/
public void testDoubleValue() throws IOException, ProofInputException, ParserConfigurationException, SAXException, ProblemLoaderException {
@Test public void testDoubleValue() throws IOException, ProofInputException, ParserConfigurationException, SAXException, ProblemLoaderException {
doTest("/set/existingContractTest/test/ExistingContractTest.java",
"ExistingContractTest[ExistingContractTest::doubleValue(int)].JML operation contract.0",
"/set/existingContractTest/oracle/ExistingContractTest.xml",
......
......@@ -27,6 +27,8 @@ import de.uka.ilkd.key.proof.io.ProblemLoaderException;
import de.uka.ilkd.key.symbolic_execution.po.ProgramMethodPO;
import de.uka.ilkd.key.symbolic_execution.testcase.AbstractSymbolicExecutionTestCase;
import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionEnvironment;
import static org.junit.Assert.*;
import org.junit.Test;
/**
* Tests for {@link ProgramMethodPO}.
......@@ -36,7 +38,7 @@ public class TestProgramMethodPO extends AbstractSymbolicExecutionTestCase {
/**
* Tests {@code complicatedMethod} without precondition.
*/
public void testComplicatedInnerMethod() throws IOException, ProofInputException, ParserConfigurationException, SAXException, ProblemLoaderException {
@Test public void testComplicatedInnerMethod() throws IOException, ProofInputException, ParserConfigurationException, SAXException, ProblemLoaderException {
doTest("/set/fullqualifiedTypeNamesTest/test/my/packageName/TheClass.java",
"my.packageName.TheClass.TheInnerClass",
"complicatedInnerMethod",
......@@ -48,7 +50,7 @@ public class TestProgramMethodPO extends AbstractSymbolicExecutionTestCase {
/**
* Tests {@code complicatedMethod} with precondition.
*/
public void testComplicatedMethod_Precondition() throws IOException, ProofInputException, ParserConfigurationException, SAXException, ProblemLoaderException {
@Test public void testComplicatedMethod_Precondition() throws IOException, ProofInputException, ParserConfigurationException, SAXException, ProblemLoaderException {
doTest("/set/fullqualifiedTypeNamesTest/test/my/packageName/TheClass.java",
"my.packageName.TheClass",
"complicatedMethod",
......@@ -60,7 +62,7 @@ public class TestProgramMethodPO extends AbstractSymbolicExecutionTestCase {
/**
* Tests {@code complicatedMethod} without precondition.
*/
public void testComplicatedMethod() throws IOException, ProofInputException, ParserConfigurationException, SAXException, ProblemLoaderException {
@Test public void testComplicatedMethod() throws IOException, ProofInputException, ParserConfigurationException, SAXException, ProblemLoaderException {
doTest("/set/fullqualifiedTypeNamesTest/test/my/packageName/TheClass.java",
"my.packageName.TheClass",
"complicatedMethod",
......@@ -72,7 +74,7 @@ public class TestProgramMethodPO extends AbstractSymbolicExecutionTestCase {
/**
* Tests {@code returnMethod} with precondition.
*/
public void testReturnMethod_Precondition() throws IOException, ProofInputException, ParserConfigurationException, SAXException, ProblemLoaderException {
@Test public void testReturnMethod_Precondition() throws IOException, ProofInputException, ParserConfigurationException, SAXException, ProblemLoaderException {
doTest("/set/methodPOTest/test/MethodPOTest.java",
"MethodPOTest",
"returnMethod",
......@@ -84,7 +86,7 @@ public class TestProgramMethodPO extends AbstractSymbolicExecutionTestCase {
/**
* Tests {@code returnMethod} without precondition.
*/
public void testReturnMethod() throws IOException, ProofInputException, ParserConfigurationException, SAXException, ProblemLoaderException {
@Test public void testReturnMethod() throws IOException, ProofInputException, ParserConfigurationException, SAXException, ProblemLoaderException {
doTest("/set/methodPOTest/test/MethodPOTest.java",
"MethodPOTest",
"returnMethod",
......@@ -96,7 +98,7 @@ public class TestProgramMethodPO extends AbstractSymbolicExecutionTestCase {
/**
* Tests {@code voidMethod} with precondition.
*/
public void testVoidMethod_Precondition() throws IOException, ProofInputException, ParserConfigurationException, SAXException, ProblemLoaderException {
@Test public void testVoidMethod_Precondition() throws IOException, ProofInputException, ParserConfigurationException, SAXException, ProblemLoaderException {
doTest("/set/methodPOTest/test/MethodPOTest.java",
"MethodPOTest",
"voidMethod",
......@@ -108,7 +110,7 @@ public class TestProgramMethodPO extends AbstractSymbolicExecutionTestCase {
/**
* Tests {@code voidMethod} without precondition.
*/
public void testVoidMethod() throws IOException, ProofInputException, ParserConfigurationException, SAXException, ProblemLoaderException {
@Test public void testVoidMethod() throws IOException, ProofInputException, ParserConfigurationException, SAXException, ProblemLoaderException {
doTest("/set/methodPOTest/test/MethodPOTest.java",
"MethodPOTest",
"voidMethod",
......
......@@ -27,6 +27,8 @@ import de.uka.ilkd.key.proof.io.ProblemLoaderException;
import de.uka.ilkd.key.symbolic_execution.po.ProgramMethodSubsetPO;
import de.uka.ilkd.key.symbolic_execution.testcase.AbstractSymbolicExecutionTestCase;
import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionEnvironment;
import static org.junit.Assert.*;
import org.junit.Test;
/**
* Tests for {@link ProgramMethodSubsetPO}.
......@@ -36,7 +38,7 @@ public class TestProgramMethodSubsetPO extends AbstractSymbolicExecutionTestCase
/**
* Tests {@code x-=42;return x;} of {@code doSomething} with precondition.
*/
public void testDoSomethingElseBranch() throws IOException, ProofInputException, ParserConfigurationException, SAXException, ProblemLoaderException {
@Test public void testDoSomethingElseBranch() throws IOException, ProofInputException, ParserConfigurationException, SAXException, ProblemLoaderException {
doTest("/set/methodPartPOTest/test/MethodPartPOTest.java",
"MethodPartPOTest",
"doSomething",
......@@ -50,7 +52,7 @@ public class TestProgramMethodSubsetPO extends AbstractSymbolicExecutionTestCase