|
|
@ -708,18 +708,9 @@ let should_report_on_proc (_, _, proc_name, proc_desc) =
|
|
|
|
Procdesc.get_access proc_desc <> PredSymb.Private &&
|
|
|
|
Procdesc.get_access proc_desc <> PredSymb.Private &&
|
|
|
|
not (Annotations.pdesc_return_annot_ends_with proc_desc Annotations.visibleForTesting)
|
|
|
|
not (Annotations.pdesc_return_annot_ends_with proc_desc Annotations.visibleForTesting)
|
|
|
|
|
|
|
|
|
|
|
|
(* creates a map from proc_envs to postconditions *)
|
|
|
|
let analyze_procedure callback =
|
|
|
|
let make_results_table get_proc_desc file_env =
|
|
|
|
|
|
|
|
(* make a Map sending each element e of list l to (f e) *)
|
|
|
|
|
|
|
|
let map_post_computation_over_procs f l =
|
|
|
|
|
|
|
|
List.fold
|
|
|
|
|
|
|
|
~f:(fun m p -> ResultsTableType.add p (f p) m)
|
|
|
|
|
|
|
|
~init:ResultsTableType.empty
|
|
|
|
|
|
|
|
l in
|
|
|
|
|
|
|
|
let is_initializer tenv proc_name =
|
|
|
|
let is_initializer tenv proc_name =
|
|
|
|
Procname.is_constructor proc_name || FbThreadSafety.is_custom_init tenv proc_name in
|
|
|
|
Procname.is_constructor proc_name || FbThreadSafety.is_custom_init tenv proc_name in
|
|
|
|
let compute_post_for_procedure = (* takes proc_env as arg *)
|
|
|
|
|
|
|
|
fun (idenv, tenv, proc_name, proc_desc) ->
|
|
|
|
|
|
|
|
let open ThreadSafetyDomain in
|
|
|
|
let open ThreadSafetyDomain in
|
|
|
|
let has_lock = false in
|
|
|
|
let has_lock = false in
|
|
|
|
let return_attrs = AttributeSetDomain.empty in
|
|
|
|
let return_attrs = AttributeSetDomain.empty in
|
|
|
@ -761,17 +752,31 @@ let make_results_table get_proc_desc file_env =
|
|
|
|
end
|
|
|
|
end
|
|
|
|
else
|
|
|
|
else
|
|
|
|
Some empty in
|
|
|
|
Some empty in
|
|
|
|
let callback_arg =
|
|
|
|
|
|
|
|
let get_procs_in_file _ = [] in
|
|
|
|
|
|
|
|
{ Callbacks.get_proc_desc; get_procs_in_file; idenv; tenv; proc_name; proc_desc } in
|
|
|
|
|
|
|
|
match
|
|
|
|
match
|
|
|
|
Interprocedural.compute_and_store_post
|
|
|
|
Interprocedural.compute_and_store_post
|
|
|
|
~compute_post
|
|
|
|
~compute_post
|
|
|
|
~make_extras:FormalMap.make
|
|
|
|
~make_extras:FormalMap.make
|
|
|
|
callback_arg with
|
|
|
|
callback with
|
|
|
|
| Some post -> post
|
|
|
|
| Some post -> post
|
|
|
|
| None -> empty
|
|
|
|
| None -> empty
|
|
|
|
in
|
|
|
|
|
|
|
|
|
|
|
|
let checker callback =
|
|
|
|
|
|
|
|
ignore (analyze_procedure callback)
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
(* creates a map from proc_envs to postconditions *)
|
|
|
|
|
|
|
|
let make_results_table get_proc_desc file_env =
|
|
|
|
|
|
|
|
(* make a Map sending each element e of list l to (f e) *)
|
|
|
|
|
|
|
|
let map_post_computation_over_procs f l =
|
|
|
|
|
|
|
|
List.fold
|
|
|
|
|
|
|
|
~f:(fun m p -> ResultsTableType.add p (f p) m)
|
|
|
|
|
|
|
|
~init:ResultsTableType.empty
|
|
|
|
|
|
|
|
l in
|
|
|
|
|
|
|
|
let compute_post_for_procedure = (* takes proc_env as arg *)
|
|
|
|
|
|
|
|
fun (idenv, tenv, proc_name, proc_desc) ->
|
|
|
|
|
|
|
|
let callback_arg =
|
|
|
|
|
|
|
|
let get_procs_in_file _ = [] in
|
|
|
|
|
|
|
|
{ Callbacks.get_proc_desc; get_procs_in_file; idenv; tenv; proc_name; proc_desc } in
|
|
|
|
|
|
|
|
analyze_procedure callback_arg in
|
|
|
|
map_post_computation_over_procs compute_post_for_procedure file_env
|
|
|
|
map_post_computation_over_procs compute_post_for_procedure file_env
|
|
|
|
|
|
|
|
|
|
|
|
let get_current_class_and_threadsafe_superclasses tenv pname =
|
|
|
|
let get_current_class_and_threadsafe_superclasses tenv pname =
|
|
|
@ -1029,9 +1034,7 @@ let process_results_table file_env tab =
|
|
|
|
tab
|
|
|
|
tab
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
(*This is a "cluster checker" *)
|
|
|
|
(* Gathers results by analyzing all the methods in a file, then post-processes the results to check
|
|
|
|
(*Gathers results by analyzing all the methods in a file, then post-processes
|
|
|
|
an (approximation of) thread safety *)
|
|
|
|
the results to check (approximation of) thread safety *)
|
|
|
|
|
|
|
|
(* file_env: (Idenv.t * Tenv.t * Procname.t * Procdesc.t) list *)
|
|
|
|
|
|
|
|
let file_analysis _ _ get_procdesc file_env =
|
|
|
|
let file_analysis _ _ get_procdesc file_env =
|
|
|
|
process_results_table file_env (make_results_table get_procdesc file_env)
|
|
|
|
process_results_table file_env (make_results_table get_procdesc file_env)
|
|
|
|