blob: b2d18c42e86bbae7047d479423ec9335d23cd506 (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
|
open Abstract_syntax_tree
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 -> t
val rmvar : t -> id -> t
val vars : t -> id list
(* abstract operation *)
val assign : t -> id -> expr ext -> t (* S[id <- expr] *)
val compare_leq : t -> expr ext -> expr ext -> t (* S[expr <= expr ?] *)
val compare_eq : t -> expr ext -> expr ext -> t (* S[expr = expr ?] *)
(* 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 var_str : t -> id list -> string
end
|
