diff options
Diffstat (limited to 'abstract/nonrelational.ml')
| -rw-r--r-- | abstract/nonrelational.ml | 38 |
1 files changed, 19 insertions, 19 deletions
diff --git a/abstract/nonrelational.ml b/abstract/nonrelational.ml index 7a83303..efa30dd 100644 --- a/abstract/nonrelational.ml +++ b/abstract/nonrelational.ml @@ -31,9 +31,9 @@ module ND (V : VALUE_DOMAIN) : NUMERICAL_ENVIRONMENT_DOMAIN = struct | NIdent id -> get_var env id | NIntConst i -> V.const i | NRealConst f -> V.const (int_of_float f) (* TODO floats *) - | NUnary (AST_UPLUS, e) -> eval env e - | NUnary (AST_UMINUS, e) -> V.neg (eval env e) - | NBinary (op, e1, e2) -> + | NUnary (AST_UPLUS, e, _) -> eval env e + | NUnary (AST_UMINUS, e, _) -> V.neg (eval env e) + | NBinary (op, e1, e2, _) -> let f = match op with | AST_PLUS -> V.add | AST_MINUS -> V.sub @@ -128,22 +128,22 @@ module ND (V : VALUE_DOMAIN) : NUMERICAL_ENVIRONMENT_DOMAIN = struct match lhs with | NIdent i -> [i, op, rhs] | NIntConst _ | NRealConst _ -> [] - | NUnary(AST_UPLUS, x) -> extract_var (x, op, rhs) - | NUnary(AST_UMINUS, x) -> - extract_var (x, inv_op op, NUnary(AST_UMINUS, x)) - | NBinary(AST_PLUS, a, b) -> - extract_var (a, op, NBinary(AST_MINUS, rhs, b)) @ - extract_var (b, op, NBinary(AST_MINUS, rhs, a)) - | NBinary(AST_MINUS, a, b) -> - extract_var (a, op, NBinary(AST_PLUS, rhs, b)) @ - extract_var (b, inv_op op, NBinary(AST_MINUS, a, rhs)) - | NBinary(AST_MUL, a, b) -> - extract_var (a, op, NBinary(AST_DIV, rhs, b)) @ - extract_var (b, op, NBinary(AST_DIV, rhs, a)) - | NBinary(AST_DIV, a, b) -> - extract_var (a, op, NBinary(AST_MUL, rhs, b)) @ - extract_var (b, inv_op op, NBinary(AST_DIV, a, rhs)) - | NBinary(AST_MOD, _, _) -> [] + | NUnary(AST_UPLUS, x, r) -> extract_var (x, op, rhs) + | NUnary(AST_UMINUS, x, r) -> + extract_var (x, inv_op op, NUnary(AST_UMINUS, x, r)) + | NBinary(AST_PLUS, a, b, r) -> + extract_var (a, op, NBinary(AST_MINUS, rhs, b, r)) @ + extract_var (b, op, NBinary(AST_MINUS, rhs, a, r)) + | NBinary(AST_MINUS, a, b, r) -> + extract_var (a, op, NBinary(AST_PLUS, rhs, b, r)) @ + extract_var (b, inv_op op, NBinary(AST_MINUS, a, rhs, r)) + | NBinary(AST_MUL, a, b, r) when r -> + extract_var (a, op, NBinary(AST_DIV, rhs, b, r)) @ + extract_var (b, op, NBinary(AST_DIV, rhs, a, r)) + | NBinary(AST_DIV, a, b, r) when r -> + extract_var (a, op, NBinary(AST_MUL, rhs, b, r)) @ + extract_var (b, inv_op op, NBinary(AST_DIV, a, rhs, r)) + | NBinary _ -> [] in let zop = match sign with | CONS_EQ -> AST_EQ | CONS_NE -> AST_NE |