summaryrefslogtreecommitdiff
path: root/abstract/interpret.ml
diff options
context:
space:
mode:
Diffstat (limited to 'abstract/interpret.ml')
-rw-r--r--abstract/interpret.ml5
1 files changed, 5 insertions, 0 deletions
diff --git a/abstract/interpret.ml b/abstract/interpret.ml
index 2f9f378..cb32e22 100644
--- a/abstract/interpret.ml
+++ b/abstract/interpret.ml
@@ -27,8 +27,12 @@ module Make (E : ENVIRONMENT_DOMAIN) = struct
E.meet (condition e1 env) (condition e2 env)
| AST_binary (AST_OR, e1, e2) ->
E.join (condition e1 env) (condition e2 env)
+ | AST_bool_const true -> env
+ | AST_bool_const false -> E.bottom
(* transformations : remove not *)
+ | AST_unary(AST_NOT, (AST_bool_const x, _)) ->
+ condition (AST_bool_const (not x), snd cond) env
| AST_unary (AST_NOT, (AST_unary(AST_NOT, cond), _)) ->
condition cond env
| AST_unary (AST_NOT, (AST_binary(AST_AND, e1, e2), x)) ->
@@ -69,6 +73,7 @@ module Make (E : ENVIRONMENT_DOMAIN) = struct
(binop AST_OR (binop AST_LESS e1 e2) (binop AST_LESS e2 e1))
env
+
| _ -> env
end