Use readable qualified field names

Author: rcosta358

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

@@ -181,13 +181,13 @@ private static ObjectState getStates(CtAnnotation<? extends Annotation> ctAnnota
 
         // has from
         if (from != null) {
-            state.setFrom(createStatePredicate(from, f.getTargetClass(), tc, e, false, prefix));
+            state.setFrom(createStatePredicate(new Predicate(from, e, prefix), from, f.getTargetClass(), tc, e, false));
             state.setFromPosition(Utils.getLJAnnotationPosition(e, from));
         }
 
         // has to
         if (to != null) {
-            state.setTo(createStatePredicate(to, f.getTargetClass(), tc, e, true, prefix));
+            state.setTo(createStatePredicate(new Predicate(to, e, prefix), to, f.getTargetClass(), tc, e, true));
             state.setToPosition(Utils.getLJAnnotationPosition(e, to));
         }
 
@@ -210,10 +210,9 @@ private static ObjectState getStates(CtAnnotation<? extends Annotation> ctAnnota
      * 
      * @return the created predicate
      */
-    private static Predicate createStatePredicate(String value, String targetClass, TypeChecker tc, CtElement e,
-            boolean isTo, String prefix) throws LJError {
+    private static Predicate createStatePredicate(Predicate p, String value, String targetClass, TypeChecker tc,
+            CtElement e, boolean isTo) throws LJError {
         SourcePosition position = Utils.getLJAnnotationPosition(e, value);
-        Predicate p = new Predicate(value, e, prefix);
         if (!p.getExpression().isBooleanExpression()) {
             throw new InvalidRefinementError(position, "State refinement transition must be a boolean expression",
                     value);
@@ -422,8 +421,12 @@ public static void updateGhostField(CtFieldWrite<?> fw, TypeChecker tc) throws L
 
         ObjectState stateChange = new ObjectState();
         String prefix = field.getDeclaringType().getQualifiedName();
-        Predicate fromPredicate = createStatePredicate(stateChangeRefinementFrom, targetClass, tc, fw, false, prefix);
-        Predicate toPredicate = createStatePredicate(stateChangeRefinementTo, targetClass, tc, fw, true, prefix);
+        Predicate fromPredicate = createStatePredicate(new Predicate(), stateChangeRefinementFrom, targetClass, tc, fw,
+                false);
+        Predicate toPredicate = Predicate.createEquals(Predicate
+                .createInvocation(Utils.qualifyName(prefix, field.getSimpleName()), Predicate.createVar(Keys.THIS)),
+                Predicate.createVar(updatedVarName));
+        toPredicate = createStatePredicate(toPredicate, stateChangeRefinementTo, targetClass, tc, fw, true);
         stateChange.setFrom(fromPredicate);
         stateChange.setTo(toPredicate);
 

liquidjava-verifier/src/main/java/liquidjava/utils/FieldNames.java

@@ -7,13 +7,6 @@ private FieldNames() {
     }
 
     public static String of(CtFieldReference<?> field) {
-        StringBuilder name = new StringBuilder("this#");
-        field.getDeclaringType().getQualifiedName().codePoints().forEach(c -> {
-            if (c >= 'a' && c <= 'z' || c >= 'A' && c <= 'Z' || c >= '0' && c <= '9' || c == '_')
-                name.appendCodePoint(c);
-            else
-                name.append('#').append(Integer.toHexString(c)).append('#');
-        });
-        return name.append('#').append(field.getSimpleName()).toString();
+        return "this#" + field.getDeclaringType().getQualifiedName() + "." + field.getSimpleName();
     }
 }