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

module type VALUE_DOMAIN = sig
    type t

    (* constructors *)
    val top     : t
    val bottom  : t
    val const   : Z.t -> t
    val rand    : Z.t -> Z.t -> t

    (* order *)
    val subset  : t -> t -> bool

    (* set-theoretic operations *)
    val join    : t -> t -> t   (* union *)
    val meet    : t -> t -> t   (* intersection *)
    val widen   : t -> t -> t

    (* arithmetic operations *)
    val neg     : t -> t
    val add     : t -> t -> t
    val sub     : t -> t -> t
    val mul     : t -> t -> t
    val div     : t -> t -> t
    val rem     : t -> t -> t

    (* boolean test *)
    val leq     : t -> t -> t * t   (* For intervals : [a, b] -> [c, d] -> ([a, min b d], [max a c, d]) *)
end