@@ -78,10 +78,12 @@ void testCompleteVariableLifecycle() {
7878 void testFunctionRegistrationAndRetrieval () {
7979 // Scenario: Register functions with refinements and retrieve them
8080 CtTypeReference <Integer > intType = factory .Type ().integerPrimitiveType ();
81- CtTypeReference <String > stringType = factory .Type ().stringType ();
8281
8382 // Create function with arguments and return refinement
84- RefinedFunction func = new RefinedFunction ("calculate" , "MathUtils" , intType , new Predicate ());
83+ RefinedFunction func = new RefinedFunction ();
84+ func .setName ("calculate" );
85+ func .setClass ("MathUtils" );
86+ func .setType (intType );
8587 func .addArgRefinements ("x" , intType , Predicate .createOperation (
8688 Predicate .createVar ("x" ), ">" , Predicate .createLit ("0" , "int" )
8789 ));
@@ -100,7 +102,10 @@ void testFunctionRegistrationAndRetrieval() {
100102 assertEquals (2 , retrieved .getArguments ().size (), "Should have 2 arguments" );
101103
102104 // Add another function with same name but different arity
103- RefinedFunction func2 = new RefinedFunction ("calculate" , "MathUtils" , intType , new Predicate ());
105+ RefinedFunction func2 = new RefinedFunction ();
106+ func2 .setName ("calculate" );
107+ func2 .setClass ("MathUtils" );
108+ func2 .setType (intType );
104109 func2 .addArgRefinements ("x" , intType , new Predicate ());
105110 context .addFunctionToContext (func2 );
106111
@@ -112,60 +117,34 @@ void testFunctionRegistrationAndRetrieval() {
112117 }
113118
114119 @ Test
115- void testGhostFunctionsAndStates () {
116- // Scenario: Register ghost functions and states, verify hierarchy
117- GhostFunction ghost1 = new GhostFunction ("ghostPredicate" , List .of (), factory .Type ().booleanPrimitiveType (), "TestClass" );
118- context .addGhostFunction (ghost1 );
119- assertTrue (context .hasGhost ("TestClass.ghostPredicate" ), "Should find ghost by qualified name" );
120- assertTrue (context .hasGhost ("ghostPredicate" ), "Should find ghost by simple name" );
121-
122- // Add ghost class with states
123- context .addGhostClass ("StateManager" );
124- GhostState state1 = new GhostState ("StateManager" , "initialized" , null , null );
125- state1 .setRefinement (Predicate .createLit ("true" , "boolean" ));
126- context .addToGhostClass ("StateManager" , state1 );
127-
128- GhostState state2 = new GhostState ("StateManager" , "ready" , null , null );
129- state2 .setRefinement (Predicate .createVar ("initialized" ));
130- context .addToGhostClass ("StateManager" , state2 );
131-
132- List <GhostState > states = context .getGhostState ("StateManager" );
133- assertEquals (2 , states .size (), "Should have 2 states" );
134-
135- // Verify state refinements
136- assertTrue (states .get (0 ).getRefinement ().toString ().contains ("true" ));
137- assertTrue (states .get (1 ).getRefinement ().toString ().contains ("initialized" ));
138- }
120+ void testGhostStatesAndRefinements () {
121+ // Scenario: Register ghost states and verify refinements
122+ context .addGhostClass ("Stack" );
123+
124+ // Define states using GhostState
125+ List <CtTypeReference <?>> emptyList = List .of ();
126+ GhostState isEmpty = new GhostState ("Stack" , "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+ ));
139131
140- @ Test
141- void testAliasManagement () {
142- // Scenario: Register and use aliases for complex predicates
143- Predicate complexPred = Predicate .createOperation (
144- Predicate .createOperation (
145- Predicate .createVar ("x" ),
146- "*" ,
147- Predicate .createVar ("x" )
148- ),
149- "+" ,
150- Predicate .createOperation (
151- Predicate .createVar ("y" ),
152- "*" ,
153- Predicate .createVar ("y" )
154- )
155- );
132+ GhostState isNonEmpty = new GhostState ("Stack" , "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+ ));
156138
157- AliasWrapper alias = new AliasWrapper ("distanceSquared" , complexPred ,
158- List .of ("x" , "y" ), List .of ("int" , "int" ));
159- context .addAlias (alias );
139+ context .addToGhostClass ("Stack" , isEmpty );
140+ context .addToGhostClass ("Stack" , isNonEmpty );
160141
161- List <AliasWrapper > aliases = context .getAlias ();
162- assertEquals (1 , aliases .size (), "Should have 1 alias" );
163- assertEquals ("distanceSquared" , aliases .get (0 ).getName ());
142+ List <GhostState > states = context .getGhostState ("Stack" );
143+ assertEquals (2 , states .size (), "Should have 2 states" );
164144
165- // Create new variables for substitution
166- List <String > newVars = alias .getNewVariables (context );
167- assertEquals (2 , newVars .size (), "Should generate 2 new variable names" );
168- assertTrue (newVars .get (0 ).contains ("alias_x" ), "Generated name should contain original" );
145+ // Verify state refinements
146+ assertTrue (states .get (0 ).getRefinement ().toString ().contains ("0" ));
147+ assertTrue (states .get (1 ).getRefinement ().toString ().contains (">" ));
169148 }
170149
171150 @ Test
@@ -233,17 +212,18 @@ void testIfBranchCombination() {
233212
234213 @ Test
235214 void testComplexScenarioWithMultipleComponents () {
236- // Realistic scenario: Function with refinements, variables, and ghosts
215+ // Realistic scenario: Function with refinements and variables
237216 CtTypeReference <Integer > intType = factory .Type ().integerPrimitiveType ();
238217
239- // Register a ghost function for validation
240- GhostFunction validationGhost = new GhostFunction ("isValid" ,
241- List .of (intType ), factory .Type ().booleanPrimitiveType (), "Validator" );
242- context .addGhostFunction (validationGhost );
218+ // Create function with precondition
219+ RefinedFunction processFunc = new RefinedFunction ();
220+ processFunc .setName ("process" );
221+ processFunc .setClass ("Processor" );
222+ processFunc .setType (intType );
243223
244- // Create function with precondition using ghost
245- RefinedFunction processFunc = new RefinedFunction ( "process" , "Processor " , intType , new Predicate ());
246- Predicate precondition = Predicate . createInvocation ( "Validator.isValid" , Predicate . createVar ( "input" ) );
224+ Predicate precondition = Predicate . createOperation (
225+ Predicate . createVar ( "input" ) , "> " , Predicate . createLit ( "0" , "int" )
226+ );
247227 processFunc .addArgRefinements ("input" , intType , precondition );
248228
249229 Predicate postcondition = Predicate .createOperation (
@@ -258,7 +238,6 @@ void testComplexScenarioWithMultipleComponents() {
258238 context .addVarToContext ("result" , intType , postcondition , null );
259239
260240 // Verify everything is integrated
261- assertTrue (context .hasGhost ("Validator.isValid" ), "Ghost function registered" );
262241 assertNotNull (context .getFunction ("process" , "Processor" ), "Function registered" );
263242 assertTrue (context .hasVariable ("input" ), "Input variable exists" );
264243 assertTrue (context .hasVariable ("result" ), "Result variable exists" );
@@ -300,4 +279,15 @@ void testCounterIncrement() {
300279 assertTrue (counter3 > counter2 , "Counter should continue incrementing" );
301280 assertEquals (1 , counter2 - counter1 , "Should increment by 1" );
302281 }
282+
283+ @ Test
284+ void testContextToString () {
285+ // Test context string representation
286+ CtTypeReference <Integer > intType = factory .Type ().integerPrimitiveType ();
287+ context .addVarToContext ("x" , intType , new Predicate (), null );
288+
289+ String result = context .toString ();
290+ assertNotNull (result , "toString should not return null" );
291+ assertTrue (result .contains ("Variables" ), "Should contain Variables section" );
292+ }
303293}
0 commit comments