summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorAlex AUVOLAT <alex.auvolat@ens.fr>2014-05-28 18:16:57 +0200
committerAlex AUVOLAT <alex.auvolat@ens.fr>2014-05-28 18:16:57 +0200
commit1038c28dab7775278c67e941a5e29d6e128eb09d (patch)
tree5e50a984f03f3387cba050e1e9c83b3403384989
parenta30fa47b4272f8c79948b741f7c388dad53c8eea (diff)
downloadSemVerif-Projet-1038c28dab7775278c67e941a5e29d6e128eb09d.tar.gz
SemVerif-Projet-1038c28dab7775278c67e941a5e29d6e128eb09d.zip
Add boolean constants.
-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