Improve Ghost Default Values in AuxStateHandler

Author: rcosta358

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

@@ -79,19 +79,15 @@ public static void setDefaultState(RefinedFunction f, TypeChecker tc) {
         Predicate c = new Predicate();
         List<GhostFunction> sets = getDifferentSets(tc, klass); // ??
         for (GhostFunction sg : sets) {
-            if (sg.getReturnType().toString().equals("int")) {
-                Predicate p = Predicate.createEquals(Predicate.createInvocation(sg.getName(), s),
-                        Predicate.createLit("0", Utils.INT));
-                c = Predicate.createConjunction(c, p);
-            } else if (sg.getReturnType().toString().equals("boolean")) {
-                Predicate p = Predicate.createEquals(Predicate.createInvocation(sg.getName(), s),
-                        Predicate.createLit("false", Utils.BOOLEAN));
-                c = Predicate.createConjunction(c, p);
-            } else {
-                // TODO: Implement other stuff
-                throw new RuntimeException("Ghost Functions not implemented for other types than int/boolean -> implement in"
-                        + " AuxStateHandler defaultState");
-            }
+            String retType = sg.getReturnType().toString();
+            Predicate typePredicate = switch (retType) {
+            case "int" -> Predicate.createLit("0", Utils.INT);
+            case "boolean" -> Predicate.createLit("false", Utils.BOOLEAN);
+            case "double" -> Predicate.createLit("0.0", Utils.DOUBLE);
+            default -> throw new RuntimeException("Ghost not implemented for type " + retType);
+            };
+            Predicate p = Predicate.createEquals(Predicate.createInvocation(sg.getName(), s), typePredicate);
+            c = Predicate.createConjunction(c, p);
         }
         ObjectState os = new ObjectState();
         os.setTo(c);