Replace long structured string literals with 'quoted strings'

Reviewed By: jvillard

Differential Revision: D5384497

fbshipit-source-id: 2139ee7
master
Josh Berdine 7 years ago committed by Facebook Github Bot
parent 8e078c33d7
commit f07de2d9c9

@ -28,100 +28,58 @@ struct
let outc = Unix.out_channel_of_descr fd in
let fmt = F.formatter_of_out_channel outc in
let s =
"<!DOCTYPE HTML PUBLIC \"-//W3C//DTD HTML 4.01 Transitional//EN\">\n\
<html>\n\
<head>\n\
<title>" ^
{|<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
<html>
<head>
<title>|} ^
fname ^
"</title>\n\
<style type=\"text/css\">\n\
body { color:#000000; background-color:#ffffff }\n\
body { font-family:Helvetica, sans-serif; font-size:10pt }\n\
h1 { font-size:14pt }\n\
.code { border-collapse:collapse; width:100%; }\n\
.code { font-family: \"Andale Mono\", monospace; font-size:10pt }\n\
.code { line-height: 1.2em }\n\
.comment { color: green; font-style: oblique }\n\
.keyword { color: blue }\n\
.string_literal { color: red }\n\
.color_black { color: black }\n\
.color_blue { color: blue }\n\
.color_green { color: green }\n\
.color_red { color: red }\n\
.color_orange { color: orange }\n\
.directive { color: darkmagenta }\n\
.expansion { display: none; }\n\
.visited:hover .expansion {\
display: block;\
border: 2px\
solid #FF0000;\
padding: 2px;\
background-color:#FFF0F0;\
font-weight: normal;\
-webkit-border-radius:5px;\
-webkit-box-shadow:1px 1px 7px #000;\
position: absolute;\
top: -1em;\
left:10em;\
z-index: 1 }\n\
.visited {\
color: darkmagenta;\
background-color:LemonChiffon;\
position: relative }\n\
.visitedproof:hover .expansion {\
display: block;\
border: 2px solid #FF0000;\
padding: 2px;\
background-color:#FFF0F0;\
font-weight: normal;\
-webkit-border-radius:5px;\
-webkit-box-shadow:1px 1px 7px #000;\
position: absolute;\
top: -1em;\
left:10em;\
z-index: 1 }\n\
.visitedproof {\
color: darkmagenta;\
background-color:lightgreen;\
position: relative }\n\
.dangling:hover .expansion {\
display: block;\
border: 2px solid #FF0000;\
padding: 2px;\
background-color:#FFF0F0;\
font-weight: normal;\
-webkit-border-radius:5px;\
-webkit-box-shadow:1px 1px 7px #000;\
position: absolute;\
top: -1em;\
left:10em;\
z-index: 1 }\n\
.dangling { color: gray; background-color:white; position: relative }\n\
.num { width:2.5em; padding-right:2ex; background-color:#eeeeee }\n\
.num { text-align:right; font-size: smaller }\n\
.num { color:#444444 }\n\
.line { padding-left: 1ex; border-left: 3px solid #ccc }\n\
.line { white-space: pre }\n\
.msg { background-color:#fff8b4; color:#000000 }\n\
.msg { -webkit-box-shadow:1px 1px 7px #000 }\n\
.msg { -webkit-border-radius:5px }\n\
.msg { font-family:Helvetica, sans-serif; font-size: smaller }\n\
.msg { font-weight: bold }\n\
.msg { float:left }\n\
.msg { padding:0.5em 1ex 0.5em 1ex }\n\
.msg { margin-top:10px; margin-bottom:10px }\n\
.msg { max-width:60em; word-wrap: break-word; white-space: pre-wrap;}\n\
.mrange { background-color:#dfddf3 }\n\
.mrange { border-bottom:1px solid #6F9DBE }\n\
.PathIndex { font-weight: bold }\n\
table.simpletable { padding: 5px; font-size:12pt; margin:20px; border-collapse: collapse;\
border-spacing: 0px; }\n\
td.rowname { text-align:right; font-weight:bold; color:#444444; padding-right:2ex; }\n\
</style>\n\
</head>\
\n\
<body>\
\n" in
{|</title>
<style type="text/css">
body { color:#000000; background-color:#ffffff }
body { font-family:Helvetica, sans-serif; font-size:10pt }
h1 { font-size:14pt }
.code { border-collapse:collapse; width:100%; }
.code { font-family: "Andale Mono", monospace; font-size:10pt }
.code { line-height: 1.2em }
.comment { color: green; font-style: oblique }
.keyword { color: blue }
.string_literal { color: red }
.color_black { color: black }
.color_blue { color: blue }
.color_green { color: green }
.color_red { color: red }
.color_orange { color: orange }
.directive { color: darkmagenta }
.expansion { display: none; }
.visited:hover .expansion { display: block; border: 2px solid #FF0000; padding: 2px; background-color:#FFF0F0; font-weight: normal; -webkit-border-radius:5px; -webkit-box-shadow:1px 1px 7px #000; position: absolute; top: -1em; left:10em; z-index: 1 }
.visited { color: darkmagenta; background-color:LemonChiffon; position: relative }
.visitedproof:hover .expansion { display: block; border: 2px solid #FF0000; padding: 2px; background-color:#FFF0F0; font-weight: normal; -webkit-border-radius:5px; -webkit-box-shadow:1px 1px 7px #000; position: absolute; top: -1em; left:10em; z-index: 1 }
.visitedproof { color: darkmagenta; background-color:lightgreen; position: relative }
.dangling:hover .expansion { display: block; border: 2px solid #FF0000; padding: 2px; background-color:#FFF0F0; font-weight: normal; -webkit-border-radius:5px; -webkit-box-shadow:1px 1px 7px #000; position: absolute; top: -1em; left:10em; z-index: 1 }
.dangling { color: gray; background-color:white; position: relative }
.num { width:2.5em; padding-right:2ex; background-color:#eeeeee }
.num { text-align:right; font-size: smaller }
.num { color:#444444 }
.line { padding-left: 1ex; border-left: 3px solid #ccc }
.line { white-space: pre }
.msg { background-color:#fff8b4; color:#000000 }
.msg { -webkit-box-shadow:1px 1px 7px #000 }
.msg { -webkit-border-radius:5px }
.msg { font-family:Helvetica, sans-serif; font-size: smaller }
.msg { font-weight: bold }
.msg { float:left }
.msg { padding:0.5em 1ex 0.5em 1ex }
.msg { margin-top:10px; margin-bottom:10px }
.msg { max-width:60em; word-wrap: break-word; white-space: pre-wrap;}
.mrange { background-color:#dfddf3 }
.mrange { border-bottom:1px solid #6F9DBE }
.PathIndex { font-weight: bold }
table.simpletable { padding: 5px; font-size:12pt; margin:20px; border-collapse: collapse; border-spacing: 0px; }
td.rowname { text-align:right; font-weight:bold; color:#444444; padding-right:2ex; }
</style>
</head>
<body>
|} in
F.fprintf fmt "%s" s;
(fd, fmt)

@ -27,8 +27,8 @@ let frame_id_of_summary stacktree =
(Str.split (Str.regexp "(") stacktree.Stacktree_j.method_name) in
match stacktree.Stacktree_j.location with
| None ->
failwith "Attempted to take signature of a frame without location \
information. This is undefined."
failwith
"Attempted to take signature of a frame without location information. This is undefined."
| Some { line = Some line_num; file } ->
F.sprintf "%s(%s:%d)" short_name (Filename.basename file) line_num
| Some { file } ->

@ -605,17 +605,19 @@ let print_kind f kind =
| Lambda_pred (no, lev, array) ->
match array with
| false ->
F.fprintf f "style=dashed; color=blue \
@\n state%iL%i \
[label=\"INTERNAL STRUCTURE %i \", style=filled, color= lightblue]@\n"
!dotty_state_count !lambda_counter !lambda_counter ;
F.fprintf f
"%s @\n state%iL%i [label=\"INTERNAL STRUCTURE %i \", %s]@\n"
"style=dashed; color=blue"
!dotty_state_count !lambda_counter !lambda_counter
"style=filled, color= lightblue";
F.fprintf f "state%iL%i -> state%iL%i [color=\"lightblue \" arrowhead=none] @\n"
!dotty_state_count !lambda_counter no lev;
| true ->
F.fprintf f "style=dashed; color=blue \
@\n state%iL%i \
[label=\"INTERNAL STRUCTURE %i \", style=filled, color= lightblue]@\n"
!dotty_state_count !lambda_counter !lambda_counter ;
F.fprintf f
"%s @\n state%iL%i [label=\"INTERNAL STRUCTURE %i \", %s]@\n"
"style=dashed; color=blue"
!dotty_state_count !lambda_counter !lambda_counter
"style=filled, color= lightblue" ;
(* F.fprintf f "state%iL%i -> struct%iL%i:%s [color=\"lightblue \" arrowhead=none] @\n"
!dotty_state_count !lambda_counter no lev lab;*)
incr dotty_state_count
@ -720,14 +722,14 @@ let rec print_struct f pe e te l coo c =
F.fprintf f "subgraph structs_%iL%i {@\n" n lambda ;
if !print_full_prop then
F.fprintf f
" node [shape=record]; @\n struct%iL%i \
[label=\"{<%s%iL%i> STRUCT: %a } | %a\" ] fontcolor=%s@\n"
" node [%s]; @\n struct%iL%i [label=\"{<%s%iL%i> STRUCT: %a } | %a\" ] fontcolor=%s@\n"
"shape=record"
n lambda
e_no_special_char n lambda (Sil.pp_exp_printenv pe) e (struct_to_dotty_str pe coo) l c
else
F.fprintf f
" node [shape=record]; @\n struct%iL%i \
[label=\"{<%s%iL%i> OBJECT: %s } | %a\" ] fontcolor=%s@\n"
" node [%s]; @\n struct%iL%i [label=\"{<%s%iL%i> OBJECT: %s } | %a\" ] fontcolor=%s@\n"
"shape=record"
n lambda e_no_special_char n lambda print_type (struct_to_dotty_str pe coo) l c;
F.fprintf f "}@\n"
@ -736,8 +738,9 @@ and print_array f pe e1 e2 l coo c =
let lambda = coo.lambda in
let e_no_special_char = strip_special_chars (Exp.to_string e1) in
F.fprintf f "subgraph structs_%iL%i {@\n" n lambda ;
F.fprintf f " node [shape=record]; @\n struct%iL%i \
[label=\"{<%s%iL%i> ARRAY| SIZE: %a } | %a\" ] fontcolor=%s@\n"
F.fprintf f
" node [%s]; @\n struct%iL%i [label=\"{<%s%iL%i> ARRAY| SIZE: %a } | %a\" ] fontcolor=%s@\n"
"shape=record"
n lambda e_no_special_char n lambda (Sil.pp_exp_printenv pe) e2 (get_contents pe coo) l c;
F.fprintf f "}@\n"
@ -749,13 +752,13 @@ and print_sll f pe nesting k e1 coo =
begin
match k with
| Sil.Lseg_NE ->
F.fprintf f "subgraph cluster_%iL%i { \
style=filled; color=lightgrey; node [style=filled,color=white]; \
label=\"list NE\";" n' lambda (*pp_nesting nesting*)
F.fprintf f
"subgraph cluster_%iL%i { %s node [style=filled,color=white]; label=\"list NE\";"
n' lambda "style=filled; color=lightgrey;"
| Sil.Lseg_PE ->
F.fprintf f "subgraph cluster_%iL%i { \
style=filled; color=lightgrey; node [style=filled,color=white]; \
label=\"list PE\";" n' lambda (*pp_nesting nesting *)
F.fprintf f
"subgraph cluster_%iL%i { %s node [style=filled,color=white]; label=\"list PE\";"
n' lambda "style=filled; color=lightgrey;"
end;
F.fprintf f "state%iL%i [label=\"%a\"]@\n" n lambda (Sil.pp_exp_printenv pe) e1;
let n' = !dotty_state_count in
@ -776,13 +779,13 @@ and print_dll f pe nesting k e1 e4 coo =
begin
match k with
| Sil.Lseg_NE ->
F.fprintf f "subgraph cluster_%iL%i { \
style=filled; color=lightgrey; node [style=filled,color=white]; \
label=\"doubly-linked list NE\";" n' lambda (*pp_nesting nesting *)
F.fprintf f
"subgraph cluster_%iL%i { %s node [style=filled,color=white]; label=\"%s\";"
n' lambda "style=filled; color=lightgrey;" "doubly-linked list NE"
| Sil.Lseg_PE ->
F.fprintf f "subgraph cluster_%iL%i { \
style=filled; color=lightgrey; node [style=filled,color=white]; \
label=\"doubly-linked list PE\";" n' lambda (*pp_nesting nesting *)
F.fprintf f
"subgraph cluster_%iL%i { %s node [style=filled,color=white]; label=\"%s\";"
n' lambda "style=filled; color=lightgrey;" "doubly-linked list PE"
end;
F.fprintf f "state%iL%i [label=\"%a\"]@\n" n lambda (Sil.pp_exp_printenv pe) e1;
let n' = !dotty_state_count in
@ -859,8 +862,8 @@ and display_pure_info f pe prop =
done in
let pure = Prop.get_pure prop in
F.fprintf f "subgraph {@\n";
F.fprintf f " node [shape=box]; \
@\n state_pi_%i [label=\"STACK \\n\\n %a\" color=orange style=filled]@\n"
F.fprintf f
" node [shape=box]; @\n state_pi_%i [label=\"STACK \\n\\n %a\" color=orange style=filled]@\n"
!proposition_counter (Prop.pp_pi pe) pure;
if !invisible_arrows then print_invisible_objects ();
F.fprintf f "}@\n"

@ -62,31 +62,27 @@ let mk_command_doc ~see_also:see_also_commands ?and_also ?environment:environmen
let analyze =
mk_command_doc ~title:"Infer Analysis"
~short_description:"analyze the files captured by infer"
~synopsis:"$(b,infer) $(b,analyze) $(i,[options])\n\
$(b,infer) $(i,[options])"
~synopsis:
{|$(b,infer) $(b,analyze) $(i,[options])
$(b,infer) $(i,[options])|}
~description:[`P "Analyze the files captured in the project results directory and report."]
~see_also:CLOpt.[Report; Run]
let capture =
mk_command_doc ~title:"Infer Compilation Capture"
~short_description:"capture source files for later analysis"
~synopsis:"$(b,infer) $(b,capture) $(i,[options]) $(b,--) $(b,buck) $(i,...)\n\
$(b,infer) $(b,capture) $(b,--flavors) $(i,[options]) $(b,--) $(b,buck) $(i,...)\n\
$(b,infer) $(b,capture) $(b,--buck-compilation-database) $(i,[no-]deps) \
$(i,[options]) $(b,--) $(b,buck) $(i,...)\n\
$(b,infer) $(b,capture) $(i,[options]) $(b,--compilation-database) $(i,file)\n\
$(b,infer) $(b,capture) $(i,[options]) $(b,--compilation-database-escaped) \
$(i,file)\n\
$(b,infer) $(b,capture) $(i,[options]) $(b,--) $(b,gradle)/$(b,gradlew) \
$(i,...)\n\
$(b,infer) $(b,capture) $(i,[options]) $(b,--) $(b,javac) $(i,...)\n\
$(b,infer) $(b,capture) $(i,[options]) $(b,--) $(b,make)/$(b,clang)/$(b,gcc) \
$(i,...)\n\
$(b,infer) $(b,capture) $(i,[options]) $(b,--) $(b,mvn)/$(b,mvnw) \
$(i,...)\n\
$(b,infer) $(b,capture) $(i,[options]) $(b,--) $(b,ndk-build) $(i,...)\n\
$(b,infer) $(b,capture) $(i,[--no-xcpretty]) $(i,[options]) $(b,--) \
$(b,xcodebuild) $(i,...)"
~synopsis:
{|$(b,infer) $(b,capture) $(i,[options]) $(b,--) $(b,buck) $(i,...)
$(b,infer) $(b,capture) $(b,--flavors) $(i,[options]) $(b,--) $(b,buck) $(i,...)
$(b,infer) $(b,capture) $(b,--buck-compilation-database) $(i,[no-]deps) $(i,[options]) $(b,--) $(b,buck) $(i,...)
$(b,infer) $(b,capture) $(i,[options]) $(b,--compilation-database) $(i,file)
$(b,infer) $(b,capture) $(i,[options]) $(b,--compilation-database-escaped) $(i,file)
$(b,infer) $(b,capture) $(i,[options]) $(b,--) $(b,gradle)/$(b,gradlew) $(i,...)
$(b,infer) $(b,capture) $(i,[options]) $(b,--) $(b,javac) $(i,...)
$(b,infer) $(b,capture) $(i,[options]) $(b,--) $(b,make)/$(b,clang)/$(b,gcc) $(i,...)
$(b,infer) $(b,capture) $(i,[options]) $(b,--) $(b,mvn)/$(b,mvnw) $(i,...)
$(b,infer) $(b,capture) $(i,[options]) $(b,--) $(b,ndk-build) $(i,...)
$(b,infer) $(b,capture) $(i,[--no-xcpretty]) $(i,[options]) $(b,--) $(b,xcodebuild) $(i,...)|}
~description:[
`P "Capture the build command or compilation database specified on the command line: infer \
intercepts calls to the compiler to read source files, translate them into infer's \
@ -109,35 +105,36 @@ let compile =
generates, which defeats the later capture of compilation commands by infer. Thus, to \
capture a CMake project, one should configure the project from within the infer build \
environment, for instance:";
`Pre " \
mkdir build && cd build\n \
infer compile -- cmake ..\n \
infer capture -- make";
`Pre
{| mkdir build && cd build
infer compile -- cmake ..
infer capture -- make|};
`P "The same solution can be used for projects whose \"./configure\" script hardcodes the \
paths to the compilers, for instance:";
`Pre " \
infer compile -- ./configure\n \
infer capture -- make";
`Pre
{| infer compile -- ./configure
infer capture -- make|};
`P "Another solution for CMake projects is to use CMake's compilation databases, for \
instance:";
`Pre " \
mkdir build && cd build\n \
cmake -DCMAKE_EXPORT_COMPILE_COMMANDS=1 ..\n \
infer capture --compilation-database compile_commands.json";
`Pre
{| mkdir build && cd build
cmake -DCMAKE_EXPORT_COMPILE_COMMANDS=1 ..
infer capture --compilation-database compile_commands.json|};
]
~see_also:CLOpt.[Capture]
let infer = mk_command_doc ~title:"Infer Static Analyzer"
~short_description:"static analysis for Java and C/C++/Objective-C/Objective-C++"
~synopsis:"$(b,infer) $(b,analyze) $(i,[options])\n\
$(b,infer) $(b,capture) $(i,[options])\n\
$(b,infer) $(b,compile) $(i,[options])\n\
$(b,infer) $(b,report) $(i,[options])\n\
$(b,infer) $(b,reportdiff) $(i,[options])\n\
$(b,infer) $(b,run) $(i,[options])\n\
$(b,infer) $(b,--compilation-database[-escaped]) $(i,file) $(i,[options])\n\
$(b,infer) $(i,[options]) $(b,--) $(b,compile command)\n\
$(b,infer) $(i,[options])"
~synopsis:
{|$(b,infer) $(b,analyze) $(i,[options])
$(b,infer) $(b,capture) $(i,[options])
$(b,infer) $(b,compile) $(i,[options])
$(b,infer) $(b,report) $(i,[options])
$(b,infer) $(b,reportdiff) $(i,[options])
$(b,infer) $(b,run) $(i,[options])
$(b,infer) $(b,--compilation-database[-escaped]) $(i,file) $(i,[options])
$(b,infer) $(i,[options]) $(b,--) $(b,compile command)
$(b,infer) $(i,[options])|}
~description:[
`P "Infer is a static analyzer. Given a collection of source files written in Java or in \
languages of the C family, and a command to build them, infer produces a list of \
@ -209,10 +206,11 @@ let infer = mk_command_doc ~title:"Infer Static Analyzer"
parent, etc., stopping at the first $(b,%s) file found."
inferconfig_file inferconfig_file);
`P "Example:";
`Pre " {\
\n \"cxx\": false,\
\n \"infer-blacklist-files-containing\": [\"@generated\",\"@Generated\"]\
\n }";
`Pre
{| {
"cxx": false,
"infer-blacklist-files-containing": ["@generated","@Generated"]
}|};
]
~see_also:(List.filter ~f:(function | CLOpt.Clang -> false | _ -> true) CLOpt.all_commands)
~and_also:", $(b,inferTraceBugs)"
@ -252,13 +250,15 @@ let reportdiff =
let run =
mk_command_doc ~title:"Infer Analysis of a Project"
~short_description:"capture source files, analyze, and report"
~synopsis:"$(b,infer) $(b,run) $(i,[options])\n\
$(b,infer) $(i,[options]) $(b,--) $(i,compile command)"
~synopsis:
{|$(b,infer) $(b,run) $(i,[options])
$(b,infer) $(i,[options]) $(b,--) $(i,compile command)|}
~description:[
`P "Calling \"$(b,infer) $(b,run) $(i,[options])\" is equivalent to performing the following \
sequence of commands:";
`Pre "$(b,infer) $(b,capture) $(i,[options])\n\
$(b,infer) $(b,analyze) $(i,[options])";
`Pre
{|$(b,infer) $(b,capture) $(i,[options])
$(b,infer) $(b,analyze) $(i,[options])|};
]
~see_also:CLOpt.[Analyze; Capture; Report]

@ -412,17 +412,19 @@ let () =
let abs_struct =
CLOpt.mk_int ~deprecated:["absstruct"] ~long:"abs-struct" ~default:1
~meta:"int"
"Specify abstraction level for fields of structs:\n\
- 0 = no\n\
- 1 = forget some fields during matching (and so lseg abstraction)\n"
{|Specify abstraction level for fields of structs:
- 0 = no
- 1 = forget some fields during matching (and so lseg abstraction)
|}
and abs_val =
CLOpt.mk_int ~deprecated:["absval"] ~long:"abs-val" ~default:2
~meta:"int"
"Specify abstraction level for expressions:\n\
- 0 = no abstraction\n\
- 1 = evaluate all expressions abstractly\n\
- 2 = 1 + abstract constant integer values during join\n"
{|Specify abstraction level for expressions:
- 0 = no abstraction
- 1 = evaluate all expressions abstractly
- 2 = 1 + abstract constant integer values during join
|}
and allow_leak =
@ -488,15 +490,13 @@ and analyzer =
| Linters -> () in
CLOpt.mk_symbol_opt ~deprecated:["analyzer"] ~long:"analyzer" ~short:'a'
~in_help:CLOpt.[Analyze, manual_generic; Run, manual_generic]
"Specify which analyzer to run (only one at a time is supported):\n\
- $(b,infer): run the bi-abduction based checker, in particular to check for memory errors \
(activated by default)\n\
- $(b,checkers), $(b,eradicate): run the specified analysis\n\
- $(b,capture): similar to specifying the $(b,capture) subcommand (DEPRECATED)\n\
- $(b,compile): similar to specifying the $(b,compile) subcommand (DEPRECATED)\n\
- $(b,crashcontext): experimental (see $(b,--crashcontext))\n\
- $(b,linters): run linters based on the ast only (Objective-C and Objective-C++ only, \
activated by default)"
{|Specify which analyzer to run (only one at a time is supported):
- $(b,infer): run the bi-abduction based checker, in particular to check for memory errors (activated by default)
- $(b,checkers), $(b,eradicate): run the specified analysis
- $(b,capture): similar to specifying the $(b,capture) subcommand (DEPRECATED)
- $(b,compile): similar to specifying the $(b,compile) subcommand (DEPRECATED)
- $(b,crashcontext): experimental (see $(b,--crashcontext))
- $(b,linters): run linters based on the ast only (Objective-C and Objective-C++ only, activated by default)|}
~f:(function
| CaptureOnly | CompileOnly as x ->
let analyzer_str = List.find_map_exn string_to_analyzer
@ -621,17 +621,18 @@ and (annotation_reachability,
and annotation_reachability_custom_pairs =
CLOpt.mk_json ~long:"annotation-reachability-custom-pairs"
~in_help:CLOpt.[Analyze, manual_java]
"Specify custom sources/sink for the annotation reachability checker\n\
Example format: for custom annotations com.my.annotation.{Source1,Source2,Sink1}\n\
{ \"sources\" : [\"Source1\", \"Source2\"], \"sink\" : \"Sink1\" }"
{|Specify custom sources/sink for the annotation reachability checker
Example format: for custom annotations com.my.annotation.{Source1,Source2,Sink1}
{ "sources" : ["Source1", "Source2"], "sink" : "Sink1" }|}
and array_level =
CLOpt.mk_int ~deprecated:["arraylevel"] ~long:"array-level" ~default:0
~meta:"int" "Level of treating the array indexing and pointer arithmetic:\n\
- 0 = treats both features soundly\n\
- 1 = assumes that the size of every array is infinite\n\
- 2 = assumes that all heap dereferences via array indexing and pointer \
arithmetic are correct\n"
~meta:"int"
{|Level of treating the array indexing and pointer arithmetic:
- 0 = treats both features soundly
- 1 = assumes that the size of every array is infinite
- 2 = assumes that all heap dereferences via array indexing and pointer arithmetic are correct
|}
and ast_file =
CLOpt.mk_path_opt ~deprecated:["ast"] ~long:"ast-file"
~meta:"file" "AST file for the translation"
@ -902,11 +903,10 @@ and (
CLOpt.mk_int_opt ~long:"debug-level"
~in_help:all_generic_manuals ~meta:"level"
~f:(fun level -> set_debug_level level; level)
"Debug level (sets $(b,--bo-debug) $(i,level), $(b,--debug-level-analysis) $(i,level), \
$(b,--debug-level-capture) $(i,level), $(b,--debug-level-linters) $(i,level)):\
\n - 0: only basic debugging enabled\
\n - 1: verbose debugging enabled\
\n - 2: very verbose debugging enabled"
{|Debug level (sets $(b,--bo-debug) $(i,level), $(b,--debug-level-analysis) $(i,level), $(b,--debug-level-capture) $(i,level), $(b,--debug-level-linters) $(i,level)):
- 0: only basic debugging enabled
- 1: verbose debugging enabled
- 2: very verbose debugging enabled|}
and debug_exceptions =
CLOpt.mk_bool_group ~long:"debug-exceptions"
@ -1200,9 +1200,11 @@ and jobs =
and join_cond =
CLOpt.mk_int ~deprecated:["join_cond"] ~long:"join-cond" ~default:1
~meta:"int" "Set the strength of the final information-loss check used by the join:\n\
- 0 = use the most aggressive join for preconditions\n\
- 1 = use the least aggressive join for preconditions\n"
~meta:"int"
{|Set the strength of the final information-loss check used by the join:
- 0 = use the most aggressive join for preconditions
- 1 = use the least aggressive join for preconditions
|}
and latex =
CLOpt.mk_path_opt ~deprecated:["latex"] ~long:"latex"
@ -1263,11 +1265,12 @@ and ml_buckets =
CLOpt.mk_symbol_seq ~deprecated:["ml_buckets"; "-ml_buckets"] ~long:"ml-buckets"
~default:[`MLeak_cf]
~in_help:CLOpt.[Analyze, manual_clang]
"Specify the memory leak buckets to be checked in Objective-C/C++:\n\
- $(b,cf) checks leaks from Core Foundation (activated by default),\n\
- $(b,arc) from code compiled in ARC mode,\n\
- $(b,narc) from code not compiled in ARC mode,\n\
- $(b,cpp) from C++ code\n"
{|Specify the memory leak buckets to be checked in Objective-C/C++:
- $(b,cf) checks leaks from Core Foundation (activated by default),
- $(b,arc) from code compiled in ARC mode,
- $(b,narc) from code not compiled in ARC mode,
- $(b,cpp) from C++ code
|}
~symbols:ml_bucket_symbols ~eq:PVariant.(=)
and models_mode =
@ -1321,8 +1324,7 @@ and patterns_skip_translation =
and per_procedure_parallelism =
CLOpt.mk_bool ~long:"per-procedure-parallelism" ~default:true
"Perform analysis with per-procedure parallelism.\n\
Java is not supported."
"Perform analysis with per-procedure parallelism. Java is not supported."
and pmd_xml =
CLOpt.mk_bool ~long:"pmd-xml"
@ -1518,9 +1520,11 @@ and sourcepath =
and spec_abs_level =
CLOpt.mk_int ~deprecated:["spec_abs_level"] ~long:"spec-abs-level" ~default:1
~meta:"int" "Set the level of abstracting the postconditions of discovered specs:\n\
- 0 = nothing special\n\
- 1 = filter out redundant posts implied by other posts\n"
~meta:"int"
{|Set the level of abstracting the postconditions of discovered specs:
- 0 = nothing special
- 1 = filter out redundant posts implied by other posts
|}
and specs_library =
let specs_library =

@ -255,7 +255,7 @@ let pp_summary fmt (thumbs_up, threads, locks,
accesses, return_attributes) =
F.fprintf
fmt
"\nThumbsUp: %a, Threads: %a, Locks: %a \nAccesses %a \nReturn Attributes: %a\n"
"@\nThumbsUp: %a, Threads: %a, Locks: %a @\nAccesses %a @\nReturn Attributes: %a@\n"
ThumbsUpDomain.pp thumbs_up
ThreadsDomain.pp threads
LocksDomain.pp locks
@ -265,7 +265,7 @@ let pp_summary fmt (thumbs_up, threads, locks,
let pp fmt { thumbs_up; threads; locks; accesses; attribute_map; } =
F.fprintf
fmt
"\nThumbsUp: %a, Threads: %a, Locks: %a \nAccesses %a \nReturn Attributes: %a\n"
"@\nThumbsUp: %a, Threads: %a, Locks: %a @\nAccesses %a @\nReturn Attributes: %a@\n"
ThumbsUpDomain.pp thumbs_up
ThreadsDomain.pp threads
LocksDomain.pp locks

@ -70,7 +70,7 @@ let get_decl_opt decl_ptr_opt =
let get_stmt stmt_ptr =
let stmt = Int.Table.find ClangPointers.pointer_stmt_table stmt_ptr in
if Option.is_none stmt then L.internal_error "stmt with pointer %d not found\n" stmt_ptr;
if Option.is_none stmt then L.internal_error "stmt with pointer %d not found@\n" stmt_ptr;
stmt
let get_stmt_opt stmt_ptr_opt =
@ -110,7 +110,7 @@ let get_type type_ptr =
match type_ptr with
| Clang_ast_types.TypePtr.Ptr raw_ptr ->
let typ = Int.Table.find ClangPointers.pointer_type_table raw_ptr in
if Option.is_none typ then L.internal_error "type with pointer %d not found\n" raw_ptr;
if Option.is_none typ then L.internal_error "type with pointer %d not found@\n" raw_ptr;
typ
| _ ->
(* otherwise, function fails *)

@ -15,25 +15,25 @@ let infer_profile_name = "infer-capture"
let infer_profile = lazy
(* indented so that users may copy it into their projects if they want to *)
(Printf.sprintf "\
\n <profile>\
\n <id>%s</id>\
\n <build>\
\n <plugins>\
\n <plugin>\
\n <groupId>org.apache.maven.plugins</groupId>\
\n <artifactId>maven-compiler-plugin</artifactId>\
\n <configuration>\
\n <compilerId>javac</compilerId>\
\n <forceJavacCompilerUse>true</forceJavacCompilerUse>\
\n <fork>true</fork>\
\n <executable>%s</executable>\
\n </configuration>\
\n </plugin>\
\n </plugins>\
\n </build>\
\n </profile>\
" infer_profile_name (Config.bin_dir ^/ CommandDoc.infer_exe_name))
(Printf.sprintf {|
<profile>
<id>%s</id>
<build>
<plugins>
<plugin>
<groupId>org.apache.maven.plugins</groupId>
<artifactId>maven-compiler-plugin</artifactId>
<configuration>
<compilerId>javac</compilerId>
<forceJavacCompilerUse>true</forceJavacCompilerUse>
<fork>true</fork>
<executable>%s</executable>
</configuration>
</plugin>
</plugins>
</build>
</profile>|}
infer_profile_name (Config.bin_dir ^/ CommandDoc.infer_exe_name))
let pom_worklist = ref [CLOpt.init_work_dir]

Loading…
Cancel
Save