diff --git a/infer/src/checkers/abstractInterpreter.ml b/infer/src/checkers/abstractInterpreter.ml index d9b4a3045..bee8c7b0a 100644 --- a/infer/src/checkers/abstractInterpreter.ml +++ b/infer/src/checkers/abstractInterpreter.ml @@ -119,14 +119,15 @@ module MakeNoCFG module Interprocedural (Summ : Summary.S with type summary = A.astate) = struct let checker { Callbacks.get_proc_desc; proc_desc; proc_name; tenv; } extras = - let post_opt = ref None in - let analyze_ondemand _source pdesc = + let analyze_ondemand_ _ pdesc = match compute_post (ProcData.make pdesc tenv extras) with | Some post -> Summ.write_summary (Cfg.Procdesc.get_proc_name pdesc) post; - post_opt := Some post + Some post | None -> - post_opt := None in + None in + let analyze_ondemand source pdesc = + ignore (analyze_ondemand_ source pdesc) in let callbacks = { Ondemand.analyze_ondemand; @@ -136,10 +137,11 @@ module MakeNoCFG then begin 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 (); - end; - !post_opt + post_opt + end + else None end end