Skip to content

Commit 61f70f8

Browse files
rcosta358rcosta358
committed
Formatting
1 parent bbc5e58 commit 61f70f8

File tree

3 files changed

+64
-133
lines changed

3 files changed

+64
-133
lines changed

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

Lines changed: 29 additions & 48 deletions
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,6 @@
66

77
import liquidjava.processor.context.*;
88
import liquidjava.rj_language.Predicate;
9-
import liquidjava.rj_language.ast.*;
109
import org.junit.jupiter.api.BeforeEach;
1110
import org.junit.jupiter.api.Test;
1211

@@ -15,8 +14,8 @@
1514
import spoon.reflect.reference.CtTypeReference;
1615

1716
/**
18-
* Integration tests for Context management with variables, functions, ghosts, and refinements
19-
* These tests verify that multiple components work together correctly in realistic scenarios
17+
* Integration tests for Context management with variables, functions, ghosts, and refinements These tests verify that
18+
* multiple components work together correctly in realistic scenarios
2019
*/
2120
class ContextIntegrationTest {
2221

@@ -35,35 +34,25 @@ void setUp() {
3534
void testCompleteVariableLifecycle() {
3635
// Scenario: Create variables, enter/exit contexts, track refinements
3736
CtTypeReference<Integer> intType = factory.Type().integerPrimitiveType();
38-
Predicate initialPred = Predicate.createOperation(
39-
Predicate.createVar("x"),
40-
">",
41-
Predicate.createLit("0", "int")
42-
);
37+
Predicate initialPred = Predicate.createOperation(Predicate.createVar("x"), ">",
38+
Predicate.createLit("0", "int"));
4339

4440
// Add variable in base scope
4541
context.addVarToContext("x", intType, initialPred, factory.createLiteral(0));
4642
assertTrue(context.hasVariable("x"), "Variable should exist in base scope");
4743

4844
// Enter new scope and add local variable
4945
context.enterContext();
50-
Predicate localPred = Predicate.createOperation(
51-
Predicate.createVar("y"),
52-
"<",
53-
Predicate.createLit("100", "int")
54-
);
46+
Predicate localPred = Predicate.createOperation(Predicate.createVar("y"), "<",
47+
Predicate.createLit("100", "int"));
5548
context.addVarToContext("y", intType, localPred, factory.createLiteral(0));
5649

5750
assertTrue(context.hasVariable("x"), "Base scope variable accessible in nested scope");
5851
assertTrue(context.hasVariable("y"), "Local variable exists");
5952
assertEquals(2, context.getAllVariables().size(), "Should have 2 variables");
6053

6154
// Update refinement for x
62-
Predicate newPred = Predicate.createOperation(
63-
Predicate.createVar("x"),
64-
">=",
65-
Predicate.createLit("5", "int")
66-
);
55+
Predicate newPred = Predicate.createOperation(Predicate.createVar("x"), ">=", Predicate.createLit("5", "int"));
6756
context.newRefinementToVariableInContext("x", newPred);
6857
assertEquals(newPred.toString(), context.getVariableRefinements("x").toString());
6958

@@ -84,15 +73,12 @@ void testFunctionRegistrationAndRetrieval() {
8473
func.setName("calculate");
8574
func.setClass("MathUtils");
8675
func.setType(intType);
87-
func.addArgRefinements("x", intType, Predicate.createOperation(
88-
Predicate.createVar("x"), ">", Predicate.createLit("0", "int")
89-
));
90-
func.addArgRefinements("y", intType, Predicate.createOperation(
91-
Predicate.createVar("y"), ">", Predicate.createLit("0", "int")
92-
));
93-
func.setRefReturn(Predicate.createOperation(
94-
Predicate.createVar("result"), ">", Predicate.createLit("0", "int")
95-
));
76+
func.addArgRefinements("x", intType,
77+
Predicate.createOperation(Predicate.createVar("x"), ">", Predicate.createLit("0", "int")));
78+
func.addArgRefinements("y", intType,
79+
Predicate.createOperation(Predicate.createVar("y"), ">", Predicate.createLit("0", "int")));
80+
func.setRefReturn(
81+
Predicate.createOperation(Predicate.createVar("result"), ">", Predicate.createLit("0", "int")));
9682

9783
context.addFunctionToContext(func);
9884

@@ -124,17 +110,14 @@ void testGhostStatesAndRefinements() {
124110
// Define states using GhostState
125111
List<CtTypeReference<?>> emptyList = List.of();
126112
GhostState isEmpty = new GhostState("isEmpty", emptyList, factory.Type().booleanPrimitiveType(), "Stack");
127-
isEmpty.setRefinement(Predicate.createEquals(
128-
Predicate.createInvocation("Stack.size", Predicate.createVar("this")),
129-
Predicate.createLit("0", "int")
130-
));
113+
isEmpty.setRefinement(
114+
Predicate.createEquals(Predicate.createInvocation("Stack.size", Predicate.createVar("this")),
115+
Predicate.createLit("0", "int")));
131116

132117
GhostState isNonEmpty = new GhostState("isNonEmpty", emptyList, factory.Type().booleanPrimitiveType(), "Stack");
133-
isNonEmpty.setRefinement(Predicate.createOperation(
134-
Predicate.createInvocation("Stack.size", Predicate.createVar("this")),
135-
">",
136-
Predicate.createLit("0", "int")
137-
));
118+
isNonEmpty.setRefinement(
119+
Predicate.createOperation(Predicate.createInvocation("Stack.size", Predicate.createVar("this")), ">",
120+
Predicate.createLit("0", "int")));
138121

139122
context.addToGhostClass("Stack", isEmpty);
140123
context.addToGhostClass("Stack", isNonEmpty);
@@ -158,7 +141,7 @@ void testVariableInstanceTracking() {
158141

159142
// Simulate assignment: x = 5
160143
VariableInstance instance1 = new VariableInstance("x_1", intType,
161-
Predicate.createEquals(Predicate.createVar("x_1"), Predicate.createLit("5", "int")));
144+
Predicate.createEquals(Predicate.createVar("x_1"), Predicate.createLit("5", "int")));
162145
var.addInstance(instance1);
163146
context.addSpecificVariable(instance1);
164147
context.addRefinementInstanceToVariable("x", "x_1");
@@ -168,8 +151,8 @@ void testVariableInstanceTracking() {
168151

169152
// Simulate second assignment: x = x + 1
170153
VariableInstance instance2 = new VariableInstance("x_2", intType,
171-
Predicate.createEquals(Predicate.createVar("x_2"),
172-
Predicate.createOperation(Predicate.createVar("x_1"), "+", Predicate.createLit("1", "int"))));
154+
Predicate.createEquals(Predicate.createVar("x_2"),
155+
Predicate.createOperation(Predicate.createVar("x_1"), "+", Predicate.createLit("1", "int"))));
173156
var.addInstance(instance2);
174157
context.addSpecificVariable(instance2);
175158
context.addRefinementInstanceToVariable("x", "x_2");
@@ -190,13 +173,13 @@ void testIfBranchCombination() {
190173

191174
// Then branch: x = 10
192175
VariableInstance thenInstance = new VariableInstance("x_then", intType,
193-
Predicate.createEquals(Predicate.createVar("x_then"), Predicate.createLit("10", "int")));
176+
Predicate.createEquals(Predicate.createVar("x_then"), Predicate.createLit("10", "int")));
194177
var.addInstance(thenInstance);
195178
context.variablesSetThenIf();
196179

197180
// Else branch: x = 20
198181
VariableInstance elseInstance = new VariableInstance("x_else", intType,
199-
Predicate.createEquals(Predicate.createVar("x_else"), Predicate.createLit("20", "int")));
182+
Predicate.createEquals(Predicate.createVar("x_else"), Predicate.createLit("20", "int")));
200183
var.addInstance(elseInstance);
201184
context.variablesSetElseIf();
202185

@@ -221,14 +204,12 @@ void testComplexScenarioWithMultipleComponents() {
221204
processFunc.setClass("Processor");
222205
processFunc.setType(intType);
223206

224-
Predicate precondition = Predicate.createOperation(
225-
Predicate.createVar("input"), ">", Predicate.createLit("0", "int")
226-
);
207+
Predicate precondition = Predicate.createOperation(Predicate.createVar("input"), ">",
208+
Predicate.createLit("0", "int"));
227209
processFunc.addArgRefinements("input", intType, precondition);
228210

229-
Predicate postcondition = Predicate.createOperation(
230-
Predicate.createVar("result"), ">=", Predicate.createVar("input")
231-
);
211+
Predicate postcondition = Predicate.createOperation(Predicate.createVar("result"), ">=",
212+
Predicate.createVar("input"));
232213
processFunc.setRefReturn(postcondition);
233214

234215
context.addFunctionToContext(processFunc);
@@ -253,7 +234,7 @@ void testGlobalVariableManagement() {
253234
CtTypeReference<Integer> intType = factory.Type().integerPrimitiveType();
254235

255236
context.addGlobalVariableToContext("GLOBAL_CONST", intType,
256-
Predicate.createEquals(Predicate.createVar("GLOBAL_CONST"), Predicate.createLit("42", "int")));
237+
Predicate.createEquals(Predicate.createVar("GLOBAL_CONST"), Predicate.createLit("42", "int")));
257238

258239
assertTrue(context.hasVariable("GLOBAL_CONST"), "Global variable should exist");
259240

‎liquidjava-verifier/src/test/java/liquidjava/integration/PredicateExpressionIntegrationTest.java‎

Lines changed: 14 additions & 39 deletions
Original file line numberDiff line numberDiff line change
@@ -12,20 +12,17 @@
1212
import org.junit.jupiter.api.Test;
1313

1414
import spoon.Launcher;
15-
import spoon.reflect.factory.Factory;
1615

1716
/**
18-
* Integration tests for Predicate and Expression classes working together
19-
* Tests realistic scenarios of expression building, manipulation, and evaluation
17+
* Integration tests for Predicate and Expression classes working together Tests realistic scenarios of expression
18+
* building, manipulation, and evaluation
2019
*/
2120
class PredicateExpressionIntegrationTest {
2221

23-
private Factory factory;
24-
2522
@BeforeEach
2623
void setUp() {
2724
Launcher launcher = new Launcher();
28-
factory = launcher.getFactory();
25+
launcher.getFactory();
2926
Context.getInstance().reinitializeAllContext();
3027
}
3128

@@ -77,11 +74,7 @@ void testVariableSubstitutionInComplexExpression() {
7774
@Test
7875
void testExpressionCloningAndModification() {
7976
// Create expression and clone it
80-
Predicate original = Predicate.createOperation(
81-
Predicate.createVar("x"),
82-
"+",
83-
Predicate.createLit("10", "int")
84-
);
77+
Predicate original = Predicate.createOperation(Predicate.createVar("x"), "+", Predicate.createLit("10", "int"));
8578

8679
Predicate cloned = original.clone();
8780

@@ -108,7 +101,7 @@ void testNestedFunctionInvocations() {
108101
assertTrue(result.contains("outer"), "Should contain outer function");
109102
assertTrue(result.contains("inner"), "Should contain inner function");
110103
assertTrue(result.contains("x") && result.contains("y") && result.contains("z"),
111-
"Should contain all variables");
104+
"Should contain all variables");
112105
}
113106

114107
@Test
@@ -118,11 +111,7 @@ void testIfThenElsePredicates() {
118111
Predicate zero = Predicate.createLit("0", "int");
119112
Predicate condition = Predicate.createOperation(x, ">", zero);
120113

121-
Predicate negX = Predicate.createOperation(
122-
Predicate.createLit("-1", "int"),
123-
"*",
124-
x
125-
);
114+
Predicate negX = Predicate.createOperation(Predicate.createLit("-1", "int"), "*", x);
126115

127116
Predicate ite = Predicate.createITE(condition, x, negX);
128117

@@ -160,18 +149,8 @@ void testOldVariableTracking() {
160149
void testVariableNameExtraction() {
161150
// Create complex expression and extract all variables
162151
Predicate expr = Predicate.createOperation(
163-
Predicate.createOperation(
164-
Predicate.createVar("a"),
165-
"+",
166-
Predicate.createVar("b")
167-
),
168-
"*",
169-
Predicate.createOperation(
170-
Predicate.createVar("c"),
171-
"-",
172-
Predicate.createVar("d")
173-
)
174-
);
152+
Predicate.createOperation(Predicate.createVar("a"), "+", Predicate.createVar("b")), "*",
153+
Predicate.createOperation(Predicate.createVar("c"), "-", Predicate.createVar("d")));
175154

176155
List<String> vars = expr.getVariableNames();
177156
assertEquals(4, vars.size(), "Should find 4 variables");
@@ -249,7 +228,7 @@ void testArithmeticWithVariablesAndConstants() {
249228
String result = division.toString();
250229
assertTrue(result.contains("x") && result.contains("y"), "Should contain both variables");
251230
assertTrue(result.contains("2") && result.contains("5") && result.contains("3"),
252-
"Should contain all constants");
231+
"Should contain all constants");
253232
}
254233

255234
@Test
@@ -307,9 +286,8 @@ void testComplexSubstitutionScenario() {
307286
Predicate func = Predicate.createInvocation("f", aPlusB, cTimesD);
308287

309288
List<String> vars = func.getVariableNames();
310-
assertTrue(vars.contains("a") && vars.contains("b") &&
311-
vars.contains("c") && vars.contains("d"),
312-
"Should contain all nested variables");
289+
assertTrue(vars.contains("a") && vars.contains("b") && vars.contains("c") && vars.contains("d"),
290+
"Should contain all nested variables");
313291
}
314292

315293
@Test
@@ -336,16 +314,13 @@ void testChainedOperations() {
336314
@Test
337315
void testPredicateEquality() {
338316
// Test that identical predicates are recognized
339-
Predicate p1 = Predicate.createOperation(
340-
Predicate.createVar("x"), "+", Predicate.createLit("5", "int"));
341-
Predicate p2 = Predicate.createOperation(
342-
Predicate.createVar("x"), "+", Predicate.createLit("5", "int"));
317+
Predicate p1 = Predicate.createOperation(Predicate.createVar("x"), "+", Predicate.createLit("5", "int"));
318+
Predicate p2 = Predicate.createOperation(Predicate.createVar("x"), "+", Predicate.createLit("5", "int"));
343319

344320
assertEquals(p1.toString(), p2.toString(), "Identical predicates have same string form");
345321

346322
// Different predicates
347-
Predicate p3 = Predicate.createOperation(
348-
Predicate.createVar("x"), "+", Predicate.createLit("6", "int"));
323+
Predicate p3 = Predicate.createOperation(Predicate.createVar("x"), "+", Predicate.createLit("6", "int"));
349324

350325
assertNotEquals(p1.toString(), p3.toString(), "Different predicates have different strings");
351326
}

0 commit comments

Comments
 (0)