Commit 6d75608b authored by Sarah Grebing's avatar Sarah Grebing

New KeY Version and modification of interface acc. to new version; corrected Sysouts;

parent 824f45f9
Pipeline #42008 passed with stages
in 5 minutes and 45 seconds
...@@ -251,7 +251,7 @@ public class ValueInjector { ...@@ -251,7 +251,7 @@ public class ValueInjector {
try { try {
t = tc.convert(userinput); t = tc.convert(userinput);
} catch (ParserException pe) { } catch (ParserException pe) {
System.out.println("edu/kit/iti/formal/psdbg/ValueInjector.java:250 ParserException"); //System.out.println("edu/kit/iti/formal/psdbg/ValueInjector.java:250 ParserException");
throw new ArgumentRequiredException( throw new ArgumentRequiredException(
String.format("Argument %s:%s is required, but %s was given. " + String.format("Argument %s:%s is required, but %s was given. " +
"For comamnd class: '%s'", "For comamnd class: '%s'",
......
...@@ -8,10 +8,10 @@ import de.uka.ilkd.key.logic.op.LogicVariable; ...@@ -8,10 +8,10 @@ import de.uka.ilkd.key.logic.op.LogicVariable;
import de.uka.ilkd.key.logic.op.SchemaVariable; import de.uka.ilkd.key.logic.op.SchemaVariable;
import de.uka.ilkd.key.parser.ParserException; import de.uka.ilkd.key.parser.ParserException;
import de.uka.ilkd.key.pp.LogicPrinter; import de.uka.ilkd.key.pp.LogicPrinter;
import de.uka.ilkd.key.proof.ApplyStrategy;
import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.proof.Goal;
import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.Proof;
import de.uka.ilkd.key.proof.init.Profile; import de.uka.ilkd.key.proof.init.Profile;
import de.uka.ilkd.key.prover.impl.ApplyStrategy;
import de.uka.ilkd.key.rule.NoPosTacletApp; import de.uka.ilkd.key.rule.NoPosTacletApp;
import de.uka.ilkd.key.rule.Taclet; import de.uka.ilkd.key.rule.Taclet;
import de.uka.ilkd.key.rule.TacletApp; import de.uka.ilkd.key.rule.TacletApp;
......
...@@ -115,6 +115,7 @@ public class ExecuteTest { ...@@ -115,6 +115,7 @@ public class ExecuteTest {
Interpreter<KeyData> run = exec.run(); Interpreter<KeyData> run = exec.run();
Assert.assertTrue(run.getCurrentGoals().isEmpty()); Assert.assertTrue(run.getCurrentGoals().isEmpty());
System.out.println("The proof of Quicksorts split method was closed");
} }
} }
\ No newline at end of file
// This file is part of KeY - Integrated Deductive Software Design \settings{
// "#Proof-Settings-Config-File
// Copyright (C) 2001-2011 Universitaet Karlsruhe (TH), Germany [StrategyProperty]OSS_OPTIONS_KEY=OSS_ON
// Universitaet Koblenz-Landau, Germany [StrategyProperty]VBT_PHASE=VBT_SYM_EX
// Chalmers University of Technology, Sweden [SMTSettings]useUninterpretedMultiplication=true
// Copyright (C) 2011-2013 Karlsruhe Institute of Technology, Germany [SMTSettings]SelectedTaclets=
// Technical University Darmstadt, Germany [StrategyProperty]METHOD_OPTIONS_KEY=METHOD_CONTRACT
// Chalmers University of Technology, Sweden [StrategyProperty]USER_TACLETS_OPTIONS_KEY3=USER_TACLETS_OFF
// [StrategyProperty]SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY=SYMBOLIC_EXECUTION_ALIAS_CHECK_NEVER
// The KeY system is protected by the GNU General [StrategyProperty]LOOP_OPTIONS_KEY=LOOP_INVARIANT
// Public License. See LICENSE.TXT for details. [StrategyProperty]USER_TACLETS_OPTIONS_KEY2=USER_TACLETS_OFF
// [StrategyProperty]USER_TACLETS_OPTIONS_KEY1=USER_TACLETS_OFF
[StrategyProperty]QUANTIFIERS_OPTIONS_KEY=QUANTIFIERS_NON_SPLITTING_WITH_PROGS
[StrategyProperty]NON_LIN_ARITH_OPTIONS_KEY=NON_LIN_ARITH_NONE
[SMTSettings]instantiateHierarchyAssumptions=true
[StrategyProperty]AUTO_INDUCTION_OPTIONS_KEY=AUTO_INDUCTION_OFF
[StrategyProperty]DEP_OPTIONS_KEY=DEP_ON
[StrategyProperty]CLASS_AXIOM_OPTIONS_KEY=CLASS_AXIOM_FREE
[StrategyProperty]SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY=SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OFF
[StrategyProperty]QUERY_NEW_OPTIONS_KEY=QUERY_OFF
[Strategy]Timeout=-1
[Strategy]MaximumNumberOfAutomaticApplications=10000
[SMTSettings]integersMaximum=2147483645
[Choice]DefaultChoices=assertions-assertions\:safe , initialisation-initialisation\:disableStaticInitialisation , intRules-intRules\:arithmeticSemanticsIgnoringOF , programRules-programRules\:Java , runtimeExceptions-runtimeExceptions\:allow , JavaCard-JavaCard\:off , Strings-Strings\:on , modelFields-modelFields\:treatAsAxiom , bigint-bigint\:on , sequences-sequences\:on , moreSeqRules-moreSeqRules\:on , reach-reach\:on , integerSimplificationRules-integerSimplificationRules\:full , permissions-permissions\:off , wdOperator-wdOperator\:L , wdChecks-wdChecks\:off , mergeGenerateIsWeakeningGoal-mergeGenerateIsWeakeningGoal\:off
[SMTSettings]useConstantsForBigOrSmallIntegers=true
[StrategyProperty]STOPMODE_OPTIONS_KEY=STOPMODE_DEFAULT
[StrategyProperty]QUERYAXIOM_OPTIONS_KEY=QUERYAXIOM_ON
[StrategyProperty]INF_FLOW_CHECK_PROPERTY=INF_FLOW_CHECK_FALSE
[SMTSettings]maxGenericSorts=2
[SMTSettings]integersMinimum=-2147483645
[SMTSettings]invariantForall=false
[SMTSettings]UseBuiltUniqueness=false
[SMTSettings]explicitTypeHierarchy=false
[Strategy]ActiveStrategy=JavaCardDLStrategy
[StrategyProperty]SPLITTING_OPTIONS_KEY=SPLITTING_DELAYED
[StrategyProperty]MPS_OPTIONS_KEY=MPS_MERGE"}
\javaSource "./"; \javaSource "./";
......
...@@ -148,7 +148,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Object> ...@@ -148,7 +148,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
Variable var = assignmentStatement.getLhs(); Variable var = assignmentStatement.getLhs();
Expression expr = assignmentStatement.getRhs(); Expression expr = assignmentStatement.getRhs();
if (t != null) { if (t != null) {
System.out.println("t = " + t+ var); // System.out.println("t = " + t+ var);
node.declareVariable(var, t); node.declareVariable(var, t);
} }
...@@ -161,7 +161,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Object> ...@@ -161,7 +161,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
if (fireVariableAssignmentHook(node, var.getIdentifier(), v)) { if (fireVariableAssignmentHook(node, var.getIdentifier(), v)) {
node.setVariableValue(var, v); node.setVariableValue(var, v);
} }
System.out.println("v = " + v); //System.out.println("v = " + v);
node.setVariableValue(var, v); node.setVariableValue(var, v);
} }
} }
......
...@@ -6,7 +6,7 @@ import de.uka.ilkd.key.macros.ProofMacro; ...@@ -6,7 +6,7 @@ import de.uka.ilkd.key.macros.ProofMacro;
import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.proof.Goal;
import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.Node;
import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.Proof;
import de.uka.ilkd.key.proof.ProverTaskListener; import de.uka.ilkd.key.prover.ProverTaskListener;
import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.ImmutableList;
public class TestGenMacro implements ProofMacro { public class TestGenMacro implements ProofMacro {
...@@ -30,6 +30,21 @@ public class TestGenMacro implements ProofMacro { ...@@ -30,6 +30,21 @@ public class TestGenMacro implements ProofMacro {
return null; return null;
} }
@Override
public boolean hasParameter(String s) {
return false;
}
@Override
public void setParameter(String s, String s1) throws IllegalArgumentException {
}
@Override
public void resetParams() {
}
@Override @Override
public boolean canApplyTo(Proof proof, ImmutableList<Goal> immutableList, PosInOccurrence posInOccurrence) { public boolean canApplyTo(Proof proof, ImmutableList<Goal> immutableList, PosInOccurrence posInOccurrence) {
return false; return false;
......
...@@ -289,6 +289,7 @@ public class InteractiveModeController { ...@@ -289,6 +289,7 @@ public class InteractiveModeController {
} catch (ScriptCommandNotApplicableException e) { } catch (ScriptCommandNotApplicableException e) {
StringBuilder sb = new StringBuilder("The macro command "); StringBuilder sb = new StringBuilder("The macro command ");
sb.append(call.getCommand()).append(" was not applicable."); sb.append(call.getCommand()).append(" was not applicable.");
LOGGER.error(e);
System.out.println("e = " + e); System.out.println("e = " + e);
//sb.append("\nSequent Formula: formula=").append(sfTerm); //sb.append("\nSequent Formula: formula=").append(sfTerm);
//sb.append("\nOn Sub Term: on=").append(onTerm); //sb.append("\nOn Sub Term: on=").append(onTerm);
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment