Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
10
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Open sidebar
sarah.grebing
ProofScriptParser
Commits
a0ff0420
Commit
a0ff0420
authored
Sep 06, 2017
by
Sarah Grebing
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Testcase for cut rule, needs to be considered next
parent
bdef62d7
Pipeline
#13438
failed with stage
in 2 minutes and 51 seconds
Changes
7
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
Showing
7 changed files
with
47 additions
and
28 deletions
+47
-28
lang/src/main/antlr4/edu/kit/iti/formal/psdbg/parser/ScriptLanguage.g4
.../antlr4/edu/kit/iti/formal/psdbg/parser/ScriptLanguage.g4
+2
-1
lang/src/main/java/edu/kit/iti/formal/psdbg/parser/TransformAst.java
...in/java/edu/kit/iti/formal/psdbg/parser/TransformAst.java
+6
-1
rt-key/src/test/java/edu/kit/iti/formal/psdbg/interpreter/ExecuteTest.java
...ava/edu/kit/iti/formal/psdbg/interpreter/ExecuteTest.java
+11
-4
rt-key/src/test/resources/edu/kit/iti/formal/psdbg/interpreter/contraposition/cutTest.kps
...t/iti/formal/psdbg/interpreter/contraposition/cutTest.kps
+3
-0
rt-key/src/test/resources/edu/kit/iti/formal/psdbg/interpreter/contraposition/w_branching.kps
...i/formal/psdbg/interpreter/contraposition/w_branching.kps
+2
-2
rt/src/test/resources/edu/kit/iti/formal/psdbg/interpreter/simple1.txt
...esources/edu/kit/iti/formal/psdbg/interpreter/simple1.txt
+9
-9
ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/java/transitive/script.kps
.../kit/iti/formal/psdbg/examples/java/transitive/script.kps
+14
-11
No files found.
lang/src/main/antlr4/edu/kit/iti/formal/psdbg/parser/ScriptLanguage.g4
View file @
a0ff0420
...
...
@@ -178,6 +178,7 @@ INDENT : '{' ;
DEDENT : '}' ;
SEMICOLON : ';' ;
COLON : ':' ;
HEAPSIMP:'heap-simp';
STRING_LITERAL
...
...
@@ -208,4 +209,4 @@ EXE_MARKER: '\u2316' -> channel(HIDDEN);
DIGITS : DIGIT+ ;
fragment DIGIT : [0-9] ;
ID : [a-zA-Z] ([_a-zA-Z0-9] | '.' | '\\')*;
\ No newline at end of file
ID : ([a-zA-Z]|'#') ([_a-zA-Z0-9] | '.' | '\\'| '#')*;
\ No newline at end of file
lang/src/main/java/edu/kit/iti/formal/psdbg/parser/TransformAst.java
View file @
a0ff0420
...
...
@@ -364,7 +364,12 @@ public class TransformAst implements ScriptLanguageVisitor<Object> {
public
Object
visitScriptCommand
(
ScriptLanguageParser
.
ScriptCommandContext
ctx
)
{
CallStatement
scs
=
new
CallStatement
();
scs
.
setRuleContext
(
ctx
);
scs
.
setCommand
(
ctx
.
cmd
.
getText
());
String
commandName
=
ctx
.
cmd
.
getText
();
//Sonderfall für KeYs heap-simp macro
if
(
commandName
.
equals
(
"heap_simp"
))
{
commandName
=
"heap-simp"
;
}
scs
.
setCommand
(
commandName
);
if
(
ctx
.
parameters
()
!=
null
)
{
scs
.
setParameters
((
Parameters
)
ctx
.
parameters
().
accept
(
this
));
}
...
...
rt-key/src/test/java/edu/kit/iti/formal/psdbg/interpreter/ExecuteTest.java
View file @
a0ff0420
package
edu.kit.iti.formal.psdbg.interpreter
;
import
edu.kit.iti.formal.psdbg.interpreter.Execute
;
import
edu.kit.iti.formal.psdbg.interpreter.Interpreter
;
import
static
edu
.
kit
.
iti
.
formal
.
psdbg
.
TestHelper
.
getFile
;
import
edu.kit.iti.formal.psdbg.interpreter.data.KeyData
;
import
org.apache.commons.cli.ParseException
;
import
org.junit.Test
;
import
java.io.IOException
;
import
static
edu
.
kit
.
iti
.
formal
.
psdbg
.
TestHelper
.
getFile
;
/**
* @author Alexander Weigl
* @version 1 (28.05.17)
...
...
@@ -47,4 +44,14 @@ public class ExecuteTest {
System
.
out
.
println
(
i
.
getCurrentState
());
}
@Test
public
void
testContrapositionCut
()
throws
IOException
,
ParseException
{
Execute
execute
=
create
(
getFile
(
getClass
(),
"contraposition/contraposition.key"
),
"-s"
,
getFile
(
getClass
(),
"contraposition/cutTest.kps"
));
Interpreter
<
KeyData
>
i
=
execute
.
run
();
System
.
out
.
println
(
i
.
getCurrentState
());
}
}
\ No newline at end of file
rt-key/src/test/resources/edu/kit/iti/formal/psdbg/interpreter/contraposition/cutTest.kps
0 → 100644
View file @
a0ff0420
script cutTest(){
cut #2=`p`;
}
\ No newline at end of file
rt-key/src/test/resources/edu/kit/iti/formal/psdbg/interpreter/contraposition/w_branching.kps
View file @
a0ff0420
...
...
@@ -2,8 +2,8 @@ script cpwb () {
impRight;
impLeft;
cases{
case match `==>
p
`:{
auto;
case match `==>
?X
`:{
auto;
}
default:{
auto;
...
...
rt/src/test/resources/edu/kit/iti/formal/psdbg/interpreter/simple1.txt
View file @
a0ff0420
...
...
@@ -10,27 +10,27 @@ script Simple1(i:int, j:int) {
assertEq i 4;
assert (i=4) & j=8;
split;
print_state;
//
print_state;
foreach {
assert (i=4) & j=8;
split 5;
print_state;
//
print_state;
}
print_state;
//
print_state;
cases {
case match `(?<X>.*).b.a` using [X : string]
{
case match `(?<X>.*).b.a` using [X : string]
:
assertEq X 'abc' msg='bla bla';
print_state;
}
case match '.*b' {
case match '.*b' :
print_state;
}
default {
default :
print_state;
}
}
}
\ No newline at end of file
ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/java/transitive/script.kps
View file @
a0ff0420
script prove_transitive(){
symbex;
symbex;
foreach{
heap_simp;
}
cases{
case match
`seqPerm(?Res0Copy, ?Arr),
`seqPerm(?Res0Copy, ?Arr),
seqPerm(?Res0Sort, ?Res0Copy),
seqPerm(?Res1Copy0, ?Res0Sort),
seqPerm(?Res2Copy1, ?Res0Sort) ==>
seqPerm(?Res2Copy1, ?Arr)`
using [ ?Res0Copy: Seq, ?Arr: Seq,?Res0Sort: Seq, ?Res1Copy0: Seq, ?Res2Copy1: Seq, ?Res0Sort: Seq ]
:
{
SeqPermSym on=`seqPerm(?Res0Copy, ?Arr) ==>`;
seqPerm(?Res2Copy1, ?Arr)`:
SeqPermSym on=`seqPerm(?Res0Copy, ?Arr) ==>`;
SeqPermSym on=`seqPerm(?Res0Sort, ?Res0Copy) ==>`;
SeqPermSym on=`seqPerm(?Res1Copy0, ?Res0Sort)==>`;
SeqPermSym on=`seqPerm(?Res2Copy1, ?Res0Sort) ==>`;
...
...
@@ -17,22 +20,22 @@ script prove_transitive(){
with=`seqPerm(?Arr,?Res2Copy1)`;
SeqPermSym on=`seqPerm(?Arr,?Res2Copy1)`;
auto;
}
case match
`seqPerm(?Res0Copy, ?Arr),
`seqPerm(?Res0Copy, ?Arr),
seqPerm(?Res0Sort, ?Res0Copy),
seqPerm(?Res1Copy0, ?Res0Sort) ==>
seqPerm(?Res1Copy0, ?Arr)`
using [ ?Res0Copy: Seq, ?Arr: Seq,?Res0Sort: Seq, ?Res1Copy0: Seq, ?Res0Sort: Seq ]
:
{
SeqPermSym on=`seqPerm(?Res0Copy, ?Arr)`;
seqPerm(?Res1Copy0, ?Arr)`:
SeqPermSym on=`seqPerm(?Res0Copy, ?Arr)`;
SeqPermSym on=`seqPerm(?Res0Sort, ?Res0Copy)`;
SeqPermSym on=`seqPerm(?Res1Copy0, ?Res0Sort)`;
SeqPermTrans on=`seqPerm(?Res0Copy, ?Arr)`;
SeqPermTrans on=`seqPerm(?Arr, ?Res0Sort)`
SeqPermSym on=`==> seqPerm(?Res1Copy0, ?Arr)`;
auto;
}
default:
{
default:
auto;
}
}
}
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