diff options
author | Alex AUVOLAT <alex.auvolat@ens.fr> | 2014-05-18 18:21:18 +0200 |
---|---|---|
committer | Alex AUVOLAT <alex.auvolat@ens.fr> | 2014-05-18 18:21:18 +0200 |
commit | 4d59f3a805d0cca882caab353ac8ec0dd4c04f73 (patch) | |
tree | ada69c3799c7fbb0d0cb6100bff2f4c649907edb /abstract/relational_apron.ml | |
parent | 9714afeb275360110161c870b50627128fda75a0 (diff) | |
download | SemVerif-Projet-4d59f3a805d0cca882caab353ac8ec0dd4c04f73.tar.gz SemVerif-Projet-4d59f3a805d0cca882caab353ac8ec0dd4c04f73.zip |
Begin work on interface with Apron
Diffstat (limited to 'abstract/relational_apron.ml')
-rw-r--r-- | abstract/relational_apron.ml | 37 |
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 + |