diff options
| author | Alex AUVOLAT <alex.auvolat@ens.fr> | 2014-05-28 18:16:57 +0200 |
|---|---|---|
| committer | Alex AUVOLAT <alex.auvolat@ens.fr> | 2014-05-28 18:16:57 +0200 |
| commit | 1038c28dab7775278c67e941a5e29d6e128eb09d (patch) | |
| tree | 5e50a984f03f3387cba050e1e9c83b3403384989 /abstract/interpret.ml | |
| parent | a30fa47b4272f8c79948b741f7c388dad53c8eea (diff) | |
| download | SemVerif-Projet-1038c28dab7775278c67e941a5e29d6e128eb09d.tar.gz SemVerif-Projet-1038c28dab7775278c67e941a5e29d6e128eb09d.zip | |
Add boolean constants.
Diffstat (limited to 'abstract/interpret.ml')
| -rw-r--r-- | abstract/interpret.ml | 5 |
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 |