Requested Changes

Author: rcosta358

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

@@ -14,7 +14,9 @@ public class StateConflictError extends LJError {
     private String className;
 
     public StateConflictError(CtElement element, Predicate predicate, String className) {
-        super("State Conflict Error", "Found multiple disjoint states in state transition", element);
+        super("State Conflict Error",
+                "Found multiple disjoint states in state transition — State transition can only go to one state of each state set",
+                element);
         this.predicate = predicate;
         this.className = className;
     }

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

@@ -174,7 +174,7 @@ public <T> void visitCtNewArray(CtNewArray<T> newArray) {
             } catch (ParsingException e) {
                 return; // error already in ErrorEmitter
             }
-            String name = String.format(Formats.RET, context.getCounter());
+            String name = String.format(Formats.FRESH, context.getCounter());
             if (c.getVariableNames().contains(Keys.WILDCARD)) {
                 c = c.substituteVariable(Keys.WILDCARD, name);
             } else {

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

@@ -304,14 +304,6 @@ void removePathVariableThatIncludes(String otherVar) {
                 .collect(Collectors.toList()).forEach(pathVariables::remove);
     }
 
-    // private void printVCs(String string, String stringSMT, Predicate expectedType) {
-    // System.out.println("\n----------------------------VC--------------------------------\n");
-    // System.out.println(string);
-    // System.out.println("\nSMT subtyping:" + stringSMT + " <: " + expectedType.toString());
-    // System.out.println("--------------------------------------------------------------");
-    // }
-
-    // Print
     // Errors---------------------------------------------------------------------------------------------------
 
     private HashMap<String, PlacementInCode> createMap(CtElement element, Predicate expectedType) {
@@ -369,13 +361,6 @@ private void printError(Exception e, Predicate premisesBeforeChange, Predicate e
         }
     }
 
-    // private void printError(Predicate premises, Predicate expectedType, CtElement element,
-    // HashMap<String, PlacementInCode> map, String s) {
-    // Predicate etMessageReady = expectedType; // substituteByMap(expectedType, map);
-    // Predicate cSMTMessageReady = premises; // substituteByMap(premises, map);
-    // ErrorHandler.printError(element, s, etMessageReady, cSMTMessageReady, map, errorEmitter);
-    // }
-
     public void printStateMismatchError(CtElement element, String method, Predicate c, String states) {
         List<RefinedVariable> lrv = new ArrayList<>(), mainVars = new ArrayList<>();
         gatherVariables(c, lrv, mainVars);

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java

@@ -498,25 +498,6 @@ private static Predicate changeState(TypeChecker tc, VariableInstance vi,
         return new Predicate();
     }
 
-    /**
-     * Method prepared to change all old vars in a predicate, however it has not been needed yet
-     *
-     * @param pred
-     * @param tc
-     *
-     * @return
-     */
-    // private static Predicate changeVarsFields(Predicate pred, TypeChecker tc) {
-    // Predicate noOld = pred;
-    // List<String> listVarsInOld = pred.getOldVariableNames();
-    // for (String varInOld : listVarsInOld) {
-    // Optional<VariableInstance> ovi = tc.getContext().getLastVariableInstance(varInOld);
-    // if (ovi.isPresent())
-    // noOld = noOld.changeOldMentions(varInOld, ovi.get().getName(), tc.getErrorEmitter());
-    // }
-    // return noOld;
-    // }
-
     private static Predicate checkOldMentions(Predicate transitionedState, String instanceName, String newInstanceName,
             TypeChecker tc) {
         return transitionedState.changeOldMentions(instanceName, newInstanceName, tc.getErrorEmitter());
@@ -534,12 +515,8 @@ private static Predicate checkOldMentions(Predicate transitionedState, String in
      */
     private static Predicate sameState(TypeChecker tc, VariableInstance variableInstance, String name,
             CtElement invocation) {
-        // if(variableInstance.getState() != null) {
         if (variableInstance.getRefinement() != null) {
             String newInstanceName = String.format(Formats.INSTANCE, name, tc.getContext().getCounter());
-            // Predicate c =
-            // variableInstance.getState().substituteVariable(variableInstance.getName(),
-            // newInstanceName);
             Predicate c = variableInstance.getRefinement().substituteVariable(Keys.WILDCARD, newInstanceName)
                     .substituteVariable(variableInstance.getName(), newInstanceName);
 
@@ -636,15 +613,5 @@ private static List<CtAnnotation<? extends Annotation>> getStateAnnotation(CtEle
         return element.getAnnotations().stream().filter(ann -> ann.getActualAnnotation().annotationType()
                 .getCanonicalName().contentEquals("liquidjava.specification.StateRefinement"))
                 .collect(Collectors.toList());
-
-        // List<CtAnnotation<? extends Annotation>> l = new ArrayList<CtAnnotation<?
-        // extends Annotation>>();
-        // for (CtAnnotation<? extends Annotation> ann : element.getAnnotations()) {
-        // String an = ann.getActualAnnotation().annotationType().getCanonicalName();
-        // if (an.contentEquals("liquidjava.specification.StateRefinement")) {
-        // l.add(ann);
-        // }
-        // }
-        // return l;
     }
 }

liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java

@@ -242,8 +242,8 @@ public static Predicate createLit(String value, String type) {
         Expression exp = switch (type) {
         case Types.BOOLEAN -> new LiteralBoolean(value);
         case Types.INT, Types.SHORT -> new LiteralInt(value);
-        case Types.DOUBLE, Types.LONG -> new LiteralReal(value);
-        default -> new LiteralReal(value);
+        case Types.DOUBLE, Types.LONG, Types.FLOAT -> new LiteralReal(value);
+        default -> throw new IllegalArgumentException("Unsupported literal type: " + type);
         };
         return new Predicate(exp);
     }