summaryrefslogtreecommitdiffstats
path: root/abstract/environment_domain.ml
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