Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Sign in
Toggle navigation
Menu
Open sidebar
sarah.grebing
ProofScriptParser
Commits
57cce75f
Commit
57cce75f
authored
May 23, 2018
by
Lulu Luong
Browse files
Merge remote-tracking branch 'origin/master'
parents
b02a9af9
d1c3fb76
Changes
7
Hide whitespace changes
Inline
Side-by-side
rt-key/src/main/java/edu/kit/iti/formal/psdbg/LabelFactory.java
View file @
57cce75f
...
...
@@ -3,7 +3,6 @@ package edu.kit.iti.formal.psdbg;
import
de.uka.ilkd.key.proof.Goal
;
import
de.uka.ilkd.key.proof.Node
;
import
de.uka.ilkd.key.proof.Proof
;
import
javafx.util.Pair
;
import
lombok.val
;
import
org.apache.commons.lang.ArrayUtils
;
import
org.key_project.util.collection.ImmutableList
;
...
...
rt-key/src/main/java/edu/kit/iti/formal/psdbg/ValueInjector.java
View file @
57cce75f
...
...
@@ -13,8 +13,6 @@ import de.uka.ilkd.key.proof.Goal;
import
de.uka.ilkd.key.proof.Node
;
import
de.uka.ilkd.key.proof.Proof
;
import
edu.kit.iti.formal.psdbg.interpreter.data.TermValue
;
import
jdk.nashorn.internal.objects.annotations.Getter
;
import
jdk.nashorn.internal.objects.annotations.Setter
;
import
lombok.RequiredArgsConstructor
;
import
lombok.Value
;
...
...
rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/funchdl/SaveCommand.java
View file @
57cce75f
...
...
@@ -5,6 +5,9 @@ import edu.kit.iti.formal.psdbg.interpreter.data.KeyData;
import
edu.kit.iti.formal.psdbg.interpreter.data.SavePoint
;
import
edu.kit.iti.formal.psdbg.interpreter.data.VariableAssignment
;
import
edu.kit.iti.formal.psdbg.parser.ast.CallStatement
;
import
javafx.application.Platform
;
import
javafx.scene.control.Alert
;
import
javafx.scene.control.ButtonType
;
import
lombok.Getter
;
import
lombok.Setter
;
import
org.apache.logging.log4j.LogManager
;
...
...
@@ -13,6 +16,11 @@ import org.apache.logging.log4j.Logger;
import
javax.annotation.Nullable
;
import
java.io.File
;
import
java.io.IOException
;
import
java.util.Optional
;
import
java.util.concurrent.CyclicBarrier
;
import
java.util.concurrent.Semaphore
;
import
java.util.concurrent.atomic.AtomicBoolean
;
import
java.util.concurrent.locks.ReentrantLock
;
public
class
SaveCommand
implements
CommandHandler
<
KeyData
>
{
public
static
final
String
SAVE_COMMAND_NAME
=
"#save"
;
...
...
@@ -47,10 +55,28 @@ public class SaveCommand implements CommandHandler<KeyData> {
consoleLogger
.
info
(
"(Safepoint) Location to be saved to = "
+
newFile
.
getAbsolutePath
());
try
{
interpreter
.
getSelectedNode
().
getData
().
getProof
().
saveToFile
(
newFile
);
AtomicBoolean
execute
=
new
AtomicBoolean
(
sp
.
getForce
()
==
SavePoint
.
ForceOption
.
YES
);
if
(
sp
.
getForce
()
==
SavePoint
.
ForceOption
.
INTERACTIVE
){
Semaphore
semaphore
=
new
Semaphore
(
0
);
Platform
.
runLater
(()
->
{
Alert
a
=
new
Alert
(
Alert
.
AlertType
.
CONFIRMATION
);
a
.
setTitle
(
"Foo"
);
Optional
<
ButtonType
>
buttonType
=
a
.
showAndWait
();
if
(
buttonType
.
isPresent
()
&&
buttonType
.
get
()
==
ButtonType
.
OK
){
execute
.
set
(
true
);
}
semaphore
.
release
();
});
semaphore
.
acquire
();
}
if
(
execute
.
get
())
interpreter
.
getSelectedNode
().
getData
().
getProof
().
saveToFile
(
newFile
);
//TODO Call to key persistend facade
}
catch
(
IOException
e
)
{
e
.
printStackTrace
();
}
catch
(
InterruptedException
e
)
{
e
.
printStackTrace
();
}
}
...
...
rt-key/src/main/resources/services/edu.kit.iti.formal.psdbg.parser.function.ScriptFunction
View file @
57cce75f
edu.kit.iti.formal.psdbg.interpreter.functions.FindInSequence
\ No newline at end of file
edu.kit.iti.formal.psdbg.interpreter.functions.FindInSequence
rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/data/SavePoint.java
View file @
57cce75f
...
...
@@ -25,7 +25,11 @@ public class SavePoint {
if
(
isSaveCommand
(
call
))
{
Parameters
p
=
call
.
getParameters
();
name
=
evalAsText
(
p
,
"#2"
,
"not-available"
);
force
=
ForceOption
.
valueOf
(
evalAsText
(
p
,
"force"
,
"yes"
).
toUpperCase
());
try
{
force
=
ForceOption
.
valueOf
(
evalAsText
(
p
,
"force"
,
"yes"
).
toUpperCase
());
}
catch
(
IllegalArgumentException
e
){
}
try
{
startOffset
=
call
.
getRuleContext
().
getStart
().
getStartIndex
();
...
...
rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/dbg/BeforeExecution.java
View file @
57cce75f
package
edu.kit.iti.formal.psdbg.interpreter.dbg
;
import
javafx.event.Event
;
public
class
BeforeExecution
{
}
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/ScriptExecutionController.java
View file @
57cce75f
...
...
@@ -8,6 +8,7 @@ import edu.kit.iti.formal.psdbg.interpreter.KeYProofFacade;
import
edu.kit.iti.formal.psdbg.interpreter.KeyInterpreter
;
import
edu.kit.iti.formal.psdbg.interpreter.data.SavePoint
;
import
edu.kit.iti.formal.psdbg.interpreter.dbg.Breakpoint
;
import
edu.kit.iti.formal.psdbg.parser.Facade
;
import
edu.kit.iti.formal.psdbg.parser.ast.ProofScript
;
import
edu.kit.iti.formal.psdbg.parser.ast.Statements
;
import
javafx.scene.control.Alert
;
...
...
@@ -153,6 +154,7 @@ public class ScriptExecutionController {
private
void
executeScript0
(
InterpreterBuilder
ib
,
Collection
<?
extends
Breakpoint
>
breakpoints
,
ProofScript
ms
,
boolean
addInitBreakpoint
)
{
ib
.
setProblemPath
(
mainCtrl
.
getFacade
().
getFilepath
());
KeyInterpreter
interpreter
=
ib
.
build
();
mainCtrl
.
createDebuggerFramework
(
breakpoints
,
ms
,
addInitBreakpoint
,
interpreter
);
}
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a 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