summaryrefslogtreecommitdiff
path: root/abstract
diff options
context:
space:
mode:
authorAlex AUVOLAT <alex.auvolat@ens.fr>2014-05-18 18:21:18 +0200
committerAlex AUVOLAT <alex.auvolat@ens.fr>2014-05-18 18:21:18 +0200
commit4d59f3a805d0cca882caab353ac8ec0dd4c04f73 (patch)
treeada69c3799c7fbb0d0cb6100bff2f4c649907edb /abstract
parent9714afeb275360110161c870b50627128fda75a0 (diff)
downloadSemVerif-Projet-4d59f3a805d0cca882caab353ac8ec0dd4c04f73.tar.gz
SemVerif-Projet-4d59f3a805d0cca882caab353ac8ec0dd4c04f73.zip
Begin work on interface with Apron
Diffstat (limited to 'abstract')
-rw-r--r--abstract/relational_apron.ml37
1 files changed, 37 insertions, 0 deletions
diff --git a/abstract/relational_apron.ml b/abstract/relational_apron.ml
new file mode 100644
index 0000000..bd078cf
--- /dev/null
+++ b/abstract/relational_apron.ml
@@ -0,0 +1,37 @@
+open Apron
+open Util
+open Environment_domain
+
+module RelationalDomain : ENVIRONMENT_DOMAIN = struct
+
+ (* manager *)
+ type man = Polka.loose Polka.t
+ let manager = Polka.manager_alloc_loose ()
+
+ (* abstract elements *)
+ type t = man Abstract1.t
+
+ (* implementation *)
+ let init = Abstract1.top manager (Environment.make [||] [||])
+ let bottom = Abstract1.bottom manager (Environment.make [||] [||])
+ let is_bot = Abstract1.is_bottom manager
+
+ let addvar x id = x (* TODO *)
+ let rmvar x id = x (* TODO *)
+ let vars x =
+ List.map Var.to_string @@
+ Array.to_list @@ snd @@ Environment.vars @@ Abstract1.env x
+
+ let assign x id e = x (* TODO *)
+ let compare x e1 e2 = x (* TODO *)
+
+ let join = Abstract1.join manager
+ let meet = Abstract1.meet manager
+ let widen = Abstract1.widening manager
+
+ let subset = Abstract1.is_leq manager
+
+ let var_str x idl = "" (* TODO *)
+
+end
+