@ -261,8 +261,8 @@ let deref_str_nil_argument_in_variadic_method pn total_args arg_number =
in
letproblem_str=
Printf.sprintf
"could be %s which results in a call to %s with %d arguments instead of %d (%s indicates that the last argument of this variadic %s has been reached)"
nil_null
"could be %s which results in a call to %s with %d arguments instead of %d (%s indicates \
that thelastargumentofthisvariadic%shasbeenreached)"nil_null
(Typ.Procname.to_simplified_stringpn)
arg_number(total_args-1)nil_nullfunction_method
in
@ -389,9 +389,11 @@ let desc_unsafe_guarded_by_access accessed_fld guarded_by_str loc =
in
letmsg=
Format.asprintf
"The field %a is annotated with %a, but the lock %a is not held during the access to the field %s. Since the current method is non-private, it can be called from outside the current class without synchronization. Consider wrapping the access in a %s block or making the method private."
"Trying to report error on procedure %a, but cannot because no summary exists for this procedure. Did you mean to log the error on the caller of %a instead?"
Typ.Procname.ppproc_nameTyp.Procname.ppproc_name
"Trying to report error on procedure %a, but cannot because no summary exists for this \
"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 intermediate representation, and store the result of the translation in the results directory."
]
"Capture the build command or compilation database specified on the command line: infer \
"Intercepts compilation commands similarly to $(b,infer-capture), but simply execute these compilation commands and do not perform any translation of the source files. This can be useful to configure build systems or for debugging purposes."
]
"Intercepts compilation commands similarly to $(b,infer-capture), but simply execute \
"$(b,cmake)(1) hardcodes the absolute paths to the compiler inside the Makefiles it 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:"
"$(b,cmake)(1) hardcodes the absolute paths to the compiler inside the Makefiles it \
"Show the list of bugs on the console and explore symbolic program traces emitted by infer to explain a report. Can also generate an HTML report from a JSON report."
]
"Show the list of bugs on the console and explore symbolic program traces emitted by \
"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 potential issues."
"Infer is a static analyzer. Given a collection of source files written in Java or in \
"When run without a subcommand, and if a compilation command is specified via the $(b,--) option or one of the $(b,--clang-compilation-database[-escaped]) options, then $(b,infer) behaves as $(b,infer-run)(1). Otherwise, $(b,infer) behaves as $(b,infer-analyze)(1)."
]
"When run without a subcommand, and if a compilation command is specified via the \
[`P"Every infer command accepts the arguments from all the other infer commands."
;`P
(Printf.sprintf
"Options are read from the $(b,%s) file, then from the $(b,%s) environment variable, then from the command line. Options in $(b,%s) take precedence over options in $(b,%s), and options passed on the command line take precedence over options in $(b,%s). See the $(i,%s) and $(i,%s) sections of this manual for more information."
"Options can be specified inside an argument file $(i,file) by passing $(b,@)$(i,file) as argument. The format is one option per line, and enclosing single ' and double \" quotes are ignored."
"Options can be specified inside an argument file $(i,file) by passing \
"Options without a default value (e.g., $(b,--linter)) and options with list-like values (e.g., $(b,--Xbuck)) all have a corresponding $(b,--option-reset) flag that resets their values to nothing or the empty list, respectively. For instance, $(b,--Xbuck-reset) will cancel any previous $(b,--Xbuck) option passed to infer."
"Options without a default value (e.g., $(b,--linter)) and options with list-like \
"See the manuals of individual infer commands for details about their supported options. The following is a list of all the supported options (see also $(b,--help-full) for options reserved for internal use)."
])
"See the manuals of individual infer commands for details about their supported \
"Extra arguments may be passed to all infer commands using the $(b,%s) environment variable (see the $(i,%s) section). $(b,%s) is expected to contain a string of %c-separated options. For instance, calling `%s=--debug^--print-logs infer` is equivalent to calling `infer --debug --print-logs`."
"If $(b,%s) is set to \"1\", then infer commands will exit with an error code in some cases when otherwise a simple warning would be emitted on stderr, for instance if a deprecated form of an option is used."
CLOpt.strict_mode_env_var)]
"If $(b,%s) is set to \"1\", then infer commands will exit with an error code in \
"$(b,%s) can be used to store infer options. Its format is that of a JSON record, where fields are infer long-form options, without their leading \"--\", and values depend on the type of the option:"
inferconfig_file)
"$(b,%s) can be used to store infer options. Its format is that of a JSON record, \
wherefieldsareinferlong-formoptions,withouttheirleading\"--\", and values \
dependonthetypeoftheoption:" inferconfig_file)
;`Noblank
;`P"- for switches options, the value is a JSON boolean (true or false, without quotes)"
;`Noblank
@ -189,14 +216,14 @@ $(b,infer) $(i,[options])|}
;`Noblank
;`P
(Printf.sprintf
"- path options have string values, and are interpreted relative to the location of the %s file"
inferconfig_file)
"- path options have string values, and are interpreted relative to the location of \
the %sfile"inferconfig_file)
;`Noblank
;`P"- cumulative options are JSON arrays of the appropriate type"
;`P
(Printf.sprintf
"Infer will look for an $(b,%s) file in the current directory, then its parent, etc., stopping at the first $(b,%s) file found."
inferconfig_file inferconfig_file)
"Infer will look for an $(b,%s) file in the current directory, then its parent, \
"Given two infer reports $(i,previous) and $(i,current), compute the following three reports and store them inside the \"differential/\" subdirectory of the results directory:"
"Given two infer reports $(i,previous) and $(i,current), compute the following three \
reportsandstoretheminsidethe\"differential/\" subdirectory of the results \
directory:"
;`Noblank
;`P
"- $(b,introduced.json) contains the issues found in $(i,current) but not $(i,previous);"
@ -233,7 +264,8 @@ let reportdiff =
;`P"- $(b,fixed.json) contains the issues found in $(i,previous) but not $(i,current);"
;`Noblank
;`P
"- $(b,preexisting.json) contains the issues found in both $(i,previous) and $(i,current)."
"- $(b,preexisting.json) contains the issues found in both $(i,previous) and \
$(i,current)."
;`P"All three files follow the same format as normal infer reports."]
~see_also:InferCommand.([Report])
@ -244,8 +276,8 @@ let events =
~synopsis:{|$(b,infer)$(b,events)|}
~description:
[`P
"Emit to stdout one JSON object per line, each describing a logged event happened during the execution of Infer"
]
"Emit to stdout one JSON object per line, each describing a logged event happened \
"the annotation reachability checker. Given a pair of source and sink annotation, e.g. @PerformanceCritical and @Expensive, this checker will warn whenever some method annotated with @PerformanceCritical calls, directly or indirectly, another method annotated with @Expensive"
"the annotation reachability checker. Given a pair of source and sink annotation, e.g. \
"the separation logic based bi-abduction analysis using the checkers framework"
@ -716,7 +720,8 @@ and ( annotation_reachability
"detects when Android fragments are not explicitly nullified before becoming unreabable"
andimmutable_cast=
mk_checker~long:"immutable-cast"~default:true
"the detection of object cast from immutable type to mutable type. For instance, it will detect cast from ImmutableList to List, ImmutableMap to Map, and ImmutableSet to Set."
"the detection of object cast from immutable type to mutable type. For instance, it will \
andlitho=mk_checker~long:"litho""Experimental checkers supporting the Litho framework"
andliveness=
@ -724,7 +729,9 @@ and ( annotation_reachability
andownership=mk_checker~long:"ownership"~default:false"the detection of C++ lifetime bugs"
andprintf_args=
mk_checker~long:"printf-args"~default:true
"the detection of mismatch between the Java printf format strings and the argument types For, example, this checker will warn about the type error in `printf(\"Hello %d\", \"world\")`"
"the detection of mismatch between the Java printf format strings and the argument types \
"Specify the file containing the list of source files from which reactive analysis should start. Source files should be specified relative to project root or be absolute"
"Specify the file containing the list of source files from which reactive analysis should \
"Use this option in the uncommon case where the normal compilation process overrides the location of internal compiler headers. This option should specify regular expression with the path to those headers so that infer can use its own clang internal headers instead."
"Use this option in the uncommon case where the normal compilation process overrides the \
"The files in this regex will be ignored in the compilation process and an empty file will be passed to clang instead. This is to be used with the buck flavour infer-capture-all to work around missing generated files."
"The files in this regex will be ignored in the compilation process and an empty file will be \
"Continue the capture for the reactive analysis, increasing the changed files/procedures. (If a procedure was changed beforehand, keep the changed marking.)"
"Continue the capture for the reactive analysis, increasing the changed files/procedures. (If \
"Include C++ header models during compilation. Infer swaps some C++ headers for its own in order to get a better model of, eg, the standard library. This can sometimes cause compilation failures."
"Include C++ header models during compilation. Infer swaps some C++ headers for its own in \
"Debug mode for developing new linters. (Sets the analyzer to $(b,linters); also sets $(b,--debug), $(b,--debug-level-linters 2), $(b,--developer-mode), and unsets $(b,--allowed-failures) and $(b,--default-linters)."
"Debug mode for developing new linters. (Sets the analyzer to $(b,linters); also sets \
"Specify the file containing the list of source files for which a differential report is desired. Source files should be specified relative to project root or be absolute"
"Specify the file containing the list of source files for which a differential report is \
"Specify which set of the differential results is filtered with the modified files provided through the $(b,--differential-modified-files) argument. By default it is applied to all sets ($(b,introduced), $(b,fixed), and $(b,preexisting))"
"Specify which set of the differential results is filtered with the modified files provided \
"Do not show reports coming from this type of issue. Each checker can report a range of issue types. This option provides fine-grained filtering over which types of issue should be reported once the checkers have run. In particular, note that disabling issue types does not make the corresponding checker not run.\n By default, the following issue types are disabled: %s.\n\n See also $(b,--report-issue-type).\n"
"Do not show reports coming from this type of issue. Each checker can report a range of \
"Show reports coming from this type of issue. By default, all issue types are enabled except the ones listed in $(b,--disable-issue-type). Note that enabling issue types does not make the corresponding checker run; see individual checker options to turn them on or off."
"Show reports coming from this type of issue. By default, all issue types are enabled except \
"Specify a filter for issues to report. If multiple filters are specified, they are applied in the order in which they are specified. Each filter is applied to each issue detected, and only issues which are accepted by all filters are reported. Each filter is of the form: `<issue_type_regex>:<filename_regex>:<reason_string>`. The first two components are OCaml Str regular expressions, with an optional `!` character prefix. If a regex has a `!` prefix, the polarity is inverted, and the filter becomes a \"blacklist\" instead of a \"whitelist\". Each filter is interpreted as an implication: an issue matches if it does not match the `issue_type_regex` or if it does match the `filename_regex`. The filenames that are tested by the regex are relative to the `--project-root` directory. The `<reason_string>` is a non-empty string used to explain why the issue was filtered."
"Specify a filter for issues to report. If multiple filters are specified, they are applied \
"Specify a script that outputs the build command to capture in the previous version of the project. The script should output the command on stdout. For example \"echo make\"."
"Specify a script that outputs the build command to capture in the previous version of the \
"Show this help in the specified format. $(b,auto) sets the format to $(b,plain) if the environment variable $(b,TERM) is \"dumb\" or undefined, and to $(b,pager) otherwise."
"Show this help in the specified format. $(b,auto) sets the format to $(b,plain) if the \
environmentvariable$(b,TERM)is\"dumb\" or undefined, and to $(b,pager) otherwise."
"Specify custom documentation URL for some linter that overrides the default one. Useful if your project has specific ways of fixing a lint error that is not true in general or public info. Format: linter_name:doc_url."
"Specify custom documentation URL for some linter that overrides the default one. Useful if \
"Specify a script to checkout the current version of the project. The project is supposed to already be at that current version when running $(b,infer diff); the script is used after having analyzed the current and previous versions of the project, to restore the project to the current version."
"Specify a script to checkout the current version of the project. The project is supposed to \
"Specify the number of procedures to analyze per process when using $(b,--per-procedure-parallelism). If 0 is specified, each file is divided into $(b,--jobs) groups of procedures."
"Specify the number of procedures to analyze per process when using \
"Specify a script to be executed after the analysis results are written. This script will be passed, $(b,--issues-json), $(b,--issues-txt), $(b,--issues-xml), $(b,--project-root), and $(b,--results-dir)."
"Specify a script to be executed after the analysis results are written. This script will be \
"File path containing a json-encoded Java crash stacktrace. Used to guide the analysis (only with '-a crashcontext'). See tests/codetoanalyze/java/crashcontext/*.json for examples of the expected format."
"File path containing a json-encoded Java crash stacktrace. Used to guide the analysis (only \
"Directory path containing multiple json-encoded Java crash stacktraces. Used to guide the analysis (only with '-a crashcontext'). See tests/codetoanalyze/java/crashcontext/*.json for examples of the expected format."
"Directory path containing multiple json-encoded Java crash stacktraces. Used to guide the \
"Report error traces for runtime exceptions (Java only): generate preconditions for runtimeexceptions in Java and report errors for public methods which throw runtime exceptions"
"Report error traces for runtime exceptions (Java only): generate preconditions for \
"Infer will use xcpretty together with xcodebuild to analyze an iOS app. xcpretty just needs to be in the path, infer command is still just $(i,`infer -- <xcodebuild command>`)."
"Infer will use xcpretty together with xcodebuild to analyze an iOS app. xcpretty just needs \
"Specify treatment of dynamic dispatch in Java code: false 'none' treats dynamic dispatch as a call to unknown code and true triggers lazy dynamic dispatch. The latter mode follows the JVM semantics and creates procedure descriptions during symbolic execution using the type information found in the abstract state"
"Specify treatment of dynamic dispatch in Java code: false 'none' treats dynamic dispatch as \
"============================================================@\n= New infer execution begins@\n============================================================"
(** The functions in this module tend to raise more often than their counterparts in [Sqlite3]. In particular, they may raise if the [Sqlite3.Rc.t] result of certain operations is unexpected. *)
(** Assert that the result is either [Sqlite3.Rc.OK]. If [row_is_ok] then [Sqlite3.Rc.ROW] is also accepted. If the result is not valid, then if [fatal] is set raise [Error], otherwise log the error and proceed. *)
"Missing command line option. Either '--stacktrace stack.json' or '--stacktrace-dir ./dir' must be used when running '-a crashcontext'. This options expects a JSON formated stack trace or a directory containing multiple such traces, respectively. See tests/codetoanalyze/java/crashcontext/*.json for examples of the expected format."
"Missing command line option. Either '--stacktrace stack.json' or '--stacktrace-dir \
@ -25,7 +25,9 @@ let filter_parsed_linters_developer parsed_linters =
matchConfig.linterwith
|None->
L.(dieUserError)
"In linters developer mode you should debug only one linter at a time. This is important for debugging the rule. Pass the flag --linter <name> to specify the linter you want to debug."
"In linters developer mode you should debug only one linter at a time. This is \
"[WARNING:] Type Comparison failed... This might indicate that the types are different or the specified type is internally represented in a different way and therefore not recognized.@\n"
"[WARNING:] Type Comparison failed... This might indicate that the types are different or the \
"Unprotected call to method of un-annotated interface %s. Consider annotating the class with %a, adding a lock, or using an interface that is known to be thread-safe."
"Unprotected call to method of un-annotated interface %s. Consider annotating the class \
"@\nxcpretty not found in the path. Please consider installing xcpretty for a more robust integration with xcodebuild. Otherwise use the option --no-xcpretty.@\n@."
Josh Berdine
7 years ago
committed by
Facebook Github Bot