From 41de08924b0d7da6e5fa37b3f47f333c48e05a6b Mon Sep 17 00:00:00 2001 From: Cristiano Calcagno Date: Thu, 4 Feb 2016 11:53:20 -0800 Subject: [PATCH] Indentation of command-line agruments. Reviewed By: sblackshear Differential Revision: D2902022 fb-gh-sync-id: 5807e37 --- infer/src/backend/inferanalyze.ml | 237 +++++++++++++++++++++++----- infer/src/backend/inferprint.ml | 180 ++++++++++++++++----- infer/src/backend/utils.ml | 135 +++++++++++++--- infer/src/clang/cMain.ml | 37 +++-- infer/src/java/jMain.ml | 55 +++++-- infer/src/llvm/lMain.ml | 4 +- infer/src/scripts/checkCopyright.ml | 5 +- 7 files changed, 522 insertions(+), 131 deletions(-) diff --git a/infer/src/backend/inferanalyze.ml b/infer/src/backend/inferanalyze.ml index 14d51ef4a..6893dbc76 100644 --- a/infer/src/backend/inferanalyze.ml +++ b/infer/src/backend/inferanalyze.ml @@ -137,63 +137,214 @@ let arg_desc = let desc = base_arg_desc @ [ - "-err_file", Arg.Set_string err_file_cmdline, Some "file", "use file for the err channel"; - "-exclude", Arg.String exclude, Some "file", "exclude from analysis the files and directories specified in file"; - "-incremental_changed_only", Arg.Unit incremental_changed_only, None, "only analyze files captured since the last analysis"; - "-incremental", Arg.Unit incremental, None, "analyze files captured since the last analysis plus any dependencies"; - "-iterations", Arg.Set_int iterations_cmdline, Some "n", "set the max number of operations for each function, expressed as a multiple of symbolic operations (default n=1)"; - "-nonstop", Arg.Set Config.nonstop, None, "activate the nonstop mode: the analysis continues after finding errors. With this option the analysis can become less precise."; - "-out_file", Arg.Set_string out_file_cmdline, Some "file", "use file for the out channel"; - "-print_builtins", Arg.Unit SymExec.print_builtins, None, "print the builtin functions and exit"; - "-source_path", Arg.String source_path, Some "path", "specify the absolute path to the root of the source files. Used to interpret relative paths when using option -exclude."; + "-err_file", + Arg.Set_string err_file_cmdline, + Some "file", + "use file for the err channel" + ; + "-exclude", + Arg.String exclude, + Some "file", + "exclude from analysis the files and directories specified in file" + ; + "-incremental_changed_only", + Arg.Unit incremental_changed_only, + None, + "only analyze files captured since the last analysis" + ; + "-incremental", + Arg.Unit incremental, + None, + "analyze files captured since the last analysis plus any dependencies" + ; + "-iterations", + Arg.Set_int iterations_cmdline, + Some "n", + "set the max number of operations for each function, + expressed as a multiple of symbolic operations (default n=1)" + ; + "-nonstop", + Arg.Set Config.nonstop, + None, + "activate the nonstop mode: the analysis continues after finding errors. + With this option the analysis can become less precise." + ; + "-out_file", + Arg.Set_string out_file_cmdline, + Some "file", + "use file for the out channel" + ; + "-print_builtins", + Arg.Unit SymExec.print_builtins, + None, + "print the builtin functions and exit" + ; + "-source_path", + Arg.String source_path, + Some "path", + "specify the absolute path to the root of the source files. + Used to interpret relative paths when using option -exclude." + ; (* TODO: merge with the -project_root option *) - "-java", Arg.Unit (fun () -> Config.curr_language := Config.Java), None, "Set language to Java"; - "-version", Arg.Unit print_version, None, "print version information and exit"; - "-version_json", Arg.Unit print_version_json, None, "print version json formatted"; - "-objcm", Arg.Set Config.objc_memory_model_on, None, "Use ObjC memory model"; - "-no_progress_bar", Arg.Unit (fun () -> Config.show_progress_bar := false), None, "Do not show a progress bar"; - "-ml_buckets", Arg.Set_string ml_buckets_arg, Some "ml_buckets", - "memory leak buckets to be checked, separated by commas. The possible buckets are cf (Core Foundation), arc, narc (No arc), cpp, unknown_origin"; + "-java", + Arg.Unit (fun () -> Config.curr_language := Config.Java), + None, + "Set language to Java" + ; + "-version", + Arg.Unit print_version, + None, + "print version information and exit" + ; + "-version_json", + Arg.Unit print_version_json, + None, + "print version json formatted" + ; + "-objcm", + Arg.Set Config.objc_memory_model_on, + None, + "Use ObjC memory model" + ; + "-no_progress_bar", + Arg.Unit (fun () -> Config.show_progress_bar := false), + None, + "Do not show a progress bar" + ; + "-ml_buckets", + Arg.Set_string ml_buckets_arg, + Some "ml_buckets", + "memory leak buckets to be checked, separated by commas. + The possible buckets are cf (Core Foundation), arc, narc (No arc), cpp, unknown_origin" + ; ] in Arg.create_options_desc false "Analysis Options" desc in let reserved_arg = let desc = reserved_arg_desc @ [ - "-analysis_stops", Arg.Set Config.analysis_stops, None, "issue a warning when the analysis stops"; - "-angelic_execution", Arg.Set Config.angelic_execution, None, "activate angelic execution: the analysis ignores errors caused by unknown procedure calls."; - "-checkers", Arg.Set checkers, None, " run only the checkers instead of the full analysis"; - "-cluster", Arg.String (fun s -> cluster_cmdline := Some s), Some "fname", "specify a .cluster file to be analyzed"; - "-codequery", Arg.String (fun s -> CodeQuery.query := Some s), Some "query", " execute the code query"; - "-eradicate", Arg.Set Config.eradicate, None, " activate the eradicate checker for java annotations"; - "-file", Arg.String (fun s -> only_files_cmdline := s :: !only_files_cmdline), Some "fname", "specify one file to be analyzed (without path); the option can be repeated"; - "-intraprocedural", Arg.Set Config.intraprocedural, None, "perform an intraprocedural analysis only"; - "-makefile", Arg.Set_string makefile_cmdline, Some "file", "create a makefile to perform the analysis"; - "-max_cluster", Arg.Set_int Config.max_cluster_size, Some "n", "set the max number of procedures in each cluster (default n=2000)"; - "-only_nospecs", Arg.Set Config.only_nospecs, None, " only analyze procedures which were analyzed before but have no specs"; - "-only_skips", Arg.Set Config.only_skips, None, " only analyze procedures dependent on previous skips which now have a .specs file"; - "-seconds_per_iteration", Arg.Set_int seconds_per_iteration, Some "n", "set the number of seconds per iteration (default n=30)"; - "-simulate", Arg.Set simulate, None, " run a simulation of the analysis only"; - "-subtype_multirange", Arg.Set Config.subtype_multirange, None, "use the multirange subtyping domain"; - "-optimistic_cast", Arg.Set Config.optimistic_cast, None, "allow cast of undefined values"; - "-select_proc", Arg.String (fun s -> select_proc := Some s), Some "string", "only consider procedures whose name contains the given string"; - "-symops_per_iteration", Arg.Set_int symops_per_iteration, Some "n", "set the number of symbolic operations per iteration (default n="^(string_of_int !symops_per_iteration)^")"; - "-type_size", Arg.Set Config.type_size, None, "consider the size of types during analysis"; - "-tracing", Arg.Unit (fun () -> Config.report_runtime_exceptions := true), None, - "Report error traces for runtime exceptions (Only for Java)"; - "-allow_specs_cleanup", Arg.Unit (fun () -> allow_specs_cleanup := true), None, - "Allow to remove existing specs before running analysis when it's not incremental"; - "-print_buckets", Arg.Unit (fun() -> Config.show_buckets := true; Config.show_ml_buckets := true), None, + "-analysis_stops", + Arg.Set Config.analysis_stops, + None, + "issue a warning when the analysis stops" + ; + "-angelic_execution", + Arg.Set Config.angelic_execution, + None, + "activate angelic execution: + The analysis ignores errors caused by unknown procedure calls." + ; + "-checkers", + Arg.Set checkers, + None, + " run only the checkers instead of the full analysis" + ; + "-cluster", + Arg.String (fun s -> cluster_cmdline := Some s), + Some "fname", + "specify a .cluster file to be analyzed" + ; + "-codequery", + Arg.String (fun s -> CodeQuery.query := Some s), + Some "query", + " execute the code query" + ; + "-eradicate", + Arg.Set Config.eradicate, + None, + " activate the eradicate checker for java annotations" + ; + "-file", + Arg.String (fun s -> only_files_cmdline := s :: !only_files_cmdline), + Some "fname", + "specify one file to be analyzed (without path); the option can be repeated" + ; + "-intraprocedural", + Arg.Set Config.intraprocedural, + None, + "perform an intraprocedural analysis only" + ; + "-makefile", + Arg.Set_string makefile_cmdline, + Some "file", + "create a makefile to perform the analysis" + ; + "-max_cluster", + Arg.Set_int Config.max_cluster_size, + Some "n", + "set the max number of procedures in each cluster (default n=2000)" + ; + "-only_nospecs", + Arg.Set Config.only_nospecs, + None, + " only analyze procedures which were analyzed before but have no specs" + ; + "-only_skips", + Arg.Set Config.only_skips, + None, + " only analyze procedures dependent on previous skips which now have a .specs file" + ; + "-seconds_per_iteration", + Arg.Set_int seconds_per_iteration, + Some "n", + "set the number of seconds per iteration (default n=30)" + ; + "-simulate", + Arg.Set simulate, + None, + " run a simulation of the analysis only" + ; + "-subtype_multirange", + Arg.Set Config.subtype_multirange, + None, + "use the multirange subtyping domain" + ; + "-optimistic_cast", + Arg.Set Config.optimistic_cast, + None, + "allow cast of undefined values" + ; + "-select_proc", + Arg.String (fun s -> select_proc := Some s), + Some "string", + "only consider procedures whose name contains the given string" + ; + "-symops_per_iteration", + Arg.Set_int symops_per_iteration, + Some "n", + "set the number of symbolic operations per iteration (default n=" + ^ (string_of_int !symops_per_iteration) ^ ")" + ; + "-type_size", + Arg.Set Config.type_size, + None, + "consider the size of types during analysis" + ; + "-tracing", + Arg.Unit (fun () -> Config.report_runtime_exceptions := true), + None, + "Report error traces for runtime exceptions (Only for Java)" + ; + "-allow_specs_cleanup", + Arg.Unit (fun () -> allow_specs_cleanup := true), + None, + "Allow to remove existing specs before running analysis when it's not incremental" + ; + "-print_buckets", + Arg.Unit (fun() -> Config.show_buckets := true; Config.show_ml_buckets := true), + None, "Add buckets to issue descriptions, useful when developing infer" + ; ] in Arg.create_options_desc false "Reserved Options: Experimental features, use with caution!" desc in base_arg @ reserved_arg let usage = - (version_string ()) ^ - "\nUsage: InferAnalyze [options]\n" ^ - " Analyze the files captured in the project results directory, which can be specified with the -results_dir option." + (version_string ()) ^ " +Usage: InferAnalyze [options] + Analyze the files captured in the project results directory, + which can be specified with the -results_dir option." let print_usage_exit () = Arg.usage arg_desc usage; diff --git a/infer/src/backend/inferprint.ml b/infer/src/backend/inferprint.ml index 9f98a8c7b..06768a344 100644 --- a/infer/src/backend/inferprint.ml +++ b/infer/src/backend/inferprint.ml @@ -94,53 +94,153 @@ let arg_desc = let base_arg = let desc = [ - "-bugs", Arg.String (fun s -> bugs_csv := create_outfile s), Some "bugs.csv", "create file bugs.csv containing a list of bugs in CSV format"; - "-bugs_json", Arg.String (fun s -> bugs_json := create_outfile s), Some "bugs.json", "create file bugs.json containing a list of bugs in JSON format"; - "-bugs_txt", Arg.String (fun s -> bugs_txt := create_outfile s), Some "bugs.txt", "create file bugs.txt containing a list of bugs in text format"; - "-bugs_xml", Arg.String (fun s -> bugs_xml := create_outfile s), Some "bugs.xml", "create file bugs.xml containing a list of bugs in XML format"; - "-calls", Arg.String (fun s -> calls_csv := create_outfile s), Some "calls.csv", "write individual calls in csv format to file.csv"; - "-load_results", Arg.String (fun s -> load_analysis_results := Some s), Some "file.iar", "load analysis results from Infer Analysis Results file file.iar"; - "-procs", Arg.String (fun s -> procs_csv := create_outfile s), Some "procs.csv", "create file procs.csv containing statistics for each procedure in CSV format"; - "-procs_xml", Arg.String (fun s -> procs_xml := create_outfile s), Some "procs.xml", "create file procs.xml containing statistics for each procedure in XML format"; - "-results_dir", Arg.String (fun s -> results_dir_cmdline := true; Config.results_dir := s), Some "dir", "read all the .specs files in the results dir"; - "-lib", Arg.String (fun s -> Config.specs_library := filename_to_absolute s :: !Config.specs_library), Some "dir", "add dir to the list of directories to be searched for spec files"; - "-q", Arg.Set quiet, None, "quiet: do not print specs on standard output"; - "-save_results", Arg.String (fun s -> save_analysis_results := Some s), Some "file.iar", "save analysis results to Infer Analysis Results file file.iar"; - "-unit_test", Arg.Set unit_test, None, "print unit test code"; - "-xml", Arg.Set xml_specs, None, "export specs into XML files file1.xml ... filen.xml"; - "-test_filtering", Arg.Set test_filtering, None, - "list all the files Infer can report on (should be call at the root of the procject, where - .inferconfig lives)."; - "-analyzer", Arg.String (fun s -> analyzer := Some (Utils.analyzer_of_string s)), Some "analyzer", - "setup the analyzer for the path filtering"; - "-inferconfig_home", Arg.String (fun s -> Inferconfig.inferconfig_home := Some s), Some "dir", - "Path to the .inferconfig file"; - "-local_config", Arg.String (fun s -> Inferconfig.local_config := Some s), Some "Path", - "Path to local config file"; - "-with_infer_src_loc", Arg.Set reports_include_ml_loc, None, - "include the location (in the Infer source code) from where reports are generated"; + "-bugs", + Arg.String (fun s -> bugs_csv := create_outfile s), + Some "bugs.csv", + "create file bugs.csv containing a list of bugs in CSV format" + ; + "-bugs_json", + Arg.String (fun s -> bugs_json := create_outfile s), + Some "bugs.json", + "create file bugs.json containing a list of bugs in JSON format" + ; + "-bugs_txt", + Arg.String (fun s -> bugs_txt := create_outfile s), + Some "bugs.txt", + "create file bugs.txt containing a list of bugs in text format" + ; + "-bugs_xml", + Arg.String (fun s -> bugs_xml := create_outfile s), + Some "bugs.xml", + "create file bugs.xml containing a list of bugs in XML format" + ; + "-calls", + Arg.String (fun s -> calls_csv := create_outfile s), + Some "calls.csv", + "write individual calls in csv format to file.csv" + ; + "-load_results", + Arg.String (fun s -> load_analysis_results := Some s), + Some "file.iar", + "load analysis results from Infer Analysis Results file file.iar" + ; + "-procs", + Arg.String (fun s -> procs_csv := create_outfile s), + Some "procs.csv", + "create file procs.csv containing statistics for each procedure in CSV format" + ; + "-procs_xml", + Arg.String (fun s -> procs_xml := create_outfile s), + Some "procs.xml", + "create file procs.xml containing statistics for each procedure in XML format" + ; + "-results_dir", + Arg.String (fun s -> results_dir_cmdline := true; Config.results_dir := s), + Some "dir", + "read all the .specs files in the results dir" + ; + "-lib", + Arg.String (fun s -> + Config.specs_library := filename_to_absolute s :: !Config.specs_library), + Some "dir", + "add dir to the list of directories to be searched for spec files" + ; + "-q", + Arg.Set quiet, + None, + "quiet: do not print specs on standard output" + ; + "-save_results", + Arg.String (fun s -> save_analysis_results := Some s), + Some "file.iar", + "save analysis results to Infer Analysis Results file file.iar" + ; + "-unit_test", + Arg.Set unit_test, + None, + "print unit test code" + ; + "-xml", + Arg.Set xml_specs, + None, + "export specs into XML files file1.xml ... filen.xml" + ; + "-test_filtering", + Arg.Set test_filtering, + None, + "list all the files Infer can report on (should be call at the root of the procject, + where .inferconfig lives)." + ; + "-analyzer", + Arg.String (fun s -> analyzer := Some (Utils.analyzer_of_string s)), + Some "analyzer", + "setup the analyzer for the path filtering" + ; + "-inferconfig_home", + Arg.String (fun s -> Inferconfig.inferconfig_home := Some s), + Some "dir", + "Path to the .inferconfig file" + ; + "-local_config", + Arg.String (fun s -> Inferconfig.local_config := Some s), + Some "Path", + "Path to local config file" + ; + "-with_infer_src_loc", + Arg.Set reports_include_ml_loc, + None, + "include the location (in the Infer source code) from where reports are generated" + ; ] in Arg.create_options_desc false "Options" desc in let reserved_arg = let desc = [ - "-latex", Arg.String (fun s -> latex := create_outfile s), Some "file.tex", "print latex report to file.tex"; - "-print_types", Arg.Set Config.print_types, None, "print types in symbolic heaps"; - "-precondition_stats", Arg.Set precondition_stats, None, "print stats about preconditions to standard output"; - "-report", Arg.String (fun s -> report := create_outfile s), Some "report_file", "create file report_file containing a report of the analysis results"; - "-source_file_copy", Arg.String (fun s -> source_file_copy := Some (DB.abs_source_file_from_path s)), Some "source_file", "print the path of the copy of source_file in the results directory"; - "-svg", Arg.Set svg, None, "generate .dot and .svg"; - "-whole_seconds", Arg.Set whole_seconds, None, "print whole seconds only"; + "-latex", + Arg.String (fun s -> latex := create_outfile s), + Some "file.tex", + "print latex report to file.tex" + ; + "-print_types", + Arg.Set Config.print_types, + None, + "print types in symbolic heaps" + ; + "-precondition_stats", + Arg.Set precondition_stats, + None, + "print stats about preconditions to standard output" + ; + "-report", + Arg.String (fun s -> report := create_outfile s), + Some "report_file", + "create file report_file containing a report of the analysis results" + ; + "-source_file_copy", + Arg.String (fun s -> source_file_copy := Some (DB.abs_source_file_from_path s)), + Some "source_file", + "print the path of the copy of source_file in the results directory" + ; + "-svg", + Arg.Set svg, + None, + "generate .dot and .svg" + ; + "-whole_seconds", + Arg.Set whole_seconds, + None, + "print whole seconds only" + ; ] in Arg.create_options_desc false "Reserved Options" desc in base_arg @ reserved_arg let usage = - "Usage: InferPrint [options] name1.specs ... namen.specs\n" ^ - " Read, convert, and print .specs files.\n" ^ - " To process all the .specs in the current directory, pass . as only parameter.\n" ^ - " To process all the .specs in the results directory, use option -results_dir.\n" ^ - " Each spec is printed to standard output unless option -q is used." + "Usage: InferPrint [options] name1.specs ... namen.specs + Read, convert, and print .specs files. + To process all the .specs in the current directory, pass . as only parameter + To process all the .specs in the results directory, use option -results_dir + Each spec is printed to standard output unless option -q is used." let print_usage_exit err_s = L.err "Load Error: %s@.@." err_s; @@ -868,11 +968,11 @@ let process_summary filters linereader stats (top_proc_set: Procname.Set.t) (fna let dot_file = DB.filename_add_suffix base ".dot" in let svg_file = DB.filename_add_suffix base ".svg" in if not (DB.file_exists dot_file) - || DB.file_modified_time (DB.filename_from_string fname) > DB.file_modified_time dot_file + || DB.file_modified_time (DB.filename_from_string fname) > DB.file_modified_time dot_file then Dotty.pp_speclist_dotty_file base specs; if not (DB.file_exists svg_file) - || DB.file_modified_time dot_file > DB.file_modified_time svg_file + || DB.file_modified_time dot_file > DB.file_modified_time svg_file then ignore (Sys.command ("dot -Tsvg \"" ^ (DB.filename_to_string dot_file) ^ "\" >\"" ^ (DB.filename_to_string svg_file) ^"\"")) end; @@ -880,7 +980,7 @@ let process_summary filters linereader stats (top_proc_set: Procname.Set.t) (fna let xml_file = DB.filename_add_suffix base ".xml" in let specs = Specs.get_specs_from_payload summary in if not (DB.file_exists xml_file) - || DB.file_modified_time (DB.filename_from_string fname) > DB.file_modified_time xml_file + || DB.file_modified_time (DB.filename_from_string fname) > DB.file_modified_time xml_file then begin let xml_out = ref (create_outfile (DB.filename_to_string xml_file)) in diff --git a/infer/src/backend/utils.ml b/infer/src/backend/utils.ml index b6880af14..923c103e9 100644 --- a/infer/src/backend/utils.ml +++ b/infer/src/backend/utils.ml @@ -679,29 +679,118 @@ let base_arg_desc = let reserved_arg_desc = [ - "-absstruct", Arg.Set_int Config.abs_struct, Some "n", "abstraction level for fields of structs (default n = 1)"; - "-absval", Arg.Set_int Config.abs_val, Some "n", "abstraction level for expressions (default n = 2)"; - "-arraylevel", Arg.Set_int Config.array_level, Some "n", "the level of treating the array indexing and pointer arithmetic (default n = 0)"; - "-developer_mode", Arg.Set Config.developer_mode, None, "reserved"; - "-dotty", Arg.Set Config.write_dotty, None, "produce dotty files in the results directory"; - "-exit_node_bias", Arg.Unit (fun () -> Config.worklist_mode:= 1), None, "nodes nearest the exit node are analyzed first"; - "-html", Arg.Set Config.write_html, None, "produce hmtl output in the results directory"; - "-join_cond", Arg.Set_int Config.join_cond, Some "n", "set the strength of the final information-loss check used by the join (default n=1)"; - "-leak", Arg.Set Config.allowleak, None, "forget leaks during abstraction"; - "-monitor_prop_size", Arg.Set Config.monitor_prop_size, None, "monitor size of props"; - "-nelseg", Arg.Set Config.nelseg, None, "use only nonempty lsegs"; - "-noliveness", Arg.Clear Config.liveness, None, "turn the dead program variable elimination off"; - "-noprintdiff", Arg.Clear Config.print_using_diff, None, "turn off highlighting diff w.r.t. previous prop in printing"; - "-notest", Arg.Clear Config.test, None, "turn test mode off"; - "-only_footprint", Arg.Set Config.only_footprint, None, "skip the re-execution phase"; - "-print_types", Arg.Set Config.print_types, None, "print types in symbolic heaps"; - "-set_pp_margin", Arg.Int (fun i -> F.set_margin i), Some "n", "set right margin for the pretty printing functions"; - "-slice_fun", Arg.Set_string Config.slice_fun, None, "analyze only functions recursively called by function given as argument"; - "-spec_abs_level", Arg.Set_int Config.spec_abs_level, Some "n", "set the level of abstracting the postconditions of discovered specs (default n=1)"; - "-trace_error", Arg.Set Config.trace_error, None, "turn on tracing of error explanation"; - "-trace_join", Arg.Set Config.trace_join, None, "turn on tracing of join"; - "-trace_rearrange", Arg.Set Config.trace_rearrange, None, "turn on tracing of rearrangement"; - "-visits_bias", Arg.Unit (fun () -> Config.worklist_mode:= 2), None, "nodes visited fewer times are analyzed first"; + "-absstruct", + Arg.Set_int Config.abs_struct, + Some "n", + "abstraction level for fields of structs (default n = 1)" + ; + "-absval", + Arg.Set_int Config.abs_val, + Some "n", + "abstraction level for expressions (default n = 2)"; + "-arraylevel", + Arg.Set_int Config.array_level, + Some "n", + "the level of treating the array indexing and pointer arithmetic (default n = 0)" + ; + "-developer_mode", + Arg.Set Config.developer_mode, + None, + "reserved" + ; + "-dotty", + Arg.Set Config.write_dotty, + None, + "produce dotty files in the results directory"; + "-exit_node_bias", + Arg.Unit (fun () -> Config.worklist_mode:= 1), + None, + "nodes nearest the exit node are analyzed first"; + "-html", + Arg.Set Config.write_html, + None, + "produce hmtl output in the results directory" + ; + "-join_cond", + Arg.Set_int Config.join_cond, + Some "n", + "set the strength of the final information-loss check used by the join (default n=1)" + ; + "-leak", + Arg.Set Config.allowleak, + None, + "forget leaks during abstraction" + ; + "-monitor_prop_size", + Arg.Set Config.monitor_prop_size, + None, + "monitor size of props" + ; + "-nelseg", + Arg.Set Config.nelseg, + None, + "use only nonempty lsegs" + ; + "-noliveness", + Arg.Clear Config.liveness, + None, + "turn the dead program variable elimination off" + ; + "-noprintdiff", + Arg.Clear Config.print_using_diff, + None, + "turn off highlighting diff w.r.t. previous prop in printing" + ; + "-notest", + Arg.Clear Config.test, + None, + "turn test mode off" + ; + "-only_footprint", + Arg.Set Config.only_footprint, + None, + "skip the re-execution phase" + ; + "-print_types", + Arg.Set Config.print_types, + None, + "print types in symbolic heaps" + ; + "-set_pp_margin", + Arg.Int (fun i -> F.set_margin i), + Some "n", + "set right margin for the pretty printing functions" + ; + "-slice_fun", + Arg.Set_string Config.slice_fun, + None, + "analyze only functions recursively called by function given as argument" + ; + "-spec_abs_level", + Arg.Set_int Config.spec_abs_level, + Some "n", + "set the level of abstracting the postconditions of discovered specs (default n=1)" + ; + "-trace_error", + Arg.Set Config.trace_error, + None, + "turn on tracing of error explanation" + ; + "-trace_join", + Arg.Set Config.trace_join, + None, + "turn on tracing of join" + ; + "-trace_rearrange", + Arg.Set Config.trace_rearrange, + None, + "turn on tracing of rearrangement" + ; + "-visits_bias", + Arg.Unit (fun () -> Config.worklist_mode:= 2), + None, + "nodes visited fewer times are analyzed first" + ; ] diff --git a/infer/src/clang/cMain.ml b/infer/src/clang/cMain.ml index 1465c75c8..efc3d6dae 100644 --- a/infer/src/clang/cMain.ml +++ b/infer/src/clang/cMain.ml @@ -23,52 +23,65 @@ let arg_desc = "-c", Arg.String (fun cfile -> CFrontend_config.source_file := Some cfile), Some "cfile", - "C File to translate"; + "C File to translate" + ; "-x", Arg.String (fun lang -> CFrontend_config.lang_from_string lang), Some "cfile", - "Language (c, objective-c, c++, objc-++)"; + "Language (c, objective-c, c++, objc-++)" + ; "-ast", Arg.String (fun file -> CFrontend_config.ast_file := Some file), Some "file", - "AST file for the translation"; + "AST file for the translation" + ; "-dotty_cfg_libs", Arg.Unit (fun _ -> Config.dotty_cfg_libs := true), None, - "Prints the cfg of the code coming from the libraries"; + "Prints the cfg of the code coming from the libraries" + ; "-no_headers", Arg.Unit (fun _ -> CFrontend_config.no_translate_libs := true), None, - "Do not translate code in header files (default)"; + "Do not translate code in header files (default)" + ; "-headers", Arg.Unit (fun _ -> CFrontend_config.no_translate_libs := false), None, - "Translate code in header files"; + "Translate code in header files" + ; "-testing_mode", Arg.Unit (fun _ -> CFrontend_config.testing_mode := true), None, - "Mode for testing, where no libraries are translated, including enums defined in the libraries"; + "Mode for testing, where no libraries are translated, + including enums defined in the libraries" + ; "-debug", Arg.Unit (fun _ -> CFrontend_config.debug_mode := true), None, - "Enables debug mode"; + "Enables debug mode" + ; "-stats", Arg.Unit (fun _ -> CFrontend_config.stats_mode := true), None, - "Enables stats mode"; + "Enables stats mode" + ; "-project_root", Arg.String (fun s -> Config.project_root := Some (Utils.filename_to_absolute s)), Some "dir", - "Toot directory of the project"; + "Toot directory of the project" + ; "-fobjc-arc", Arg.Unit (fun s -> Config.arc_mode := true), None, - "Translate with Objective-C Automatic Reference Counting (ARC)"; + "Translate with Objective-C Automatic Reference Counting (ARC)" + ; "-models_mode", Arg.Unit (fun _ -> CFrontend_config.models_mode := true), None, - "Mode for computing the models"; + "Mode for computing the models" + ; ] in Utils.Arg.create_options_desc false "Parsing Options" desc diff --git a/infer/src/java/jMain.ml b/infer/src/java/jMain.ml index 2c25bfaac..3adf8e0f2 100644 --- a/infer/src/java/jMain.ml +++ b/infer/src/java/jMain.ml @@ -18,18 +18,51 @@ let arg_desc = let desc = (arg_desc_filter options_to_keep base_arg_desc) @ [ - "-classpath", Arg.String (fun classpath -> JConfig.classpath := Some classpath), None, "set the classpath"; - "-class_source_map", Arg.String (fun filename -> JConfig.class_source_map := Some filename), None, "path to class -> source map in JSON format"; - "-models", Arg.String (fun filename -> JClasspath.add_models filename), Some "paths", "set the path to the jar containing the models"; - "-debug", Arg.Unit (fun () -> JConfig.debug_mode := true), None, "write extra translation information"; - "-dependencies", Arg.Unit (fun _ -> JConfig.dependency_mode := true), None, "translate all the dependencies during the capture"; - "-no-static_final", Arg.Unit (fun () -> JTrans.no_static_final := true), None, "no special treatment for static final fields"; - "-tracing", Arg.Unit (fun () -> JConfig.translate_checks := true), None, - "Translate JVM checks"; - "-harness", Arg.Unit (fun () -> JConfig.create_harness := true), None, - "Create Android lifecycle harness"; - "-verbose_out", Arg.String (fun path -> JClasspath.set_verbose_out path), None, + "-classpath", + Arg.String (fun classpath -> JConfig.classpath := Some classpath), + None, + "set the classpath" + ; + "-class_source_map", + Arg.String (fun filename -> JConfig.class_source_map := Some filename), + None, + "path to class -> source map in JSON format" + ; + "-models", + Arg.String (fun filename -> JClasspath.add_models filename), + Some "paths", + "set the path to the jar containing the models" + ; + "-debug", + Arg.Unit (fun () -> JConfig.debug_mode := true), + None, + "write extra translation information" + ; + "-dependencies", + Arg.Unit (fun _ -> JConfig.dependency_mode := true), + None, + "translate all the dependencies during the capture" + ; + "-no-static_final", + Arg.Unit (fun () -> JTrans.no_static_final := true), + None, + "no special treatment for static final fields" + ; + "-tracing", + Arg.Unit (fun () -> JConfig.translate_checks := true), + None, + "Translate JVM checks" + ; + "-harness", + Arg.Unit (fun () -> JConfig.create_harness := true), + None, + "Create Android lifecycle harness" + ; + "-verbose_out", + Arg.String (fun path -> JClasspath.set_verbose_out path), + None, "Set the path to the javac verbose output" + ; ] in Arg.create_options_desc false "Parsing Options" desc diff --git a/infer/src/llvm/lMain.ml b/infer/src/llvm/lMain.ml index 2d0f34d84..fb092c54e 100644 --- a/infer/src/llvm/lMain.ml +++ b/infer/src/llvm/lMain.ml @@ -17,11 +17,13 @@ let arg_desc = "-c", Arg.String (fun cfile -> LConfig.source_filename := Some cfile), Some "cfile", - "C/C++ file being translated"; + "C/C++ file being translated" + ; "-debug", Arg.Unit (fun _ -> LConfig.debug_mode := true), None, "Enables debug mode" + ; ] in Arg.create_options_desc false "Parsing Options" desc diff --git a/infer/src/scripts/checkCopyright.ml b/infer/src/scripts/checkCopyright.ml index 009924195..ad4b39938 100644 --- a/infer/src/scripts/checkCopyright.ml +++ b/infer/src/scripts/checkCopyright.ml @@ -264,7 +264,10 @@ let check_copyright fname = match read_file fname with let speclist = [ - ("-i", Arg.Set update_files, "Update copyright notice in-place"); + "-i", + Arg.Set update_files, + "Update copyright notice in-place" + ; ] let usage_msg = "checkCopyright [-i] file1 ..."