diff --git a/infer/man/man1/infer-debug.txt b/infer/man/man1/infer-debug.txt index 43c2deb0d..f0031ed4e 100644 --- a/infer/man/man1/infer-debug.txt +++ b/infer/man/man1/infer-debug.txt @@ -33,6 +33,9 @@ OPTIONS --help-full Show this manual with all internal options in the INTERNAL OPTIONS section + + --select N + Select option number N. If omitted, prompt for input. DEBUG GLOBAL TYPE ENVIRONMENT --global-tenv Activates: Print the global type environment. (Conversely: diff --git a/infer/man/man1/infer-explore.txt b/infer/man/man1/infer-explore.txt index bce669ddb..1d9865edf 100644 --- a/infer/man/man1/infer-explore.txt +++ b/infer/man/man1/infer-explore.txt @@ -37,7 +37,7 @@ EXPLORE BUGS shown. --select N - Select bug number N. If omitted, prompt for input. + Select option number N. If omitted, prompt for input. --no-source-preview Deactivates: print code excerpts around trace elements diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt index 0a08a3827..5387e1bd8 100644 --- a/infer/man/man1/infer-full.txt +++ b/infer/man/man1/infer-full.txt @@ -1044,7 +1044,8 @@ OPTIONS See also infer-analyze(1). --select N - Select bug number N. If omitted, prompt for input. See also infer-explore(1). + Select option number N. If omitted, prompt for input. + See also infer-debug(1) and infer-explore(1). --no-self-in-block Deactivates: checker self-in-block: An Objective-C-specific diff --git a/infer/man/man1/infer.txt b/infer/man/man1/infer.txt index 40c4da9ae..1db7a1fa6 100644 --- a/infer/man/man1/infer.txt +++ b/infer/man/man1/infer.txt @@ -1044,7 +1044,8 @@ OPTIONS See also infer-analyze(1). --select N - Select bug number N. If omitted, prompt for input. See also infer-explore(1). + Select option number N. If omitted, prompt for input. + See also infer-debug(1) and infer-explore(1). --no-self-in-block Deactivates: checker self-in-block: An Objective-C-specific diff --git a/infer/src/backend/Procedures.ml b/infer/src/backend/Procedures.ml index 7f2e7badc..523d10315 100644 --- a/infer/src/backend/Procedures.ml +++ b/infer/src/backend/Procedures.ml @@ -4,8 +4,10 @@ * This source code is licensed under the MIT license found in the * LICENSE file in the root directory of this source tree. *) + open! IStd module F = Format +module L = Logging let get_all ~filter () = let db = ResultsDatabase.get_database () in @@ -19,33 +21,37 @@ let get_all ~filter () = let select_proc_names_interactive ~filter = let proc_names = get_all ~filter () |> List.rev in - match proc_names with - | [] -> - print_endline "No procedures found" ; + let proc_names_len = List.length proc_names in + match (proc_names, Config.select) with + | [], _ -> + F.eprintf "No procedures found" ; None - | [proc_name] -> - Format.printf "Selected proc name: %a@\n" Procname.pp proc_name ; - Format.print_flush () ; + | _, Some n when n >= proc_names_len -> + L.die UserError "Cannot select result #%d out of only %d procedures" n proc_names_len + | [proc_name], _ -> + F.eprintf "Selected proc name: %a@." Procname.pp proc_name ; Some proc_names - | _ -> + | _, Some n -> + let proc_names_array = List.to_array proc_names in + Some [proc_names_array.(n)] + | _, None -> 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 () ; + F.eprintf "%d: %a@\n" i Procname.pp proc_name ) ; let rec ask_user_input () = - print_string "Select one number (type 'a' for selecting all, 'q' for quit): " ; - Out_channel.(flush stdout) ; + F.eprintf "Select one number (type 'a' for selecting all, 'q' for quit): " ; + Out_channel.flush stderr ; 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" ; + F.eprintf "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" ; + F.eprintf "Invalid input" ; ask_user_input () in ask_user_input () @@ -74,7 +80,7 @@ let pp_all ~filter ~proc_name:proc_name_cond ~attr_kind ~source_file:source_file let path = DotCfg.emit_proc_desc source_file cfg in F.fprintf fmt "'%s'" path in - Format.fprintf fmt "@[%s@,%a%a%a%a%a@]@\n" proc_uid + F.fprintf fmt "@[%s@,%a%a%a%a%a@]@\n" proc_uid (pp_if source_file_cond "source_file" SourceFile.pp) source_file (pp_if proc_name_cond "proc_name" Procname.pp) diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index c6d4595ce..a21f15207 100644 --- a/infer/src/base/Config.ml +++ b/infer/src/base/Config.ml @@ -2065,8 +2065,8 @@ and seconds_per_iteration = and select = CLOpt.mk_int_opt ~long:"select" ~meta:"N" - ~in_help:InferCommand.[(Explore, manual_explore_bugs)] - "Select bug number $(i,N). If omitted, prompt for input." + ~in_help:InferCommand.[(Debug, manual_generic); (Explore, manual_explore_bugs)] + "Select option number $(i,N). If omitted, prompt for input." and scuba_logging, cost_scuba_logging =