Skip to content

Commit

Permalink
Use ReachableFromA in malloc_null
Browse files Browse the repository at this point in the history
  • Loading branch information
karoliineh committed Aug 23, 2023
1 parent 178a9c6 commit 08c9f1d
Showing 1 changed file with 8 additions and 4 deletions.
12 changes: 8 additions & 4 deletions src/analyses/malloc_null.ml
Original file line number Diff line number Diff line change
Expand Up @@ -95,10 +95,14 @@ struct
let remove_unreachable (ask: Queries.ask) (args: exp list) (st: D.t) : D.t =
let reachable =
let do_exp e =
match ask.f (Queries.ReachableFrom e) with
| a when not (Queries.LS.is_top a) ->
let to_extra (v,o) xs = AD.of_mval (v, Offs.of_exp o) :: xs in
Queries.LS.fold to_extra (Queries.LS.remove (dummyFunDec.svar, `NoOffset) a) []
match ask.f (Queries.ReachableFromA e) with
| a when not (Queries.AD.is_top a) ->
Queries.AD.fold (
fun addr xs ->
match addr with
| Queries.AD.Addr.Addr (v,o) -> AD.of_mval (v,o) :: xs
| _ -> xs
) a []
(* Ignore soundness warnings, as invalidation proper will raise them. *)
| _ -> []
in
Expand Down

0 comments on commit 08c9f1d

Please sign in to comment.