Check If State Refinement Transitions Are Boolean Expressions

Author: rcosta358

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

@@ -65,8 +65,15 @@ private static void setConstructorStates(RefinedFunction f, List<CtAnnotation<?
             Map<String, CtExpression> m = an.getAllValues();
             String to = TypeCheckingUtils.getStringFromAnnotation(m.get("to"));
             ObjectState state = new ObjectState();
-            if (to != null)
-                state.setTo(new Predicate(to, element, tc.getErrorEmitter()));
+            if (to != null) {
+                Predicate p = new Predicate(to, element, tc.getErrorEmitter());
+                if (!p.getExpression().isBooleanExpression()) {
+                    ErrorHandler.printCustomError(element, "State refinement must be a boolean expression",
+                            tc.getErrorEmitter());
+                    return;
+                }
+                state.setTo(p);
+            }
             l.add(state);
         }
         f.setAllStates(l);
@@ -176,6 +183,10 @@ private static ObjectState getStates(CtAnnotation<? extends Annotation> ctAnnota
     private static Predicate createStatePredicate(String value, /* RefinedFunction f */ String targetClass,
             TypeChecker tc, CtElement e, boolean isTo, String prefix) throws ParsingException {
         Predicate p = new Predicate(value, e, tc.getErrorEmitter(), prefix);
+        if (!p.getExpression().isBooleanExpression()) {
+            ErrorHandler.printCustomError(e, "State refinement must be a boolean expression", tc.getErrorEmitter());
+            return new Predicate();
+        }
         String t = targetClass; // f.getTargetClass();
         CtTypeReference<?> r = tc.getFactory().Type().createReference(t);