Skip to content

Commit ae73f92

Browse files
rodrigomilissercosta358
authored andcommitted
added basic support for boolean ghost variables
1 parent b9a8f5d commit ae73f92

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
@@ -81,9 +81,13 @@ public static void setDefaultState(RefinedFunction f, TypeChecker tc) {
8181
Predicate p = Predicate.createEquals(Predicate.createInvocation(sg.getQualifiedName(), s),
8282
Predicate.createLit("0", Utils.INT));
8383
c = Predicate.createConjunction(c, p);
84+
} else if (sg.getReturnType().toString().equals("boolean")) {
85+
Predicate p = Predicate.createEquals(Predicate.createInvocation(sg.getName(), s),
86+
Predicate.createLit("false", Utils.BOOLEAN));
87+
c = Predicate.createConjunction(c, p);
8488
} else {
8589
// TODO: Implement other stuff
86-
throw new RuntimeException("Ghost Functions not implemented for other types than int -> implement in"
90+
throw new RuntimeException("Ghost Functions not implemented for other types than int/boolean -> implement in"
8791
+ " AuxStateHandler defaultState");
8892
}
8993
}

0 commit comments

Comments
 (0)