Commit 0054d220 authored by Sarah Grebing's avatar Sarah Grebing
Browse files

minor cleaning code and possible bugfix

parent 38d2c3e6
......@@ -110,7 +110,9 @@ public class ProofTree extends BorderPane {
Utils.createWithFXML(this);
//TODO remove this hack for a better solution
main.getModel().debuggerFrameworkProperty().addListener((p, n, m) -> {
treeScriptCreation = new ScriptTreeTransformation(m.getPtreeManager());
if(m != null) {
treeScriptCreation = new ScriptTreeTransformation(m.getPtreeManager());
}
});
treeCreation = new KeyProofTreeTransformation(sentinels);
......
......@@ -254,6 +254,8 @@ public class ScriptTreeGraph {
@Override
public Void visit(CallStatement call) {
if(call.getCommand().equals("")) return null;
if (nextPtreeNode.toString().equals("End of Script")) return null;
Node n = nextPtreeNode.getStateBeforeStmt().getSelectedGoalNode().getData().getNode();
ScriptTreeNode sn = new ScriptTreeNode(n, nextPtreeNode, nextPtreeNode.getStatement().getStartPosition().getLineNumber());
......@@ -348,16 +350,30 @@ public class ScriptTreeGraph {
@Override
public Void visit(ForeachStatement foreachStatement) {
List<GoalNode<KeyData>> goals = nextPtreeNode.getStateBeforeStmt().getGoals();
if (goals.size() == 0) return null;
goals.forEach(k -> putIntoMapping(k.getData().getNode(), new ForeachTreeNode(k.getData().getNode(), nextPtreeNode, nextPtreeNode.getStatement().getStartPosition().getLineNumber(),true)));
// add to foreachNodes lsit
List<GoalNode<KeyData>> aftergoals = (nextPtreeNode.getStateAfterStmt() != null)? nextPtreeNode.getStateAfterStmt().getGoals()
: (nextPtreeNode.getStepOver() != null && nextPtreeNode.getStepOver().getStateBeforeStmt() != null) ? nextPtreeNode.getStepOver().getStateBeforeStmt().getGoals()
: new ArrayList<>();
aftergoals.forEach(k -> foreachNodes.put(k.getData().getNode(), nextPtreeNode));
//
// add to foreachNodes list
List<GoalNode<KeyData>> goalsAfterForeach = new ArrayList<>();
assert nextPtreeNode.getStateAfterStmt() != null;
goalsAfterForeach.addAll(nextPtreeNode.getStateAfterStmt().getGoals());
/* List<GoalNode<KeyData>> aftergoals =
(nextPtreeNode.getStateAfterStmt() != null)
? nextPtreeNode.getStateAfterStmt().getGoals()
:
(nextPtreeNode.getStepOver() != null && nextPtreeNode.getStepOver().getStateBeforeStmt() != null) ? nextPtreeNode.getStepOver().getStateBeforeStmt().getGoals()
: new ArrayList<>();*/
//aftergoals.forEach(k -> foreachNodes.put(k.getData().getNode(), nextPtreeNode));
if(goalsAfterForeach.size() == 0){
return null;
}
for (GoalNode<KeyData> goalNode : goalsAfterForeach) {
foreachNodes.put(goalNode.getData().getNode(), nextPtreeNode);
}
return null;
}
......
script testfull(){
impRight;
impRight;
impLeft;
foreach{
notLeft;
}
auto;
}
script full(){
impRight;
impRight;
......
script s() {
symbex;
}
script s1() {
symbex;
foreach{
auto;
}
}
\ No newline at end of file
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