Store Derivation Nodes in State Refinement Errors

Author: rcosta358

liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java

@@ -1,7 +1,7 @@
 package liquidjava.diagnostics.errors;
 
 import liquidjava.diagnostics.TranslationTable;
-import liquidjava.rj_language.ast.Expression;
+import liquidjava.rj_language.opt.derivation_node.ValDerivationNode;
 import spoon.reflect.cu.SourcePosition;
 
 /**
@@ -11,23 +11,23 @@
  */
 public class StateRefinementError extends LJError {
 
-    private final String expected;
-    private final String found;
+    private final ValDerivationNode expected;
+    private final ValDerivationNode found;
 
-    public StateRefinementError(SourcePosition position, Expression expected, Expression found,
+    public StateRefinementError(SourcePosition position, ValDerivationNode expected, ValDerivationNode found,
             TranslationTable translationTable, String customMessage) {
-        super("State Refinement Error",
-                String.format("Expected state %s but found %s", expected.toDisplayString(), found.toDisplayString()),
-                position, translationTable, customMessage);
-        this.expected = expected.toDisplayString();
-        this.found = found.toDisplayString();
+        super("State Refinement Error", String.format("Expected state %s but found %s",
+                expected.getValue().toDisplayString(), found.getValue().toDisplayString()), position, translationTable,
+                customMessage);
+        this.expected = expected;
+        this.found = found;
     }
 
-    public String getExpected() {
+    public ValDerivationNode getExpected() {
         return expected;
     }
 
-    public String getFound() {
+    public ValDerivationNode getFound() {
         return found;
     }
 }

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java

@@ -75,8 +75,8 @@ public <R> void visitCtMethod(CtMethod<R> method) {
                 String signature = method.getSignature();
                 String message = String.format("Could not find constructor '%s' for '%s'", signature, prefix);
                 String[] overloads = getOverloads(targetType, method);
-                diagnostics.add(new ExternalMethodNotFoundWarning(method.getPosition(), message, signature,
-                        prefix, overloads));
+                diagnostics.add(
+                        new ExternalMethodNotFoundWarning(method.getPosition(), message, signature, prefix, overloads));
             }
         } else {
             if (!methodExists(targetType, method)) {

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java

@@ -391,8 +391,8 @@ protected void throwStateRefinementError(SourcePosition position, Predicate foun
         gatherVariables(found, lrv, mainVars);
         TranslationTable map = new TranslationTable();
         VCImplication foundState = joinPredicates(found, mainVars, lrv, map);
-        throw new StateRefinementError(position, expected.getExpression(),
-                foundState.toConjunctions().simplify(context).getValue(), map, customMessage);
+        throw new StateRefinementError(position, expected.simplify(context),
+                foundState.toConjunctions().simplify(context), map, customMessage);
     }
 
     protected void throwStateConflictError(SourcePosition position, Predicate expected) throws StateConflictError {