summaryrefslogtreecommitdiff
path: root/abstract/apron_domain.ml
diff options
context:
space:
mode:
Diffstat (limited to 'abstract/apron_domain.ml')
-rw-r--r--abstract/apron_domain.ml6
1 files changed, 5 insertions, 1 deletions
diff --git a/abstract/apron_domain.ml b/abstract/apron_domain.ml
index 288f961..a929c0b 100644
--- a/abstract/apron_domain.ml
+++ b/abstract/apron_domain.ml
@@ -6,6 +6,11 @@ open Num_domain
open Apron
+(*
+ Link between our NUMERICAL_ENVIRONMENT_DOMAIN interface and Apron.
+ Mostly direct translation between the two.
+*)
+
module ND : NUMERICAL_ENVIRONMENT_DOMAIN = struct
(* manager *)
@@ -18,7 +23,6 @@ module ND : NUMERICAL_ENVIRONMENT_DOMAIN = struct
type t = man Abstract1.t
(* direct translation of numerical expressions into Apron tree expressions *)
- (* TODO : some variables have type real and not int... *)
let rec texpr_of_nexpr = function
| NIdent id -> Texpr1.Var (Var.of_string id)
| NIntConst i -> Texpr1.Cst (Coeff.s_of_mpqf (Mpqf.of_int i))