[hil] don't let clients pass `debug:true`

Reviewed By: ddino

Differential Revision: D6149943

fbshipit-source-id: c68ec94
master
Sam Blackshear 7 years ago committed by Facebook Github Bot
parent fe89c5688c
commit 0a5c10c8ef

@ -88,8 +88,7 @@ struct
module Interpreter =
AbstractInterpreter.Make (CFG) (Make (MakeTransferFunctions) (DefaultConfig))
let compute_post ?(debug= Config.debug_mode) proc_data ~initial =
let compute_post proc_data ~initial =
let initial' = (initial, IdAccessPathMapDomain.empty) in
Option.map ~f:fst (Interpreter.compute_post ~debug proc_data ~initial:initial')
Option.map ~f:fst (Interpreter.compute_post ~debug:false proc_data ~initial:initial')
end

@ -41,7 +41,7 @@ module MakeAbstractInterpreter
module type of AbstractInterpreter.Make (CFG) (Make (MakeTransferFunctions) (DefaultConfig))
val compute_post :
?debug:bool -> Interpreter.TransferFunctions.extras ProcData.t
Interpreter.TransferFunctions.extras ProcData.t
-> initial:MakeTransferFunctions(CFG).Domain.astate
-> MakeTransferFunctions(CFG).Domain.astate option
(** compute and return the postcondition for the given procedure starting from [initial]. If

@ -135,6 +135,5 @@ module Analyzer = LowerHil.MakeAbstractInterpreter (ProcCfg.Exceptional) (Transf
let checker {Callbacks.summary; proc_desc; tenv} =
let initial = Domain.empty in
let proc_data = ProcData.make proc_desc tenv summary in
ignore (Analyzer.compute_post proc_data ~initial ~debug:false) ;
ignore (Analyzer.compute_post proc_data ~initial) ;
summary

@ -185,7 +185,7 @@ let checker {Callbacks.summary; proc_desc; tenv} =
(* Assume all fields are not null in the beginning *)
let initial = Domain.empty in
let proc_data = ProcData.make_default proc_desc tenv in
match Analyzer.compute_post proc_data ~initial ~debug:false with
match Analyzer.compute_post proc_data ~initial with
| Some post ->
report post proc_data ; summary
| None ->

@ -1144,7 +1144,7 @@ let analyze_procedure {Callbacks.proc_desc; get_proc_desc; tenv; summary} =
in
{RacerDDomain.empty with ownership; threads}
in
match Analyzer.compute_post proc_data ~initial ~debug:false with
match Analyzer.compute_post proc_data ~initial with
| Some {threads; locks; accesses; ownership; attribute_map} ->
let return_var_ap =
AccessPath.of_pvar
@ -1883,4 +1883,3 @@ let file_analysis {Callbacks.procedures} =
else (module MayAliasQuotientedAccessListMap) )
class_env))
(aggregate_by_class procedures)

@ -118,7 +118,7 @@ let checker {Callbacks.summary; proc_desc; tenv} : Specs.summary =
in
let extras = FormalMap.make proc_desc in
let proc_data = ProcData.make proc_desc tenv extras in
match Analyzer.compute_post proc_data ~initial:ResourceLeakDomain.initial ~debug:false with
match Analyzer.compute_post proc_data ~initial:ResourceLeakDomain.initial with
| Some post ->
(* 1(f) *)
report post proc_data ;
@ -127,4 +127,3 @@ let checker {Callbacks.summary; proc_desc; tenv} : Specs.summary =
L.(die InternalError)
"Analyzer failed to compute post for %a" Typ.Procname.pp
(Procdesc.get_proc_name proc_data.pdesc)

Loading…
Cancel
Save