diff --git a/infer/man/man1/infer-explore.txt b/infer/man/man1/infer-explore.txt index b10892640..2297b3984 100644 --- a/infer/man/man1/infer-explore.txt +++ b/infer/man/man1/infer-explore.txt @@ -85,6 +85,10 @@ EXPLORE PROCEDURES Deactivates: Include the source file in which the procedure definition or declaration was found in the output of --procedures (Conversely: --procedures-source-file) + + --procedures-summary + Activates: Print the summaries of each procedure in the output of + --procedures (Conversely: --no-procedures-summary) EXPLORE SOURCE FILES --source-files Activates: Print source files discovered by infer (Conversely: diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt index de83a1f25..f1b2e02bc 100644 --- a/infer/man/man1/infer-full.txt +++ b/infer/man/man1/infer-full.txt @@ -875,6 +875,10 @@ OPTIONS definition or declaration was found in the output of --procedures (Conversely: --procedures-source-file) See also infer-explore(1). + --procedures-summary + Activates: Print the summaries of each procedure in the output of + --procedures (Conversely: --no-procedures-summary) See also infer-explore(1). + --no-progress-bar,-P Deactivates: Show a progress bar (Conversely: --progress-bar | -p) See also infer-run(1). diff --git a/infer/man/man1/infer.txt b/infer/man/man1/infer.txt index 76848c533..72f290387 100644 --- a/infer/man/man1/infer.txt +++ b/infer/man/man1/infer.txt @@ -875,6 +875,10 @@ OPTIONS definition or declaration was found in the output of --procedures (Conversely: --procedures-source-file) See also infer-explore(1). + --procedures-summary + Activates: Print the summaries of each procedure in the output of + --procedures (Conversely: --no-procedures-summary) See also infer-explore(1). + --no-progress-bar,-P Deactivates: Show a progress bar (Conversely: --progress-bar | -p) See also infer-run(1). diff --git a/infer/src/backend/Procedures.ml b/infer/src/backend/Procedures.ml index 900b87fd9..533ccca71 100644 --- a/infer/src/backend/Procedures.ml +++ b/infer/src/backend/Procedures.ml @@ -17,6 +17,39 @@ let get_all ~filter () = if filter source_file proc_name then proc_name :: rev_results else rev_results ) +let select_proc_names_interactive ~filter = + let proc_names = get_all ~filter () |> List.rev in + match proc_names with + | [] -> + print_endline "No procedures found" ; + None + | [proc_name] -> + Format.printf "Selected proc name: %a@\n" Procname.pp proc_name ; + Format.print_flush () ; + Some proc_names + | _ -> + let proc_names_array = List.to_array proc_names in + Array.iteri proc_names_array ~f:(fun i proc_name -> + Format.printf "%d: %a@\n" i Procname.pp proc_name ) ; + Format.print_flush () ; + let rec ask_user_input () = + print_string "Select one number (type 'a' for selecting all, 'q' for quit): " ; + Out_channel.(flush stdout) ; + let input = String.strip In_channel.(input_line_exn stdin) in + if String.equal (String.lowercase input) "a" then Some proc_names + else if String.equal (String.lowercase input) "q" then ( + print_endline "Quit interactive mode" ; + None ) + else + match int_of_string_opt input with + | Some n when 0 <= n && n < Array.length proc_names_array -> + Some [proc_names_array.(n)] + | _ -> + print_endline "Invalid input" ; ask_user_input () + in + ask_user_input () + + let pp_all ~filter ~proc_name:proc_name_cond ~attr_kind ~source_file:source_file_cond ~proc_attributes fmt () = let db = ResultsDatabase.get_database () in diff --git a/infer/src/backend/Procedures.mli b/infer/src/backend/Procedures.mli index ab0869121..e0c8c47fa 100644 --- a/infer/src/backend/Procedures.mli +++ b/infer/src/backend/Procedures.mli @@ -18,3 +18,5 @@ val pp_all : -> Format.formatter -> unit -> unit + +val select_proc_names_interactive : filter:Filtering.procedures_filter -> Procname.t list option diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index 41143d03b..43f6ca4aa 100644 --- a/infer/src/base/Config.ml +++ b/infer/src/base/Config.ml @@ -1941,6 +1941,12 @@ and procedures_source_file = output of $(b,--procedures)" +and procedures_summary = + CLOpt.mk_bool ~long:"procedures-summary" ~default:false + ~in_help:InferCommand.[(Explore, manual_explore_procedures)] + "Print the summaries of each procedure in the output of $(b,--procedures)" + + and process_clang_ast = CLOpt.mk_bool ~long:"process-clang-ast" ~default:false "process the ast to emit some info about the file (Not available for Java)" @@ -3087,6 +3093,8 @@ and[@warning "-32"] procedures_per_process = !procedures_per_process and procedures_source_file = !procedures_source_file +and procedures_summary = !procedures_summary + and process_clang_ast = !process_clang_ast and progress_bar = diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index 17e31a83e..60d1002af 100644 --- a/infer/src/base/Config.mli +++ b/infer/src/base/Config.mli @@ -547,6 +547,8 @@ val procedures_name : bool val procedures_source_file : bool +val procedures_summary : bool + val process_clang_ast : bool val clang_frontend_action_string : string diff --git a/infer/src/infer.ml b/infer/src/infer.ml index b667544ff..ec66a8f6f 100644 --- a/infer/src/infer.ml +++ b/infer/src/infer.ml @@ -180,13 +180,24 @@ let () = | Explore -> ( match (Config.procedures, Config.source_files) with | true, false -> - L.result "%a" - Config.( - Procedures.pp_all - ~filter:(Lazy.force Filtering.procedures_filter) - ~proc_name:procedures_name ~attr_kind:procedures_definedness - ~source_file:procedures_source_file ~proc_attributes:procedures_attributes) - () + let filter = Lazy.force Filtering.procedures_filter in + if Config.procedures_summary then + let pp_summary fmt proc_name = + match Summary.OnDisk.get proc_name with + | None -> + Format.fprintf fmt "No summary found: %a@\n" Procname.pp proc_name + | Some summary -> + Summary.pp_text fmt summary + in + Option.iter (Procedures.select_proc_names_interactive ~filter) ~f:(fun proc_names -> + L.result "%a" (fun fmt () -> List.iter proc_names ~f:(pp_summary fmt)) () ) + else + L.result "%a" + Config.( + Procedures.pp_all ~filter ~proc_name:procedures_name + ~attr_kind:procedures_definedness ~source_file:procedures_source_file + ~proc_attributes:procedures_attributes) + () | false, true -> let filter = Lazy.force Filtering.source_files_filter in L.result "%a"