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

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

    (* pretty-printing *)
    val var_str : t -> id list -> string
end