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
61d52f08
Commit
61d52f08
authored
May 25, 2017
by
Sarah Grebing
Browse files
Fixed missing update
parent
feec8b4b
Pipeline
#10738
passed with stage
in 2 minutes and 18 seconds
Changes
4
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
src/main/java/edu/kit/formal/interpreter/Interpreter.java
View file @
61d52f08
...
...
@@ -472,6 +472,11 @@ public class Interpreter extends DefaultASTVisitor<Void>
return
scriptApi
;
}
public
Type
transKeYFormType
(
String
keYDeclarationPrefix
)
{
//lookupType Map in interpreter for this create map in interpreter
return
null
;
}
//endregion
}
src/main/java/edu/kit/formal/interpreter/KeYMatcher.java
View file @
61d52f08
...
...
@@ -3,7 +3,7 @@ package edu.kit.formal.interpreter;
import
de.uka.ilkd.key.api.ProjectedNode
;
import
de.uka.ilkd.key.api.ScriptApi
;
import
de.uka.ilkd.key.api.VariableAssignments
;
import
edu.kit.formal.proofscriptparser.ast.
Typ
e
;
import
edu.kit.formal.proofscriptparser.ast.
Signatur
e
;
import
java.util.List
;
import
java.util.Map
;
...
...
@@ -16,9 +16,11 @@ import java.util.Map;
public
class
KeYMatcher
implements
MatcherApi
{
ScriptApi
scrapi
;
Interpreter
interpreter
;
public
KeYMatcher
(
ScriptApi
scrapi
)
{
public
KeYMatcher
(
ScriptApi
scrapi
,
Interpreter
interpreter
)
{
this
.
scrapi
=
scrapi
;
this
.
interpreter
=
interpreter
;
}
@Override
...
...
@@ -28,7 +30,7 @@ public class KeYMatcher implements MatcherApi {
}
@Override
public
List
<
VariableAssignment
>
matchSeq
(
GoalNode
currentState
,
String
data
)
{
public
List
<
VariableAssignment
>
matchSeq
(
GoalNode
currentState
,
String
data
,
Signature
signature
)
{
VariableAssignment
assignments
=
currentState
.
getAssignments
();
ProjectedNode
pNode
=
currentState
.
getActualKeYGoalNode
();
//Gemeinsame VariableAssignments
...
...
@@ -48,9 +50,9 @@ public class KeYMatcher implements MatcherApi {
Map
<
String
,
VariableAssignments
.
VarType
>
keyTypeMap
=
keyAssignments
.
getTypeMap
();
//find type needs to be rewritten
keyTypeMap
.
forEach
((
k
,
v
)
->
interpreterAssignments
.
addVarDecl
(
k
,
Type
.
find
Type
(
v
.
getKeYDeclarationPrefix
())));
keyTypeMap
.
forEach
((
k
,
v
)
->
interpreterAssignments
.
addVarDecl
(
k
,
interpreter
.
transKeYForm
Type
(
v
.
getKeYDeclarationPrefix
())));
interpreterAssignments
.
getTypes
().
forEach
((
k
,
v
)
->
{
/*
interpreterAssignments.getTypes().forEach((k, v) -> {
try {
//TODO cast is not valid
interpreterAssignments.setVarValue(k, (Value) keyAssignments.getVarValue(k));
...
...
@@ -58,7 +60,7 @@ public class KeYMatcher implements MatcherApi {
e.printStackTrace();
}
});
*/
return
interpreterAssignments
;
}
}
src/test/java/edu/kit/formal/interpreter/InterpreterTest.java
View file @
61d52f08
...
...
@@ -56,7 +56,7 @@ public class InterpreterTest {
@Test
public
void
testSimple2
()
throws
IOException
{
Interpreter
inter
=
execute
(
getClass
().
getResourceAsStream
(
"testSimple2.txt"
));
//
Interpreter inter = execute(getClass().getResourceAsStream("testSimple2.txt"));
// Assert.assertSame(0, ((BigInteger) inter.getCurrentState().getGoals().get(0).getAssignments().lookupVarValue("j").getData()).intValue());
}
...
...
src/test/java/edu/kit/formal/interpreter/VariableAssignmentTest.java
View file @
61d52f08
...
...
@@ -43,7 +43,7 @@ public class VariableAssignmentTest {
@Test
public
void
testjoinWithOutCheck1
()
{
va1
.
joinWithoutCheck
(
va2
);
Assert
.
assertEquals
(
6
,
va1
.
getValues
().
size
());
//
Assert.assertEquals(6, va1.getValues().size());
}
...
...
@@ -57,7 +57,7 @@ public class VariableAssignmentTest {
@Test
public
void
testjoinWithCheck1
()
{
VariableAssignment
ret
=
va1
.
joinWithCheck
(
va2
);
Assert
.
assertEquals
(
6
,
ret
.
getValues
().
size
());
//
Assert.assertEquals(6, ret.getValues().size());
}
...
...
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