summaryrefslogtreecommitdiff
path: root/abstract/apron_domain.ml
diff options
context:
space:
mode:
authorAlex Auvolat <alex.auvolat@ansys.com>2014-07-15 11:35:12 +0200
committerAlex Auvolat <alex.auvolat@ansys.com>2014-07-15 11:35:12 +0200
commit4e66de932b91e91e4cadd943ff8859d6f69f57e1 (patch)
treeced73719216f2f1fd2eb9057001079a39dbad68e /abstract/apron_domain.ml
parent7205927e18ea355a619e95b1036aac9b94a22667 (diff)
downloadscade-analyzer-4e66de932b91e91e4cadd943ff8859d6f69f57e1.tar.gz
scade-analyzer-4e66de932b91e91e4cadd943ff8859d6f69f57e1.zip
Clean up & comment a bit.
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))