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

open Abstract_syntax_tree

module type ENVIRONMENT_DOMAIN = sig
    type t

    (* construction *)
    val init    : t
    val bottom  : t

    (* variable management *)
    val addvar  : t -> id -> t
    val rmvar   : t -> id -> t

    (* abstract operation *)
    val assign  : t -> id -> expr ext -> t      (*    S[id <- expr]     *)
    val compare : 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
end