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
f0a7e8cf
Commit
f0a7e8cf
authored
Jul 06, 2017
by
Sarah Grebing
Browse files
bug fix
parent
d8cc45e9
Pipeline
#11937
passed with stage
in 2 minutes and 23 seconds
Changes
9
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
lib/components/key.core.jar
View file @
f0a7e8cf
No preview for this file type
lib/components/key.ui.jar
View file @
f0a7e8cf
No preview for this file type
lib/components/key.util.jar
View file @
f0a7e8cf
No preview for this file type
src/main/java/edu/kit/formal/gui/controller/DebuggerMainWindowController.java
View file @
f0a7e8cf
...
...
@@ -231,8 +231,9 @@ public class DebuggerMainWindowController implements Initializable {
}
});
pc
.
executeScript
(
this
.
debugMode
.
get
());
model
.
currentSelectedGoalNodeProperty
().
bind
(
pc
.
currentSelectedGoalProperty
());
model
.
currentGoalNodesProperty
().
bind
(
pc
.
currentGoalsProperty
());
pc
.
currentGoalsProperty
().
addListener
((
observable
,
oldValue
,
newValue
)
->
{
model
.
setCurrentGoalNodes
(
newValue
);
});
pc
.
startHighlightPositionPropertyProperty
().
addListener
((
observable
,
oldValue
,
newValue
)
->
{
if
(
newValue
.
getLineNumber
()
>
-
1
)
{
...
...
src/main/java/edu/kit/formal/interpreter/InterpreterBuilder.java
View file @
f0a7e8cf
...
...
@@ -96,7 +96,7 @@ public class InterpreterBuilder {
}
public
InterpreterBuilder
macros
(
Collection
<
ProofMacro
>
macros
)
{
macros
.
forEach
(
m
->
pmh
.
getMacros
().
put
(
m
.
getName
(),
m
));
macros
.
forEach
(
m
->
pmh
.
getMacros
().
put
(
m
.
get
ScriptCommand
Name
(),
m
));
return
this
;
}
...
...
src/main/java/edu/kit/formal/interpreter/funchdl/MacroCommandHandler.java
View file @
f0a7e8cf
...
...
@@ -2,11 +2,9 @@ package edu.kit.formal.interpreter.funchdl;
import
de.uka.ilkd.key.macros.ProofMacro
;
import
edu.kit.formal.interpreter.Interpreter
;
import
edu.kit.formal.interpreter.data.Value
;
import
edu.kit.formal.interpreter.data.VariableAssignment
;
import
edu.kit.formal.proofscriptparser.ast.CallStatement
;
import
edu.kit.formal.proofscriptparser.ast.Parameters
;
import
edu.kit.formal.proofscriptparser.ast.StringLiteral
;
import
edu.kit.formal.proofscriptparser.ast.Variable
;
import
edu.kit.formal.proofscriptparser.ast.*
;
import
lombok.Getter
;
import
lombok.RequiredArgsConstructor
;
...
...
@@ -36,15 +34,16 @@ public class MacroCommandHandler implements CommandHandler {
CallStatement
call
,
VariableAssignment
params
)
{
//ProofMacro m = macros.get(call.getCommand());
macros
.
forEach
((
k
,
v
)
->
{
System
.
out
.
println
(
k
);
});
Parameters
p
=
new
Parameters
();
p
.
put
(
new
Variable
(
"#2"
),
new
StringLiteral
(
call
.
getCommand
()));
CallStatement
macroCall
=
new
CallStatement
(
"macro"
,
p
);
macroCall
.
setRuleContext
(
call
.
getRuleContext
());
VariableAssignment
newParam
=
new
VariableAssignment
(
null
);
newParam
.
declare
(
"#2"
,
Type
.
STRING
);
newParam
.
assign
(
"#2"
,
Value
.
from
(
call
.
getCommand
()));
//macro proofscript command
interpreter
.
getFunctionLookup
().
callCommand
(
interpreter
,
call
,
params
);
interpreter
.
getFunctionLookup
().
callCommand
(
interpreter
,
macroCall
,
newParam
);
//TODO change MacroCommand.Parameters to public
}
}
src/main/java/edu/kit/formal/interpreter/funchdl/ProofScriptCommandBuilder.java
View file @
f0a7e8cf
...
...
@@ -47,7 +47,7 @@ public class ProofScriptCommandBuilder implements CommandHandler<KeyData> {
GoalNode
<
KeyData
>
expandedNode
=
state
.
getSelectedGoalNode
();
KeyData
kd
=
expandedNode
.
getData
();
Map
<
String
,
String
>
map
=
new
HashMap
<>();
params
.
asMap
().
forEach
((
k
,
v
)
->
map
.
put
(
k
.
getIdentifier
(),
v
.
toString
()));
params
.
asMap
().
forEach
((
k
,
v
)
->
map
.
put
(
k
.
getIdentifier
(),
v
.
getData
().
toString
()));
System
.
out
.
println
(
map
);
try
{
EngineState
estate
=
new
EngineState
(
kd
.
getProof
());
...
...
src/main/java/edu/kit/formal/interpreter/graphs/ProofTreeController.java
View file @
f0a7e8cf
...
...
@@ -108,6 +108,7 @@ public class ProofTreeController {
this
.
setCurrentGoals
(
newValue
);
});
});
//add listener to nextcomputed node, that is updated whenever a new node is added to the stategraph
nextComputedNode
.
addListener
((
observable
,
oldValue
,
newValue
)
->
{
//update statepointer
...
...
src/main/resources/META-INF/services/de.uka.ilkd.key.macros.scripts.ProofScriptCommand
0 → 100644
View file @
f0a7e8cf
#
# Script commands to be used in proof scripts
#
#de.uka.ilkd.key.macros.scripts.FinishSymbolicExecutionMacro
\ No newline at end of file
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