summaryrefslogtreecommitdiff
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