File tree Expand file tree Collapse file tree 1 file changed +7
-8
lines changed Expand file tree Collapse file tree 1 file changed +7
-8
lines changed Original file line number Diff line number Diff 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
You can’t perform that action at this time.
0 commit comments