From ce4f339ced19e2ff7d79c2c8ec5b3ee478d5d365 Mon Sep 17 00:00:00 2001 From: Alex Auvolat Date: Tue, 17 Jun 2014 15:31:47 +0200 Subject: Add bindings to apron. Next : work on abstract interpret. --- abstract/environment_domain.ml | 36 ++++++++++++++++++++++++++++++++++++ 1 file changed, 36 insertions(+) create mode 100644 abstract/environment_domain.ml (limited to 'abstract/environment_domain.ml') diff --git a/abstract/environment_domain.ml b/abstract/environment_domain.ml new file mode 100644 index 0000000..5664474 --- /dev/null +++ b/abstract/environment_domain.ml @@ -0,0 +1,36 @@ +open Ast +open Formula + +module type ENVIRONMENT_DOMAIN = sig + type t + + (* construction *) + val init : t + val bottom : t + val is_bot : t -> bool + + (* variable management *) + val addvar : t -> id -> bool -> t (* integer or float variable ? *) + val rmvar : t -> id -> t + val vars : t -> (id * bool) list + val vbottom : t -> t (* bottom value with same environment *) + + (* abstract operation *) + val apply_f : t -> bool_expr -> t + val apply_cl : t -> conslist -> t + + (* set-theoretic operations *) + val join : t -> t -> t (* union *) + val meet : t -> t -> t (* intersection *) + val widen : t -> t -> t + + (* order *) + val subset : t -> t -> bool + val eq : t -> t -> bool + + (* pretty-printing *) + val print_vars : Format.formatter -> t -> id list -> unit + val print_all : Format.formatter -> t -> unit +end + + -- cgit v1.2.3