Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Sign in
Toggle navigation
Menu
Open sidebar
sarah.grebing
ProofScriptParser
Commits
7df3ceaf
Commit
7df3ceaf
authored
Jun 26, 2018
by
Alexander Weigl
Browse files
delete unused field in debuggerframework
parent
7b854843
Changes
5
Hide whitespace changes
Inline
Side-by-side
rt-key/src/main/java/edu/kit/iti/formal/psdbg/InteractiveCLIDebugger.java
View file @
7df3ceaf
...
...
@@ -60,7 +60,7 @@ public class InteractiveCLIDebugger {
//ControlFlowVisitor cfgVistor = new ControlFlowVisitor(ib.getLookup());
//MutableValueGraph<ControlFlowNode, ControlFlowTypes> cfg = cfgVistor.getGraph();
df
=
new
DebuggerFramework
<>(
interpreter
,
scripts
.
get
(
0
)
,
null
);
df
=
new
DebuggerFramework
<>(
interpreter
,
scripts
.
get
(
0
));
df
.
getStatePointerListener
().
add
(
this
::
printNode
);
//df.getBeforeExecutionListener().add(this::printNode);
//df.getAfterExecutionListener().add(this::end);
...
...
rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/dbg/DebuggerFramework.java
View file @
7df3ceaf
package
edu.kit.iti.formal.psdbg.interpreter.dbg
;
import
com.google.common.graph.MutableValueGraph
;
import
edu.kit.iti.formal.psdbg.interpreter.Interpreter
;
import
edu.kit.iti.formal.psdbg.interpreter.graphs.ControlFlowNode
;
import
edu.kit.iti.formal.psdbg.interpreter.graphs.ControlFlowTypes
;
import
edu.kit.iti.formal.psdbg.parser.ast.CallStatement
;
import
edu.kit.iti.formal.psdbg.parser.ast.ProofScript
;
import
lombok.Getter
;
...
...
@@ -103,15 +100,14 @@ public class DebuggerFramework<T> {
public
DebuggerFramework
(
@Nonnull
Interpreter
<
T
>
interpreter
,
@Nonnull
ProofScript
main
,
MutableValueGraph
<
ControlFlowNode
,
ControlFlowTypes
>
cfg
)
{
@Nonnull
ProofScript
main
)
{
this
.
interpreter
=
interpreter
;
mainScript
=
main
;
blocker
=
new
BlockListener
<>(
interpreter
);
breakpointBlocker
=
new
Blocker
.
BreakpointLine
<>(
interpreter
);
blocker
.
getPredicates
().
add
(
breakpointBlocker
);
stateWrapper
=
new
StateWrapper
<>(
interpreter
);
ptreeManager
=
new
ProofTreeManager
<>(
cfg
);
ptreeManager
=
new
ProofTreeManager
<>();
stateWrapper
.
setEmitNode
(
ptreeManager:
:
receiveNode
);
interpreterThread
=
new
Thread
(
this
::
run
);
}
...
...
rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/dbg/ProofTreeManager.java
View file @
7df3ceaf
...
...
@@ -34,11 +34,6 @@ public class ProofTreeManager<T> {
ValueGraphBuilder.directed().allowsSelfLoops(false).build();
*/
@Getter
@Setter
@Nullable
private
final
MutableValueGraph
<
ControlFlowNode
,
ControlFlowTypes
>
controlFlowGraph
;
@Getter
private
final
Set
<
PTreeNode
<
T
>>
nodes
=
new
HashSet
<>();
...
...
@@ -59,8 +54,7 @@ public class ProofTreeManager<T> {
private
List
<
List
<
PTreeNode
<
T
>>>
context
=
new
ArrayList
<>(
10
);
public
ProofTreeManager
(
MutableValueGraph
<
ControlFlowNode
,
ControlFlowTypes
>
controlFlowGraph
)
{
this
.
controlFlowGraph
=
controlFlowGraph
;
public
ProofTreeManager
()
{
pushContext
();
}
...
...
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java
View file @
7df3ceaf
...
...
@@ -2,7 +2,6 @@ package edu.kit.iti.formal.psdbg.gui.controller;
import
alice.tuprolog.InvalidLibraryException
;
import
alice.tuprolog.InvalidTheoryException
;
import
antlr.collections.AST
;
import
com.google.common.eventbus.Subscribe
;
import
de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIcon
;
import
de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIconView
;
...
...
@@ -36,9 +35,7 @@ import edu.kit.iti.formal.psdbg.interpreter.data.SavePoint;
import
edu.kit.iti.formal.psdbg.interpreter.data.State
;
import
edu.kit.iti.formal.psdbg.interpreter.dbg.*
;
import
edu.kit.iti.formal.psdbg.parser.ASTDiff
;
import
edu.kit.iti.formal.psdbg.parser.Facade
;
import
edu.kit.iti.formal.psdbg.parser.ast.ASTNode
;
import
edu.kit.iti.formal.psdbg.parser.ast.CaseStatement
;
import
edu.kit.iti.formal.psdbg.parser.ast.ProofScript
;
import
edu.kit.iti.formal.psdbg.storage.KeyPersistentFacade
;
import
javafx.application.Platform
;
...
...
@@ -61,7 +58,6 @@ import javafx.stage.FileChooser;
import
javafx.stage.Modality
;
import
lombok.Getter
;
import
lombok.RequiredArgsConstructor
;
import
lombok.val
;
import
org.apache.commons.io.FileUtils
;
import
org.apache.logging.log4j.LogManager
;
import
org.apache.logging.log4j.Logger
;
...
...
@@ -75,11 +71,6 @@ import org.reactfx.util.Timer;
import
javax.annotation.Nullable
;
import
javax.swing.*
;
import
javax.xml.bind.JAXBException
;
import
java.awt.event.WindowAdapter
;
import
java.awt.event.WindowEvent
;
import
java.awt.event.WindowListener
;
import
java.awt.event.WindowStateListener
;
import
java.awt.im.InputContext
;
import
java.io.*
;
import
java.net.URL
;
import
java.nio.charset.Charset
;
...
...
@@ -89,8 +80,6 @@ import java.util.*;
import
java.util.concurrent.*
;
import
java.util.stream.Collectors
;
import
org.reactfx.util.Timer
;
/**
* Controller for the Debugger MainWindow
...
...
@@ -742,7 +731,7 @@ public class DebuggerMain implements Initializable {
public
void
createDebuggerFramework
(
Collection
<?
extends
Breakpoint
>
breakpoints
,
ProofScript
ms
,
boolean
addInitBreakpoint
,
KeyInterpreter
interpreter
)
{
DebuggerFramework
<
KeyData
>
df
=
new
DebuggerFramework
<>(
interpreter
,
ms
,
null
);
DebuggerFramework
<
KeyData
>
df
=
new
DebuggerFramework
<>(
interpreter
,
ms
);
df
.
setSucceedListener
(
this
::
onInterpreterSucceed
);
df
.
setErrorListener
(
this
::
onInterpreterError
);
if
(
addInitBreakpoint
)
{
...
...
ui/src/test/java/edu/kit/iti/formal/psdbg/gui/controls/ProofTreeTest.java
View file @
7df3ceaf
...
...
@@ -4,7 +4,6 @@ import de.uka.ilkd.key.proof.io.ProblemLoaderException;
import
edu.kit.iti.formal.psdbg.interpreter.Interpreter
;
import
edu.kit.iti.formal.psdbg.interpreter.InterpreterBuilder
;
import
edu.kit.iti.formal.psdbg.interpreter.KeYProofFacade
;
import
edu.kit.iti.formal.psdbg.interpreter.data.KeyData
;
import
edu.kit.iti.formal.psdbg.interpreter.dbg.DebuggerFramework
;
import
edu.kit.iti.formal.psdbg.interpreter.dbg.PTreeNode
;
...
...
@@ -12,28 +11,21 @@ import edu.kit.iti.formal.psdbg.parser.Facade;
import
edu.kit.iti.formal.psdbg.parser.ast.ProofScript
;
import
javafx.scene.control.TreeItem
;
import
org.antlr.v4.runtime.CharStreams
;
import
org.junit.Before
;
import
org.junit.Test
;
import
java.io.File
;
import
java.io.FileInputStream
;
import
java.io.IOException
;
import
java.util.List
;
public
class
ProofTreeTest
{
KeYProofFacade
facade
;
List
<
ProofScript
>
scripts
;
Interpreter
<
KeyData
>
i
;
private
KeYProofFacade
facade
;
private
List
<
ProofScript
>
scripts
;
private
Interpreter
<
KeyData
>
interpreter
;
@Before
public
void
setUp
()
throws
Exception
{
facade
=
new
KeYProofFacade
();
facade
=
new
KeYProofFacade
();
}
@Test
...
...
@@ -42,9 +34,9 @@ public class ProofTreeTest {
facade
.
loadKeyFileSync
(
keyProblem
);
scripts
=
Facade
.
getAST
(
CharStreams
.
fromStream
(
getClass
().
getResourceAsStream
(
"proofTreeScript.kps"
)));
InterpreterBuilder
ib
=
facade
.
buildInterpreter
();
i
=
ib
.
build
();
DebuggerFramework
<
KeyData
>
df
=
new
DebuggerFramework
<>(
i
,
scripts
.
get
(
0
)
,
null
);
i
.
interpret
(
scripts
.
get
(
0
));
i
nterpreter
=
ib
.
build
();
DebuggerFramework
<
KeyData
>
df
=
new
DebuggerFramework
<>(
i
nterpreter
,
scripts
.
get
(
0
));
i
nterpreter
.
interpret
(
scripts
.
get
(
0
));
ScriptTreeTransformation
treeScriptCreation
=
new
ScriptTreeTransformation
(
df
.
getPtreeManager
(),
facade
.
getProof
(),
facade
.
getProof
().
root
());
treeScriptCreation
.
create
(
facade
.
getProof
());
PTreeNode
startNode
=
df
.
getPtreeManager
().
getStartNode
();
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment