Skip to content

Commit 0d299f4

Browse files
committed
Add NullByteSet to API documentation (PR #1076)
1 parent c90eb12 commit 0d299f4

File tree

2 files changed

+11
-8
lines changed

2 files changed

+11
-8
lines changed

src/cdomains/nullByteSet.ml

Lines changed: 10 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,5 @@
1+
(** Abstract domains for tracking [NULL] bytes in C arrays. *)
2+
13
module MustSet = struct
24
module M = SetDomain.Reverse (SetDomain.ToppedSet (IntDomain.BigInt) (struct let topname = "All Null" end))
35
include M
@@ -109,7 +111,7 @@ module MustMaySet = struct
109111
| Definitely -> MustSet.interval_mem (l,u) musts
110112
| Possibly -> failwith "not implemented"
111113

112-
let remove mode i (musts, mays) min_size =
114+
let remove mode i (musts, mays) min_size =
113115
match mode with
114116
| Definitely -> (MustSet.remove i musts min_size, MaySet.remove i mays min_size)
115117
| Possibly -> (MustSet.remove i musts min_size, mays)
@@ -133,20 +135,20 @@ module MustMaySet = struct
133135
in
134136
let mays =
135137
match maxfull with
136-
| Some Some maxfull when Z.equal l Z.zero && Z.geq u maxfull ->
138+
| Some Some maxfull when Z.equal l Z.zero && Z.geq u maxfull ->
137139
MaySet.top ()
138140
| _ ->
139141
add_indexes l u mays
140142
in
141143
match mode with
142144
| Definitely -> (add_indexes l u musts, mays)
143145
| Possibly -> (musts, mays)
144-
146+
145147
let remove_interval mode (l,u) min_size (musts, mays) =
146148
match mode with
147149
| Definitely -> failwith "todo"
148150
| Possibly ->
149-
if Z.equal l Z.zero && Z.geq u min_size then
151+
if Z.equal l Z.zero && Z.geq u min_size then
150152
(MustSet.top (), mays)
151153
else
152154
(MustSet.filter ~min_size (fun x -> (Z.lt x l || Z.gt x u) && Z.lt x min_size) musts, mays)
@@ -164,8 +166,8 @@ module MustMaySet = struct
164166
let is_full_set mode (musts, mays) =
165167
match mode with
166168
| Definitely -> MustSet.is_bot musts
167-
| Possibly -> MaySet.is_top mays
168-
169+
| Possibly -> MaySet.is_top mays
170+
169171
let get_set mode (musts, mays) =
170172
match mode with
171173
| Definitely -> musts
@@ -174,10 +176,10 @@ module MustMaySet = struct
174176
let elements ?max_size ?min_size mode (musts, mays) =
175177
match mode with
176178
| Definitely ->failwith "todo"
177-
| Possibly -> MaySet.elements ?max_size mays
179+
| Possibly -> MaySet.elements ?max_size mays
178180

179181
let union_mays (must,mays) (_,mays2) = (must, MaySet.join mays mays2)
180-
182+
181183

182184
let precise_singleton i =
183185
(MustSet.singleton i, MaySet.singleton i)

src/goblint_lib.ml

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -219,6 +219,7 @@ module AddressDomain = AddressDomain
219219
module StructDomain = StructDomain
220220
module UnionDomain = UnionDomain
221221
module ArrayDomain = ArrayDomain
222+
module NullByteSet = NullByteSet
222223
module JmpBufDomain = JmpBufDomain
223224

224225
(** {5 Combined}

0 commit comments

Comments
 (0)