diff options
| author | Alex AUVOLAT <alex.auvolat@ens.fr> | 2014-05-28 16:45:46 +0200 |
|---|---|---|
| committer | Alex AUVOLAT <alex.auvolat@ens.fr> | 2014-05-28 16:45:46 +0200 |
| commit | a30fa47b4272f8c79948b741f7c388dad53c8eea (patch) | |
| tree | e979e7362637ae8d1d44857b29fbd62ce99316e7 /abstract/interpret.ml | |
| parent | 77df0b0f119fc70624e4b830320a2b3e1034f7b5 (diff) | |
| download | SemVerif-Projet-a30fa47b4272f8c79948b741f7c388dad53c8eea.tar.gz SemVerif-Projet-a30fa47b4272f8c79948b741f7c388dad53c8eea.zip | |
RETAB, CLEANUP
Diffstat (limited to 'abstract/interpret.ml')
| -rw-r--r-- | abstract/interpret.ml | 28 |
1 files changed, 14 insertions, 14 deletions
diff --git a/abstract/interpret.ml b/abstract/interpret.ml index c599a76..2f9f378 100644 --- a/abstract/interpret.ml +++ b/abstract/interpret.ml @@ -4,18 +4,18 @@ open Util module Make (E : ENVIRONMENT_DOMAIN) = struct - let neg (e, l) = - (AST_unary(AST_NOT, (e, l))), l + let neg e = + (AST_unary(AST_NOT, e)), snd e - let binop op (e, l) e2 = - (AST_binary (op, (e,l), e2)), l - let m1 (e, l) = - binop AST_MINUS (e, l) (AST_int_const("1", l), l) - let p1 (e, l) = - binop AST_PLUS (e, l) (AST_int_const("1", l), l) + let binop op e e2 = + (AST_binary (op, e, e2)), snd e + let m1 e = + binop AST_MINUS e (AST_int_const("1", snd e), snd e) + let p1 e = + binop AST_PLUS e (AST_int_const("1", snd e), snd e) - let bottom_with_vars = - List.fold_left E.addvar E.bottom + let bottom_with_vars vlist = + List.fold_left E.addvar E.bottom vlist let rec condition cond env = begin match fst cond with @@ -29,7 +29,7 @@ module Make (E : ENVIRONMENT_DOMAIN) = struct E.join (condition e1 env) (condition e2 env) (* transformations : remove not *) - | AST_unary (AST_NOT, (AST_unary(AST_NOT, cond), x)) -> + | AST_unary (AST_NOT, (AST_unary(AST_NOT, cond), _)) -> condition cond env | AST_unary (AST_NOT, (AST_binary(AST_AND, e1, e2), x)) -> condition @@ -38,7 +38,7 @@ module Make (E : ENVIRONMENT_DOMAIN) = struct condition (AST_binary(AST_AND, neg e1, neg e2), x) env - | AST_unary (AST_NOT, (AST_binary(op, e1, e2), x)) -> + | AST_unary (AST_NOT, (AST_binary(op, e1, e2), _)) -> let op2 = match op with | AST_LESS_EQUAL -> AST_GREATER | AST_LESS -> AST_GREATER_EQUAL @@ -88,8 +88,8 @@ module Make (E : ENVIRONMENT_DOMAIN) = struct (interp_stmt (condition cond env) tb) (condition (neg cond) env) | AST_if (cond, tb, Some eb) -> - let e1 = (interp_stmt (condition cond env) tb) in - let e2 = (interp_stmt (condition (neg cond) env) eb) in + let e1 = interp_stmt (condition cond env) tb in + let e2 = interp_stmt (condition (neg cond) env) eb in E.join e1 e2 | AST_while (cond, body) -> (* loop unrolling *) |