Skip to content

Commit 066e8c8

Browse files
committed
Fix unknown pointer case in base get (closes #588)
1 parent e1d65b2 commit 066e8c8

File tree

1 file changed

+7
-8
lines changed

1 file changed

+7
-8
lines changed

src/analyses/base.ml

Lines changed: 7 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -359,20 +359,19 @@ struct
359359
| `Blob (c,s,_) -> c
360360
| x -> x
361361
in
362-
let f x =
363-
match Addr.to_var_offset x with
364-
| Some x -> f_addr x (* normal reference *)
365-
| None when x = Addr.NullPtr -> VD.bot () (* null pointer *)
366-
| None -> `Int (ID.top_of IChar) (* string pointer *)
362+
let f = function
363+
| Addr.Addr (x, o) -> f_addr (x, o)
364+
| Addr.NullPtr -> VD.bot () (* TODO: why bot? *)
365+
| Addr.UnknownPtr -> VD.top ()
366+
| Addr.StrPtr _ -> `Int (ID.top_of IChar)
367367
in
368368
(* We form the collecting function by joining *)
369369
let c x = match x with (* If address type is arithmetic, and our value is an int, we cast to the correct ik *)
370370
| `Int _ when Cil.isArithmeticType at -> VD.cast at x
371371
| _ -> x
372372
in
373-
let f x a = VD.join (c @@ f x) a in (* Finally we join over all the addresses in the set. If any of the
374-
* addresses is a topped value, joining will fail. *)
375-
try AD.fold f addrs (VD.bot ()) with SetDomain.Unsupported _ -> VD.top ()
373+
let f x a = VD.join (c @@ f x) a in (* Finally we join over all the addresses in the set. *)
374+
AD.fold f addrs (VD.bot ())
376375
in
377376
if M.tracing then M.traceu "get" "Result: %a\n" VD.pretty res;
378377
res

0 commit comments

Comments
 (0)