Skip to content

Commit 1fa8d17

Browse files
committed
Use bot instead of top for base mutex contents
This avoids unknown value escape warnings.
1 parent 53495c1 commit 1fa8d17

File tree

1 file changed

+3
-2
lines changed

1 file changed

+3
-2
lines changed

src/cdomains/valueDomain.ml

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -142,7 +142,7 @@ struct
142142

143143
let rec init_value (t: typ): t = (* top_value is not used here because structs, blob etc will not contain the right members *)
144144
match t with
145-
| t when is_mutex_type t -> `Top
145+
| t when is_mutex_type t -> `Bot (* use `Bot instead of `Top to avoid unknown value escape warnings *)
146146
| TInt (ik,_) -> `Int (ID.top_of ik)
147147
| TPtr _ -> `Address AD.top_ptr
148148
| TComp ({cstruct=true; _} as ci,_) -> `Struct (Structs.create (fun fd -> init_value fd.ftype) ci)
@@ -883,7 +883,8 @@ struct
883883
let mu = function `Blob (`Blob (y, s', orig), s, orig2) -> `Blob (y, ID.join s s',orig) | x -> x in
884884
let r =
885885
match x, offs with
886-
| _, _ when is_mutex_type t -> `Top (* hide mutex structure contents, not updated anyway *)
886+
| _, _ when is_mutex_type t -> (* hide mutex structure contents, not updated anyway *)
887+
`Bot (* use `Bot instead of `Top to avoid unknown value escape warnings *)
887888
| `Blob (x,s,orig), `Index (_,ofs) ->
888889
begin
889890
let l', o' = shift_one_over l o in

0 commit comments

Comments
 (0)