diff options
author | Alex Auvolat <alex.auvolat@ansys.com> | 2014-06-17 15:31:47 +0200 |
---|---|---|
committer | Alex Auvolat <alex.auvolat@ansys.com> | 2014-06-17 15:31:47 +0200 |
commit | ce4f339ced19e2ff7d79c2c8ec5b3ee478d5d365 (patch) | |
tree | ea18aa2b09601987bf3f2978c4986679b80e47a7 /abstract/environment_domain.ml | |
parent | d57e3491720e912b4e2fd6c73f9d356901a42df5 (diff) | |
download | scade-analyzer-ce4f339ced19e2ff7d79c2c8ec5b3ee478d5d365.tar.gz scade-analyzer-ce4f339ced19e2ff7d79c2c8ec5b3ee478d5d365.zip |
Add bindings to apron. Next : work on abstract interpret.
Diffstat (limited to 'abstract/environment_domain.ml')
-rw-r--r-- | abstract/environment_domain.ml | 36 |
1 files changed, 36 insertions, 0 deletions
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 + + |