diff options
Diffstat (limited to 'abstract/apron_domain.ml')
| -rw-r--r-- | abstract/apron_domain.ml | 20 |
1 files changed, 12 insertions, 8 deletions
diff --git a/abstract/apron_domain.ml b/abstract/apron_domain.ml index 45803fc..288f961 100644 --- a/abstract/apron_domain.ml +++ b/abstract/apron_domain.ml @@ -23,17 +23,21 @@ module ND : NUMERICAL_ENVIRONMENT_DOMAIN = struct | NIdent id -> Texpr1.Var (Var.of_string id) | NIntConst i -> Texpr1.Cst (Coeff.s_of_mpqf (Mpqf.of_int i)) | NRealConst r -> Texpr1.Cst (Coeff.s_of_mpqf (Mpqf.of_float r)) - | NUnary(AST_UPLUS, e) -> - texpr_of_nexpr e - | NUnary(AST_UMINUS, e) -> + | NUnary(AST_UPLUS, e, is_real) -> + Texpr1.Unop( + Texpr1.Cast, + texpr_of_nexpr e, + (if is_real then Texpr1.Real else Texpr1.Int), + Texpr1.Rnd) + | NUnary(AST_UMINUS, e, is_real) -> (* APRON bug ? Unary negate seems to not work correctly... *) Texpr1.Binop( Texpr1.Sub, Texpr1.Cst(Coeff.s_of_mpqf (Mpqf.of_string "0")), (texpr_of_nexpr e), - Texpr1.Int, - Texpr1.Zero) - | NBinary(op, e1, e2) -> + (if is_real then Texpr1.Real else Texpr1.Int), + Texpr1.Rnd) + | NBinary(op, e1, e2, is_real) -> let f = match op with | AST_PLUS -> Texpr1.Add | AST_MINUS -> Texpr1.Sub @@ -45,8 +49,8 @@ module ND : NUMERICAL_ENVIRONMENT_DOMAIN = struct f, (texpr_of_nexpr e1), (texpr_of_nexpr e2), - Texpr1.Int, - Texpr1.Zero) + (if is_real then Texpr1.Real else Texpr1.Int), + Texpr1.Rnd) (* direct translation of constraints into Apron constraints *) let tcons_of_cons env (eq, op) = |