|
|
@ -119,14 +119,15 @@ module MakeNoCFG
|
|
|
|
module Interprocedural (Summ : Summary.S with type summary = A.astate) = struct
|
|
|
|
module Interprocedural (Summ : Summary.S with type summary = A.astate) = struct
|
|
|
|
|
|
|
|
|
|
|
|
let checker { Callbacks.get_proc_desc; proc_desc; proc_name; tenv; } extras =
|
|
|
|
let checker { Callbacks.get_proc_desc; proc_desc; proc_name; tenv; } extras =
|
|
|
|
let post_opt = ref None in
|
|
|
|
let analyze_ondemand_ _ pdesc =
|
|
|
|
let analyze_ondemand _source pdesc =
|
|
|
|
|
|
|
|
match compute_post (ProcData.make pdesc tenv extras) with
|
|
|
|
match compute_post (ProcData.make pdesc tenv extras) with
|
|
|
|
| Some post ->
|
|
|
|
| Some post ->
|
|
|
|
Summ.write_summary (Cfg.Procdesc.get_proc_name pdesc) post;
|
|
|
|
Summ.write_summary (Cfg.Procdesc.get_proc_name pdesc) post;
|
|
|
|
post_opt := Some post
|
|
|
|
Some post
|
|
|
|
| None ->
|
|
|
|
| None ->
|
|
|
|
post_opt := None in
|
|
|
|
None in
|
|
|
|
|
|
|
|
let analyze_ondemand source pdesc =
|
|
|
|
|
|
|
|
ignore (analyze_ondemand_ source pdesc) in
|
|
|
|
let callbacks =
|
|
|
|
let callbacks =
|
|
|
|
{
|
|
|
|
{
|
|
|
|
Ondemand.analyze_ondemand;
|
|
|
|
Ondemand.analyze_ondemand;
|
|
|
@ -136,10 +137,11 @@ module MakeNoCFG
|
|
|
|
then
|
|
|
|
then
|
|
|
|
begin
|
|
|
|
begin
|
|
|
|
Ondemand.set_callbacks callbacks;
|
|
|
|
Ondemand.set_callbacks callbacks;
|
|
|
|
analyze_ondemand DB.source_file_empty proc_desc;
|
|
|
|
let post_opt = analyze_ondemand_ DB.source_file_empty proc_desc in
|
|
|
|
Ondemand.unset_callbacks ();
|
|
|
|
Ondemand.unset_callbacks ();
|
|
|
|
end;
|
|
|
|
post_opt
|
|
|
|
!post_opt
|
|
|
|
end
|
|
|
|
|
|
|
|
else None
|
|
|
|
end
|
|
|
|
end
|
|
|
|
end
|
|
|
|
end
|
|
|
|
|
|
|
|
|
|
|
|