-
Notifications
You must be signed in to change notification settings - Fork 0
/
domain.ml
47 lines (31 loc) · 1004 Bytes
/
domain.ml
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
35
36
37
38
39
40
41
42
43
44
45
46
47
(* Abstract interpretation - Domains signature (abstract or concrete) *)
open Ast
module type DOMAIN =
sig
(* abstract elements type *)
type t
(* initial empty environment *)
val init: unit -> t
(* empty set *)
val bottom: unit -> t
(* add a variable in environment *)
val add_var: t -> string -> t
(* remove a variable in environment *)
val del_var: t -> string -> t
(* assign an integer expression to a variable *)
val assign: t -> string -> expr -> t
(* filter environments *)
val compare: t -> expr -> binop -> expr -> t
(* abstract join *)
val join: t -> t -> t
(* abstract intersection *)
val meet: t -> t -> t
(* abstract widening *)
val widen: t -> t -> t
(* abstract element is included in another one *)
val subset: t -> t -> bool
(* abstract element is the empty set *)
val is_bottom: t -> bool
val print: int -> t -> string -> unit
val print_all: int -> t -> unit
end