Skip to content

Commit 5b834f1

Browse files
committed
Fix GhostState constructor calls - remove duplicate parameter
GhostState constructor signature: GhostState(String name, List<CtTypeReference<?>>, CtTypeReference<?>, String prefix) Changed from incorrect 5 parameters to correct 4 parameters
1 parent 5eca3db commit 5b834f1

File tree

2 files changed

+4
-4
lines changed

2 files changed

+4
-4
lines changed

liquidjava-verifier/src/test/java/liquidjava/integration/ContextIntegrationTest.java

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -123,13 +123,13 @@ void testGhostStatesAndRefinements() {
123123

124124
// Define states using GhostState
125125
List<CtTypeReference<?>> emptyList = List.of();
126-
GhostState isEmpty = new GhostState("Stack", "isEmpty", emptyList, factory.Type().booleanPrimitiveType(), "Stack");
126+
GhostState isEmpty = new GhostState("isEmpty", emptyList, factory.Type().booleanPrimitiveType(), "Stack");
127127
isEmpty.setRefinement(Predicate.createEquals(
128128
Predicate.createInvocation("Stack.size", Predicate.createVar("this")),
129129
Predicate.createLit("0", "int")
130130
));
131131

132-
GhostState isNonEmpty = new GhostState("Stack", "isNonEmpty", emptyList, factory.Type().booleanPrimitiveType(), "Stack");
132+
GhostState isNonEmpty = new GhostState("isNonEmpty", emptyList, factory.Type().booleanPrimitiveType(), "Stack");
133133
isNonEmpty.setRefinement(Predicate.createOperation(
134134
Predicate.createInvocation("Stack.size", Predicate.createVar("this")),
135135
">",

liquidjava-verifier/src/test/java/liquidjava/integration/VerificationWorkflowIntegrationTest.java

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -175,13 +175,13 @@ void testGhostStateVerificationWorkflow() {
175175

176176
// Define states
177177
List<CtTypeReference<?>> emptyList = List.of();
178-
GhostState empty = new GhostState("Stack", "isEmpty", emptyList, factory.Type().booleanPrimitiveType(), "Stack");
178+
GhostState empty = new GhostState("isEmpty", emptyList, factory.Type().booleanPrimitiveType(), "Stack");
179179
empty.setRefinement(Predicate.createEquals(
180180
Predicate.createInvocation("Stack.size", Predicate.createVar("this")),
181181
Predicate.createLit("0", "int")
182182
));
183183

184-
GhostState nonEmpty = new GhostState("Stack", "isNonEmpty", emptyList, factory.Type().booleanPrimitiveType(), "Stack");
184+
GhostState nonEmpty = new GhostState("isNonEmpty", emptyList, factory.Type().booleanPrimitiveType(), "Stack");
185185
nonEmpty.setRefinement(Predicate.createOperation(
186186
Predicate.createInvocation("Stack.size", Predicate.createVar("this")),
187187
">",

0 commit comments

Comments
 (0)