|
|
@ -548,14 +548,20 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
|
|
|
|
specs
|
|
|
|
specs
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
let merge_callee_map call_site pdesc callee_pname astate =
|
|
|
|
let merge_callee_map call_site pdesc callee_pname tenv specs astate =
|
|
|
|
match Payload.read pdesc callee_pname with
|
|
|
|
match Payload.read pdesc callee_pname with
|
|
|
|
| None ->
|
|
|
|
| None ->
|
|
|
|
astate
|
|
|
|
astate
|
|
|
|
| Some callee_call_map ->
|
|
|
|
| Some callee_call_map ->
|
|
|
|
let add_call_site annot sink calls astate =
|
|
|
|
let add_call_site annot sink calls astate =
|
|
|
|
if AnnotReachabilityDomain.CallSites.is_empty calls then astate
|
|
|
|
if AnnotReachabilityDomain.CallSites.is_empty calls then astate
|
|
|
|
else Domain.add_call_site annot sink call_site astate
|
|
|
|
else
|
|
|
|
|
|
|
|
let pname = Procdesc.get_proc_name pdesc in
|
|
|
|
|
|
|
|
List.fold
|
|
|
|
|
|
|
|
~f:(fun astate (spec : AnnotationSpec.t) ->
|
|
|
|
|
|
|
|
if spec.sanitizer_predicate tenv pname then astate
|
|
|
|
|
|
|
|
else Domain.add_call_site annot sink call_site astate )
|
|
|
|
|
|
|
|
~init:astate specs
|
|
|
|
in
|
|
|
|
in
|
|
|
|
AnnotReachabilityDomain.fold
|
|
|
|
AnnotReachabilityDomain.fold
|
|
|
|
(fun annot sink_map astate ->
|
|
|
|
(fun annot sink_map astate ->
|
|
|
@ -570,7 +576,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
|
|
|
|
let caller_pname = Procdesc.get_proc_name pdesc in
|
|
|
|
let caller_pname = Procdesc.get_proc_name pdesc in
|
|
|
|
let call_site = CallSite.make callee_pname call_loc in
|
|
|
|
let call_site = CallSite.make callee_pname call_loc in
|
|
|
|
check_call tenv callee_pname caller_pname call_site astate extras
|
|
|
|
check_call tenv callee_pname caller_pname call_site astate extras
|
|
|
|
|> merge_callee_map call_site pdesc callee_pname
|
|
|
|
|> merge_callee_map call_site pdesc callee_pname tenv extras
|
|
|
|
| Sil.Load (id, exp, _, _) when is_tracking_exp astate exp ->
|
|
|
|
| Sil.Load (id, exp, _, _) when is_tracking_exp astate exp ->
|
|
|
|
Domain.add_tracking_var (Var.of_id id) astate
|
|
|
|
Domain.add_tracking_var (Var.of_id id) astate
|
|
|
|
| Sil.Store (Exp.Lvar pvar, _, exp, _) when is_tracking_exp astate exp ->
|
|
|
|
| Sil.Store (Exp.Lvar pvar, _, exp, _) when is_tracking_exp astate exp ->
|
|
|
|