Skip to content

Commit 85b4249

Browse files
committed
Add interface to Invariant
1 parent bce9f92 commit 85b4249

File tree

2 files changed

+18
-1
lines changed

2 files changed

+18
-1
lines changed

src/cdomain/value/domains/invariant.ml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
(** Invariants for witnesses. *)
1+
22

33
open GoblintCil
44

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
(** Invariants for witnesses. *)
2+
3+
include Lattice.S with type t = [ `Bot | `Lifted of GoblintCil.exp | `Top ]
4+
5+
val none: t
6+
val of_exp: GoblintCil.exp -> t
7+
8+
val (&&): t -> t -> t
9+
val (||): t -> t -> t
10+
11+
12+
type context = {
13+
path: int option;
14+
lvals: Lval.Set.t;
15+
}
16+
17+
val default_context : context

0 commit comments

Comments
 (0)