pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Indentation of command-line agruments.

Browse Source 
Reviewed By: sblackshear

Differential Revision: D2902022

fb-gh-sync-id: 5807e37
master
Cristiano Calcagno 9 years ago committed by facebook-github-bot-1
parent dba7e7124f
commit 41de08924b
7 changed files with 522 additions and 131 deletions
Show Stats Download Patch File Download Diff File

237
infer/src/backend/inferanalyze.ml
Unescape View File

@ -137,63 +137,214 @@ let arg_desc =
let desc = let desc =
base_arg_desc @ base_arg_desc @
[ [
"-err_file", Arg.Set_string err_file_cmdline, Some "file", "use file for the err channel"; "-err_file",
"-exclude", Arg.String exclude, Some "file", "exclude from analysis the files and directories specified in file"; Arg.Set_string err_file_cmdline,
"-incremental_changed_only", Arg.Unit incremental_changed_only, None, "only analyze files captured since the last analysis"; Some "file",
"-incremental", Arg.Unit incremental, None, "analyze files captured since the last analysis plus any dependencies"; "use file for the err channel"
"-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."; "-exclude",
"-out_file", Arg.Set_string out_file_cmdline, Some "file", "use file for the out channel"; Arg.String exclude,
"-print_builtins", Arg.Unit SymExec.print_builtins, None, "print the builtin functions and exit"; Some "file",
"-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."; "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 *) (* TODO: merge with the -project_root option *)
"-java", Arg.Unit (fun () -> Config.curr_language := Config.Java), None, "Set language to Java"; "-java",
"-version", Arg.Unit print_version, None, "print version information and exit"; Arg.Unit (fun () -> Config.curr_language := Config.Java),
"-version_json", Arg.Unit print_version_json, None, "print version json formatted"; None,
"-objcm", Arg.Set Config.objc_memory_model_on, None, "Use ObjC memory model"; "Set language to Java"
"-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", "-version",
"memory leak buckets to be checked, separated by commas. The possible buckets are cf (Core Foundation), arc, narc (No arc), cpp, unknown_origin"; 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 ] in
Arg.create_options_desc false "Analysis Options" desc in Arg.create_options_desc false "Analysis Options" desc in
let reserved_arg = let reserved_arg =
let desc = let desc =
reserved_arg_desc @ reserved_arg_desc @
[ [
"-analysis_stops", Arg.Set Config.analysis_stops, None, "issue a warning when the analysis stops"; "-analysis_stops",
"-angelic_execution", Arg.Set Config.angelic_execution, None, "activate angelic execution: the analysis ignores errors caused by unknown procedure calls."; Arg.Set Config.analysis_stops,
"-checkers", Arg.Set checkers, None, " run only the checkers instead of the full analysis"; None,
"-cluster", Arg.String (fun s -> cluster_cmdline := Some s), Some "fname", "specify a .cluster file to be analyzed"; "issue a warning when the analysis stops"
"-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"; "-angelic_execution",
"-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"; Arg.Set Config.angelic_execution,
"-intraprocedural", Arg.Set Config.intraprocedural, None, "perform an intraprocedural analysis only"; None,
"-makefile", Arg.Set_string makefile_cmdline, Some "file", "create a makefile to perform the analysis"; "activate angelic execution:
"-max_cluster", Arg.Set_int Config.max_cluster_size, Some "n", "set the max number of procedures in each cluster (default n=2000)"; The analysis ignores errors caused by unknown procedure calls."
"-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"; "-checkers",
"-seconds_per_iteration", Arg.Set_int seconds_per_iteration, Some "n", "set the number of seconds per iteration (default n=30)"; Arg.Set checkers,
"-simulate", Arg.Set simulate, None, " run a simulation of the analysis only"; None,
"-subtype_multirange", Arg.Set Config.subtype_multirange, None, "use the multirange subtyping domain"; " run only the checkers instead of the full analysis"
"-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"; "-cluster",
"-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)^")"; Arg.String (fun s -> cluster_cmdline := Some s),
"-type_size", Arg.Set Config.type_size, None, "consider the size of types during analysis"; Some "fname",
"-tracing", Arg.Unit (fun () -> Config.report_runtime_exceptions := true), None, "specify a .cluster file to be analyzed"
"Report error traces for runtime exceptions (Only for Java)"; ;
"-allow_specs_cleanup", Arg.Unit (fun () -> allow_specs_cleanup := true), None, "-codequery",
"Allow to remove existing specs before running analysis when it's not incremental"; Arg.String (fun s -> CodeQuery.query := Some s),
"-print_buckets", Arg.Unit (fun() -> Config.show_buckets := true; Config.show_ml_buckets := true), None, 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" "Add buckets to issue descriptions, useful when developing infer"
;
] in ] in
Arg.create_options_desc false Arg.create_options_desc false
"Reserved Options: Experimental features, use with caution!" desc in "Reserved Options: Experimental features, use with caution!" desc in
base_arg @ reserved_arg base_arg @ reserved_arg
let usage = let usage =
(version_string ()) ^ (version_string ()) ^ "
"\nUsage: InferAnalyze [options]\n" ^ Usage: InferAnalyze [options]
" Analyze the files captured in the project results directory, which can be specified with the -results_dir option." Analyze the files captured in the project results directory,
which can be specified with the -results_dir option."
let print_usage_exit () = let print_usage_exit () =
Arg.usage arg_desc usage; Arg.usage arg_desc usage;

180
infer/src/backend/inferprint.ml
Unescape View File

@ -94,53 +94,153 @@ let arg_desc =
let base_arg = let base_arg =
let desc = 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",
"-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"; Arg.String (fun s -> bugs_csv := create_outfile s),
"-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"; Some "bugs.csv",
"-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"; "create file bugs.csv containing a list of bugs in CSV 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"; "-bugs_json",
"-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"; Arg.String (fun s -> bugs_json := create_outfile s),
"-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"; Some "bugs.json",
"-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"; "create file bugs.json containing a list of bugs in JSON format"
"-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"; "-bugs_txt",
"-save_results", Arg.String (fun s -> save_analysis_results := Some s), Some "file.iar", "save analysis results to Infer Analysis Results file file.iar"; Arg.String (fun s -> bugs_txt := create_outfile s),
"-unit_test", Arg.Set unit_test, None, "print unit test code"; Some "bugs.txt",
"-xml", Arg.Set xml_specs, None, "export specs into XML files file1.xml ... filen.xml"; "create file bugs.txt containing a list of bugs in text format"
"-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 "-bugs_xml",
.inferconfig lives)."; Arg.String (fun s -> bugs_xml := create_outfile s),
"-analyzer", Arg.String (fun s -> analyzer := Some (Utils.analyzer_of_string s)), Some "analyzer", Some "bugs.xml",
"setup the analyzer for the path filtering"; "create file bugs.xml containing a list of bugs in XML format"
"-inferconfig_home", Arg.String (fun s -> Inferconfig.inferconfig_home := Some s), Some "dir", ;
"Path to the .inferconfig file"; "-calls",
"-local_config", Arg.String (fun s -> Inferconfig.local_config := Some s), Some "Path", Arg.String (fun s -> calls_csv := create_outfile s),
"Path to local config file"; Some "calls.csv",
"-with_infer_src_loc", Arg.Set reports_include_ml_loc, None, "write individual calls in csv format to file.csv"
"include the location (in the Infer source code) from where reports are generated"; ;
"-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 ] in
Arg.create_options_desc false "Options" desc in Arg.create_options_desc false "Options" desc in
let reserved_arg = let reserved_arg =
let desc = let desc =
[ [
"-latex", Arg.String (fun s -> latex := create_outfile s), Some "file.tex", "print latex report to file.tex"; "-latex",
"-print_types", Arg.Set Config.print_types, None, "print types in symbolic heaps"; Arg.String (fun s -> latex := create_outfile s),
"-precondition_stats", Arg.Set precondition_stats, None, "print stats about preconditions to standard output"; Some "file.tex",
"-report", Arg.String (fun s -> report := create_outfile s), Some "report_file", "create file report_file containing a report of the analysis results"; "print latex report to file.tex"
"-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"; "-print_types",
"-whole_seconds", Arg.Set whole_seconds, None, "print whole seconds only"; 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 ] in
Arg.create_options_desc false "Reserved Options" desc in Arg.create_options_desc false "Reserved Options" desc in
base_arg @ reserved_arg base_arg @ reserved_arg
let usage = let usage =
"Usage: InferPrint [options] name1.specs ... namen.specs\n" ^ "Usage: InferPrint [options] name1.specs ... namen.specs
" Read, convert, and print .specs files.\n" ^ Read, convert, and print .specs files.
" To process all the .specs in the current directory, pass . as only parameter.\n" ^ 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.\n" ^ 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." Each spec is printed to standard output unless option -q is used."
let print_usage_exit err_s = let print_usage_exit err_s =
L.err "Load Error: %s@.@." 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 dot_file = DB.filename_add_suffix base ".dot" in
let svg_file = DB.filename_add_suffix base ".svg" in let svg_file = DB.filename_add_suffix base ".svg" in
if not (DB.file_exists dot_file) 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 then
Dotty.pp_speclist_dotty_file base specs; Dotty.pp_speclist_dotty_file base specs;
if not (DB.file_exists svg_file) 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 then
ignore (Sys.command ("dot -Tsvg \"" ^ (DB.filename_to_string dot_file) ^ "\" >\"" ^ (DB.filename_to_string svg_file) ^"\"")) ignore (Sys.command ("dot -Tsvg \"" ^ (DB.filename_to_string dot_file) ^ "\" >\"" ^ (DB.filename_to_string svg_file) ^"\""))
end; 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 xml_file = DB.filename_add_suffix base ".xml" in
let specs = Specs.get_specs_from_payload summary in let specs = Specs.get_specs_from_payload summary in
if not (DB.file_exists xml_file) 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 then
begin begin
let xml_out = ref (create_outfile (DB.filename_to_string xml_file)) in let xml_out = ref (create_outfile (DB.filename_to_string xml_file)) in

135
infer/src/backend/utils.ml
Unescape View File

@ -679,29 +679,118 @@ let base_arg_desc =
let reserved_arg_desc = let reserved_arg_desc =
[ [
"-absstruct", Arg.Set_int Config.abs_struct, Some "n", "abstraction level for fields of structs (default n = 1)"; "-absstruct",
"-absval", Arg.Set_int Config.abs_val, Some "n", "abstraction level for expressions (default n = 2)"; Arg.Set_int Config.abs_struct,
"-arraylevel", Arg.Set_int Config.array_level, Some "n", "the level of treating the array indexing and pointer arithmetic (default n = 0)"; Some "n",
"-developer_mode", Arg.Set Config.developer_mode, None, "reserved"; "abstraction level for fields of structs (default n = 1)"
"-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"; "-absval",
"-html", Arg.Set Config.write_html, None, "produce hmtl output in the results directory"; Arg.Set_int Config.abs_val,
"-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)"; Some "n",
"-leak", Arg.Set Config.allowleak, None, "forget leaks during abstraction"; "abstraction level for expressions (default n = 2)";
"-monitor_prop_size", Arg.Set Config.monitor_prop_size, None, "monitor size of props"; "-arraylevel",
"-nelseg", Arg.Set Config.nelseg, None, "use only nonempty lsegs"; Arg.Set_int Config.array_level,
"-noliveness", Arg.Clear Config.liveness, None, "turn the dead program variable elimination off"; Some "n",
"-noprintdiff", Arg.Clear Config.print_using_diff, None, "turn off highlighting diff w.r.t. previous prop in printing"; "the level of treating the array indexing and pointer arithmetic (default n = 0)"
"-notest", Arg.Clear Config.test, None, "turn test mode off"; ;
"-only_footprint", Arg.Set Config.only_footprint, None, "skip the re-execution phase"; "-developer_mode",
"-print_types", Arg.Set Config.print_types, None, "print types in symbolic heaps"; Arg.Set Config.developer_mode,
"-set_pp_margin", Arg.Int (fun i -> F.set_margin i), Some "n", "set right margin for the pretty printing functions"; None,
"-slice_fun", Arg.Set_string Config.slice_fun, None, "analyze only functions recursively called by function given as argument"; "reserved"
"-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"; "-dotty",
"-trace_join", Arg.Set Config.trace_join, None, "turn on tracing of join"; Arg.Set Config.write_dotty,
"-trace_rearrange", Arg.Set Config.trace_rearrange, None, "turn on tracing of rearrangement"; None,
"-visits_bias", Arg.Unit (fun () -> Config.worklist_mode:= 2), None, "nodes visited fewer times are analyzed first"; "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"
;
] ]

37
infer/src/clang/cMain.ml
Unescape View File

@ -23,52 +23,65 @@ let arg_desc =
"-c", "-c",
Arg.String (fun cfile -> CFrontend_config.source_file := Some cfile), Arg.String (fun cfile -> CFrontend_config.source_file := Some cfile),
Some "cfile", Some "cfile",
"C File to translate"; "C File to translate"
;
"-x", "-x",
Arg.String (fun lang -> CFrontend_config.lang_from_string lang), Arg.String (fun lang -> CFrontend_config.lang_from_string lang),
Some "cfile", Some "cfile",
"Language (c, objective-c, c++, objc-++)"; "Language (c, objective-c, c++, objc-++)"
;
"-ast", "-ast",
Arg.String (fun file -> CFrontend_config.ast_file := Some file), Arg.String (fun file -> CFrontend_config.ast_file := Some file),
Some "file", Some "file",
"AST file for the translation"; "AST file for the translation"
;
"-dotty_cfg_libs", "-dotty_cfg_libs",
Arg.Unit (fun _ -> Config.dotty_cfg_libs := true), Arg.Unit (fun _ -> Config.dotty_cfg_libs := true),
None, None,
"Prints the cfg of the code coming from the libraries"; "Prints the cfg of the code coming from the libraries"
;
"-no_headers", "-no_headers",
Arg.Unit (fun _ -> CFrontend_config.no_translate_libs := true), Arg.Unit (fun _ -> CFrontend_config.no_translate_libs := true),
None, None,
"Do not translate code in header files (default)"; "Do not translate code in header files (default)"
;
"-headers", "-headers",
Arg.Unit (fun _ -> CFrontend_config.no_translate_libs := false), Arg.Unit (fun _ -> CFrontend_config.no_translate_libs := false),
None, None,
"Translate code in header files"; "Translate code in header files"
;
"-testing_mode", "-testing_mode",
Arg.Unit (fun _ -> CFrontend_config.testing_mode := true), Arg.Unit (fun _ -> CFrontend_config.testing_mode := true),
None, 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", "-debug",
Arg.Unit (fun _ -> CFrontend_config.debug_mode := true), Arg.Unit (fun _ -> CFrontend_config.debug_mode := true),
None, None,
"Enables debug mode"; "Enables debug mode"
;
"-stats", "-stats",
Arg.Unit (fun _ -> CFrontend_config.stats_mode := true), Arg.Unit (fun _ -> CFrontend_config.stats_mode := true),
None, None,
"Enables stats mode"; "Enables stats mode"
;
"-project_root", "-project_root",
Arg.String (fun s -> Arg.String (fun s ->
Config.project_root := Some (Utils.filename_to_absolute s)), Config.project_root := Some (Utils.filename_to_absolute s)),
Some "dir", Some "dir",
"Toot directory of the project"; "Toot directory of the project"
;
"-fobjc-arc", "-fobjc-arc",
Arg.Unit (fun s -> Config.arc_mode := true), Arg.Unit (fun s -> Config.arc_mode := true),
None, None,
"Translate with Objective-C Automatic Reference Counting (ARC)"; "Translate with Objective-C Automatic Reference Counting (ARC)"
;
"-models_mode", "-models_mode",
Arg.Unit (fun _ -> CFrontend_config.models_mode := true), Arg.Unit (fun _ -> CFrontend_config.models_mode := true),
None, None,
"Mode for computing the models"; "Mode for computing the models"
;
] in ] in
Utils.Arg.create_options_desc false "Parsing Options" desc Utils.Arg.create_options_desc false "Parsing Options" desc

55
infer/src/java/jMain.ml
Unescape View File

@ -18,18 +18,51 @@ let arg_desc =
let desc = let desc =
(arg_desc_filter options_to_keep base_arg_desc) @ (arg_desc_filter options_to_keep base_arg_desc) @
[ [
"-classpath", Arg.String (fun classpath -> JConfig.classpath := Some classpath), None, "set the classpath"; "-classpath",
"-class_source_map", Arg.String (fun filename -> JConfig.class_source_map := Some filename), None, "path to class -> source map in JSON format"; Arg.String (fun classpath -> JConfig.classpath := Some classpath),
"-models", Arg.String (fun filename -> JClasspath.add_models filename), Some "paths", "set the path to the jar containing the models"; None,
"-debug", Arg.Unit (fun () -> JConfig.debug_mode := true), None, "write extra translation information"; "set the classpath"
"-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"; "-class_source_map",
"-tracing", Arg.Unit (fun () -> JConfig.translate_checks := true), None, Arg.String (fun filename -> JConfig.class_source_map := Some filename),
"Translate JVM checks"; None,
"-harness", Arg.Unit (fun () -> JConfig.create_harness := true), None, "path to class -> source map in JSON format"
"Create Android lifecycle harness"; ;
"-verbose_out", Arg.String (fun path -> JClasspath.set_verbose_out path), None, "-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" "Set the path to the javac verbose output"
;
] in ] in
Arg.create_options_desc false "Parsing Options" desc Arg.create_options_desc false "Parsing Options" desc

4
infer/src/llvm/lMain.ml
Unescape View File

@ -17,11 +17,13 @@ let arg_desc =
"-c", "-c",
Arg.String (fun cfile -> LConfig.source_filename := Some cfile), Arg.String (fun cfile -> LConfig.source_filename := Some cfile),
Some "cfile", Some "cfile",
"C/C++ file being translated"; "C/C++ file being translated"
;
"-debug", "-debug",
Arg.Unit (fun _ -> LConfig.debug_mode := true), Arg.Unit (fun _ -> LConfig.debug_mode := true),
None, None,
"Enables debug mode" "Enables debug mode"
;
] in ] in
Arg.create_options_desc false "Parsing Options" desc Arg.create_options_desc false "Parsing Options" desc

5
infer/src/scripts/checkCopyright.ml
Unescape View File

@ -264,7 +264,10 @@ let check_copyright fname = match read_file fname with
let speclist = [ 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 ..." let usage_msg = "checkCopyright [-i] file1 ..."

Write Preview
Loading…
Cancel
Save