Skip to content

Commit 7efb3fa

Browse files
committed
CHC: check for zero
1 parent 574b2fb commit 7efb3fa

File tree

1 file changed

+2
-1
lines changed

1 file changed

+2
-1
lines changed

CodeHawk/CHC/cchpre/cCHCheckValid.ml

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -128,7 +128,8 @@ let rec get_num_value env e =
128128
| (PlusA, Some v1, Some v2) -> Some (v1#add v2)
129129
| (MinusA, Some v1, Some v2) -> Some (v1#sub v2)
130130
| (Mult, Some v1, Some v2) -> Some (v1#mult v2)
131-
| (Div, Some v1, Some v2) -> Some (v1#div v2)
131+
| (Div, Some v1, Some v2) when not (v2#equal numerical_zero) ->
132+
Some (v1#div v2)
132133
| (Mod, Some _, Some _) -> None
133134
(* TODO: add some code for mod Some (v1 mod v2) *)
134135
| _ -> None

0 commit comments

Comments
 (0)