Commit 87f25c1a authored by Sarah Grebing's avatar Sarah Grebing

NPE und Fehlerbehandlung

parent c60feb1b
...@@ -4,7 +4,6 @@ import de.uka.ilkd.key.control.AbstractUserInterfaceControl; ...@@ -4,7 +4,6 @@ import de.uka.ilkd.key.control.AbstractUserInterfaceControl;
import de.uka.ilkd.key.control.DefaultUserInterfaceControl; import de.uka.ilkd.key.control.DefaultUserInterfaceControl;
import de.uka.ilkd.key.macros.scripts.EngineState; import de.uka.ilkd.key.macros.scripts.EngineState;
import de.uka.ilkd.key.macros.scripts.ProofScriptCommand; import de.uka.ilkd.key.macros.scripts.ProofScriptCommand;
import de.uka.ilkd.key.macros.scripts.meta.ProofScriptArgument;
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 edu.kit.iti.formal.psdbg.interpreter.Interpreter; import edu.kit.iti.formal.psdbg.interpreter.Interpreter;
...@@ -15,10 +14,14 @@ import edu.kit.iti.formal.psdbg.interpreter.data.VariableAssignment; ...@@ -15,10 +14,14 @@ import edu.kit.iti.formal.psdbg.interpreter.data.VariableAssignment;
import edu.kit.iti.formal.psdbg.parser.ast.CallStatement; import edu.kit.iti.formal.psdbg.parser.ast.CallStatement;
import lombok.Getter; import lombok.Getter;
import lombok.RequiredArgsConstructor; import lombok.RequiredArgsConstructor;
import org.apache.commons.io.IOUtils;
import org.apache.logging.log4j.LogManager; import org.apache.logging.log4j.LogManager;
import org.apache.logging.log4j.Logger; import org.apache.logging.log4j.Logger;
import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.ImmutableList;
import java.io.IOException;
import java.net.URISyntaxException;
import java.net.URL;
import java.util.Collection; import java.util.Collection;
import java.util.HashMap; import java.util.HashMap;
import java.util.Iterator; import java.util.Iterator;
...@@ -104,17 +107,17 @@ public class ProofScriptCommandBuilder implements CommandHandler<KeyData> { ...@@ -104,17 +107,17 @@ public class ProofScriptCommandBuilder implements CommandHandler<KeyData> {
@Override @Override
public String getHelp(CallStatement call) { public String getHelp(CallStatement call) {
ProofScriptCommand c = commands.get(call.getCommand()); ProofScriptCommand c = commands.get(call.getCommand());
/* URL res = getClass().getResource("/edu/kit/iti/formal/psdbg/commands/" + call.getCommand() + ".html"); URL res = getClass().getResource("/edu/kit/iti/formal/psdbg/commands/" + call.getCommand() + ".html");
try { try {
return IOUtils.toString(res.toURI(), "utf-8"); return IOUtils.toString(res.toURI(), "utf-8");
} catch (NullPointerException | IOException | URISyntaxException e) { } catch (NullPointerException | IOException | URISyntaxException e) {
return "No Help found for " + call.getCommand(); return "No Help found for " + call.getCommand();
}*/ }
StringBuilder html = new StringBuilder(); /* StringBuilder html = new StringBuilder();
html.append("<html><head><style>body {font-family: monospace;}</style></head><body>"); html.append("<html><head><style>body {font-family: monospace;}</style></head><body>");
...@@ -164,6 +167,6 @@ public class ProofScriptCommandBuilder implements CommandHandler<KeyData> { ...@@ -164,6 +167,6 @@ public class ProofScriptCommandBuilder implements CommandHandler<KeyData> {
html.append("</body></html>"); html.append("</body></html>");
return html.toString(); return html.toString();
*/
} }
} }
...@@ -41,6 +41,7 @@ import java.util.Set; ...@@ -41,6 +41,7 @@ import java.util.Set;
*/ */
@RequiredArgsConstructor @RequiredArgsConstructor
public class RuleCommandHandler implements CommandHandler<KeyData> { public class RuleCommandHandler implements CommandHandler<KeyData> {
private static final Logger LOGGER = LogManager.getLogger(RuleCommandHandler.class); private static final Logger LOGGER = LogManager.getLogger(RuleCommandHandler.class);
@Getter @Getter
...@@ -122,14 +123,17 @@ public class RuleCommandHandler implements CommandHandler<KeyData> { ...@@ -122,14 +123,17 @@ public class RuleCommandHandler implements CommandHandler<KeyData> {
KeyData kdn = new KeyData(kd, g.node()); KeyData kdn = new KeyData(kd, g.node());
state.getGoals().add(new GoalNode<>(expandedNode, kdn, kdn.getNode().isClosed())); state.getGoals().add(new GoalNode<>(expandedNode, kdn, kdn.getNode().isClosed()));
} }
} catch (Exception e) { } catch (ScriptException e) {
if (e.getClass().equals(ScriptException.class)) { if (interpreter.isStrictMode()) {
System.out.println("e.getMessage() = " + e.getMessage());
throw new ScriptCommandNotApplicableException(e, c, map); throw new ScriptCommandNotApplicableException(e, c, map);
} else { } else {
throw new RuntimeException(e); //Utils necessary oder schmeißen
LOGGER.error("Command " + call.getCommand() + " is not applicable in line " + call.getRuleContext().getStart().getLine());
} }
} catch (InterruptedException e) {
e.printStackTrace();
} catch (Exception e) {
e.printStackTrace();
} }
} }
......
<!DOCTYPE html>
<html lang="en">
<head>
<meta charset="UTF-8">
<title>rule</title>
</head>
<body>
<h2 id="rule">Rule Application</h2>
<blockquote>
<p>Synopsis: <code>rule tacletname on=&lt;TERM&gt; formula=&lt;TERM&gt; occ=&lt;INT&gt; </code></p>
</blockquote>
Rule keyword can be ommited
<p><strong>Arguments:</strong></p>
<ul>
<li>rulename : <em>STRING</em> name of taclet to apply</li>
<li><code>on</code> : <em>TERM</em> (find term of the taclet)</li>
<li><code>formula</code>: <em>TERM</em> (top-level formula in which term appears)</li>
<li><code>occ</code> : <em>INT</em> (occurrence number of term formula in sequent)</li>
</ul>
</body>
</html>
...@@ -282,17 +282,15 @@ public class DebuggerMain implements Initializable { ...@@ -282,17 +282,15 @@ public class DebuggerMain implements Initializable {
* @see {@link #handleStatePointer(PTreeNode)} * @see {@link #handleStatePointer(PTreeNode)}
*/ */
private void handleStatePointerUI(PTreeNode<KeyData> node) { private void handleStatePointerUI(PTreeNode<KeyData> node) {
if (node != null) { if (node != null) {
graph.addPartiallyAndMark(node);
getInspectionViewsController().getActiveInspectionViewTab().activate(node, node.getStateBeforeStmt()); getInspectionViewsController().getActiveInspectionViewTab().activate(node, node.getStateBeforeStmt());
scriptController.getDebugPositionHighlighter().highlight(node.getStatement()); scriptController.getDebugPositionHighlighter().highlight(node.getStatement());
} else { } else {
getInspectionViewsController().getActiveInspectionViewTab().getFrames().getItems().clear(); getInspectionViewsController().getActiveInspectionViewTab().getFrames().getItems().clear();
scriptController.getDebugPositionHighlighter().remove(); scriptController.getDebugPositionHighlighter().remove();
} }
graph.addPartiallyAndMark(node);
} }
private void marriageJavaCode() { private void marriageJavaCode() {
...@@ -514,6 +512,7 @@ public class DebuggerMain implements Initializable { ...@@ -514,6 +512,7 @@ public class DebuggerMain implements Initializable {
State<KeyData> lastState = statePointer.getStateAfterStmt(); State<KeyData> lastState = statePointer.getStateAfterStmt();
getInspectionViewsController().getActiveInspectionViewTab().activate(statePointer, lastState); getInspectionViewsController().getActiveInspectionViewTab().activate(statePointer, lastState);
}); });
} }
...@@ -1008,7 +1007,7 @@ public class DebuggerMain implements Initializable { ...@@ -1008,7 +1007,7 @@ public class DebuggerMain implements Initializable {
} }
} }
} else { } else {
throw new RuntimeException("Something went wrong when reading stop button"); throw new RuntimeException("Something went wrong when reloading");
} }
} }
...@@ -1224,6 +1223,7 @@ public class DebuggerMain implements Initializable { ...@@ -1224,6 +1223,7 @@ public class DebuggerMain implements Initializable {
); );
node.dock(dockStation, DockPos.CENTER, scriptController.getOpenScripts().get(getScriptController().getMainScript().getScriptArea())); node.dock(dockStation, DockPos.CENTER, scriptController.getOpenScripts().get(getScriptController().getMainScript().getScriptArea()));
node.requestFocus();
} }
} }
......
...@@ -312,7 +312,7 @@ public class ScriptController { ...@@ -312,7 +312,7 @@ public class ScriptController {
getDockNode(area).focus(); getDockNode(area).focus();
area.requestFocus(); area.requestFocus();
//area.scrollBy(new Point2D(0, scrollY)); //area.scrollBy(new Point2D(0, scrollY));
area.selectRange(0, r.start, 0, r.stop); area.selectRange(0, r.start, 0, r.start);
lastScriptArea = area; lastScriptArea = area;
lastRegion = r; lastRegion = r;
......
...@@ -72,29 +72,33 @@ public class Graph<T> { ...@@ -72,29 +72,33 @@ public class Graph<T> {
} }
public void addPartiallyAndMark(PTreeNode<KeyData> node) { public void addPartiallyAndMark(PTreeNode<KeyData> node) {
Cell cell = addCell(node);
if (node.getStepOver() != null) {
addEdge(node, node.getStepOver(), "over");
}
if (node.getStepInto() != null) {
addEdge(node, node.getStepInto(), "into");
}
if (node.getStepInvOver() != null) {
addEdge(node, node.getStepInvOver(), "revo");
}
if (node.getStepInvInto() != null) {
addEdge(node, node.getStepInvInto(), "otni");
}
if (node.getStepReturn() != null) {
addEdge(node, node.getStepReturn(), "rtrn");
}
if (lastHighlightedCell != null) { if (lastHighlightedCell != null) {
lastHighlightedCell.getStyleClass().remove("current-node"); lastHighlightedCell.getStyleClass().remove("current-node");
} }
cell.getStyleClass().add("current-node");
lastHighlightedCell = cell; if (node != null) {
Cell cell = addCell(node);
if (node.getStepOver() != null) {
addEdge(node, node.getStepOver(), "over");
}
if (node.getStepInto() != null) {
addEdge(node, node.getStepInto(), "into");
}
if (node.getStepInvOver() != null) {
addEdge(node, node.getStepInvOver(), "revo");
}
if (node.getStepInvInto() != null) {
addEdge(node, node.getStepInvInto(), "otni");
}
if (node.getStepReturn() != null) {
addEdge(node, node.getStepReturn(), "rtrn");
}
cell.getStyleClass().add("current-node");
lastHighlightedCell = cell;
}
} }
} }
} }
// This file is not written yet!! // This file is not written yet!!
script main() { script main() {
feqff : TERM := `f(c) = f(f(c))`;
ffeqf : TERM := `f(f(c)) = f(c)`;
feqfff: TERM := `f(c) = f(f(f(c)))`;
impRight;
instantiate var=`x` with=`c`;
applyEq on=`f(f(c))` formula=feqfff;
eqSymm on=feqff;
close;
}
script main1() {
impRight; impRight;
//instantiate var=`x` with=`c`; //instantiate var=`x` with=`c`;
//allLeft formula=`\forall` with=`a`; //allLeft formula=`\forall` with=`a`;
allLeft on=`\forall s x; f(f(x)) = f(x)` inst_t=`c`; //allLeft on=`\forall s x; f(f(x)) = f(x)` inst_t=`c`;
} }
......
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