Skip to content

Commit 31ec501

Browse files
added basic support for boolean ghost variables
1 parent f8a0315 commit 31ec501

File tree

1 file changed

+5
-1
lines changed
  • liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers

1 file changed

+5
-1
lines changed

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

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -83,9 +83,13 @@ public static void setDefaultState(RefinedFunction f, TypeChecker tc) {
8383
Predicate p = Predicate.createEquals(Predicate.createInvocation(sg.getName(), s),
8484
Predicate.createLit("0", Utils.INT));
8585
c = Predicate.createConjunction(c, p);
86+
} else if (sg.getReturnType().toString().equals("boolean")) {
87+
Predicate p = Predicate.createEquals(Predicate.createInvocation(sg.getName(), s),
88+
Predicate.createLit("false", Utils.BOOLEAN));
89+
c = Predicate.createConjunction(c, p);
8690
} else {
8791
// TODO: Implement other stuff
88-
throw new RuntimeException("Ghost Functions not implemented for other types than int -> implement in"
92+
throw new RuntimeException("Ghost Functions not implemented for other types than int/boolean -> implement in"
8993
+ " AuxStateHandler defaultState");
9094
}
9195
}

0 commit comments

Comments
 (0)