Provided by: jbmc_5.95.1-4ubuntu1_amd64 
NAME
janalyzer - Data-flow analysis for Java bytecode
SYNOPSIS
janalyzer [-?] [-h] [--help]
show help
janalyzer method-name
Use the fully qualified name of a method as entry point, e.g., 'mypackage.Myclass.foo:(I)Z'
janalyzer class-name
The entry point is the method specified by --function, or otherwise, the public static void
main(String[]) method of the given class class-name.
janalyzer -jar jarfile
JAR file to be checked. The entry point is the method specified by --function or otherwise, the
public static void main(String[]) method of the class specified by --main-class or the main class
specified in the JAR manifest (checked in this order).
janalyzer --gb goto-binary
GOTO binary file to be checked. The entry point is the method specified by --function, or
otherwise, the public static void main(String[]) of the class specified by --main-class (checked
in this order).
DESCRIPTION
OPTIONS
-classpath dirs/jars, -cp dirs/jars, --classpath dirs/jars
Set class search path of directories and jar files using a colon-separated list of directories and
JAR archives to search for class files.
--main-class class-name
Set the name of the main class.
--function name
Set entry point function name.
Task options:
--show Displays a domain for every instruction in the GOTO binary. The format and information will
depend on the domain that has been selected.
--verify
Every property in the program is checked to see whether it is true (it always holds), unreachable,
false if it is reachable (due to the over-approximate analysis, it is not clear if locations are
reachable or if it is an overapproximation, so this is the best that can be achieved) or unknown.
If there are multiple points of execution that reach the same location, each will be checked and
the answers combined, with unknown taking precedence.
--simplify file_name
Writes a new version of the input program to file_name in which the program has been simplified
using information from the abstract interpreter. The exact simplification will depend on the
domain that is used but typically this might be replacing any expression that has a constant
value. If this makes instructions unreachable (for example if GOTO can be shown to never be
taken) they will be removed. Removal can be deactivated by passing --no-simplify-slicing. In the
ideal world simplify would be idempotent (i.e. running it a second time would not simplify
anything more than the first). However there are edge cases which are difficult or prohibitively
expensive to handle in the domain which can result in a second (or more) runs giving
simplification. Submitting bug reports for these is helpful but they may not be viable to fix.
--no-simplify-slicing
Do not remove instructions from which no property can be reached (use with --simplify).
--unreachable-instructions
Lists which instructions have a domain which is bottom (i.e. unreachable). If --function has been
used to set the program entry point then this can flag things like the main function as
unreachable.
--unreachable-functions
Similar to --unreachable-instructions, but reports which functions are definitely unreachable
rather than just instructions.
--reachable-functions
The negation of --unreachable-functions, reports which functions may be reachable. Note that
because the analysis is over-approximate, it is possible this will mark functions as reachable
when a more precise analysis (possibly using jbmc(1)) will show that there are no execution traces
that reach them.
Abstract interpreter options:
--location-sensitive
use location-sensitive abstract interpreter
--concurrent
This extends abstract interpretation with very restricted and special purpose handling of threads.
This needs the domain to have certain unusual properties for it to give a correct answer. At the
time of writing only --dependence-graph is compatible with it.
Domain options:
--constants
The default option, this stores one constant value per variable. This means it is fast but will
only find things that can be resolved by constant propagation. The domain has some handling of
arrays but limited support for pointers which means that in can potentially give unsound behavior.
--intervals
A domain that stores an interval for each integer and float variable. At the time of writing not
all operations are supported so the results can be quite over-approximate at points. It also has
limitations in the handling of pointers so can give unsound results.
--non-null
This domain is intended to find which pointers are not null. Its implementation is very limited
and it is not recommended.
--dependence-graph
Tracks data flow and information flow dependencies between instructions and produces a graph.
This includes doing points-to analysis and tracking reaching definitions (i.e. use-def chains).
This is one of the most extensive, correct and feature complete domains.
Output options:
These options control how the result of the task is output. The default is text to the standard output.
In the case of tasks that produce goto-programs (--simplify for example), the output options only affect
the logging and not the final form of the program.
--text file_name
Output results in plain text to given file.
--json file_name
Writes the output as a JSON object to file_name.
--xml file_name
Output results in XML format to file_name.
--dot file_name
Writes the output in dot(1) format to file_name. This is only supported by some domains and tasks
(for example --show --dependence-graph).
Specific analyses:
--taint file_name
perform taint analysis using rules in given file
--show-taint
print taint analysis results on stdout
--show-local-may-alias
perform procedure-local may alias analysis
Java Bytecode frontend options:
--disable-uncaught-exception-check
ignore uncaught exceptions and errors
--throw-assertion-error
Throw java.lang.AssertionError on violated assert statements instead of failing at the location of
the assert statement.
--throw-runtime-exceptions
Make implicit runtime exceptions explicit.
--assert-no-exceptions-thrown
Transform throw instructions into assert FALSE followed by assume FALSE.
--max-nondet-array-length N
Limit nondet (e.g. input) array size to at most N.
--max-nondet-tree-depth N
Limit size of nondet (e.g. input) object tree; at level N references are set to null.
--java-assume-inputs-non-null
Never initialize reference-typed parameter to the entry point with null.
--java-assume-inputs-interval [L:U] or [L:] or [:U]
Force numerical primitive-typed inputs (byte, short, int, long, float, double) to be initialized
within the given range; lower bound L and upper bound U must be integers; does not work for
arrays.
--java-assume-inputs-integral
Force float and double inputs to have integer values; does not work for arrays;
--java-max-vla-length N
Limit the length of user-code-created arrays to N.
--java-cp-include-files r
Regular expression or JSON list of files to load (with '@' prefix).
--java-load-class CLASS
Also load code from class CLASS.
--java-no-load-class CLASS
Never load code from class CLASS.
--ignore-manifest-main-class
Ignore Main-Class entries in JAR manifest files. If this option is specified and the options
--function and --main-class are not, we can be certain that all classes in the JAR file are
loaded.
--context-include i, --context-exclude e
Only analyze code matching specification i that does not match specification e, if
--context-exclude e is also used. All other methods are excluded, i.e., we load their signatures
and meta-information, but not their bodies. A specification is any prefix of a package, class or
method name, e.g. "org.cprover." or "org.cprover.MyClass." or
"org.cprover.MyClass.methodToStub:(I)Z". These options can be given multiple times. The default
for context-include is 'all included'; default for context-exclude is 'nothing excluded'.
--no-lazy-methods
Load and translate all methods given on the command line and in --classpath Default is to load
methods that appear to be reachable from the --function entry point or main class. Note that
--show-symbol-table, --show-goto-functions and --show-properties output are restricted to loaded
methods by default.
--lazy-methods-extra-entry-point METHODNAME
Treat METHODNAME as a possible program entry point for the purpose of lazy method loading.
METHODNAME can be a regular expression that will be matched against all symbols. If missing, a
java:: prefix will be added. If no descriptor is found, all overloads of a method will also be
added.
--static-values f
Load initial values of static fields from the given JSON file. We assign static fields to these
values instead of calling the normal static initializer (clinit) method. The argument can be a
relative or absolute path to the file.
--java-lift-clinit-calls
Lifts clinit calls in function bodies to the top of the function. This may reduce the overall cost
of static initialisation, but may be unsound if there are cyclic dependencies between static
initializers due to potentially changing their order of execution, or if static initializers have
side-effects such as updating another class' static field.
Platform options:
--arch arch
Set analysis architecture, which defaults to the host architecture. Use one of: alpha, arm, arm64,
armel, armhf, hppa, i386, ia64, mips, mips64, mips64el, mipsel, mipsn32, mipsn32el, powerpc,
ppc64, ppc64le, riscv64, s390, s390x, sh4, sparc, sparc64, v850, x32, x86_64, or none.
--os os
Set analysis operating system, which defaults to the host operating system. Use one of: freebsd,
linux, macos, solaris, or windows.
--i386-linux, --i386-win32, --i386-macos, --ppc-macos, --win32, --winx64
Set analysis architecture and operating system.
--LP64, --ILP64, --LLP64, --ILP32, --LP32
Set width of int, long and pointers, but don't override default architecture and operating system.
--16, --32, --64
Equivalent to --LP32, --ILP32, --LP64 (on Windows: --LLP64).
--little-endian
allow little-endian word-byte conversions
--big-endian
allow big-endian word-byte conversions
--gcc use GCC as preprocessor
Program representations:
--show-parse-tree
show parse tree
--show-symbol-table
show loaded symbol table
--show-goto-functions
show loaded goto program
--list-goto-functions
list loaded goto functions
--show-properties
show the properties, but don't run analysis
Program instrumentation options:
--no-assertions
ignore user assertions
--no-assumptions
ignore user assumptions
--property id
enable selected properties only
Other options:
--version
show version and exit
--verbosity n
verbosity level
--timestamp [monotonic|wall]
Print microsecond-precision timestamps. monotonic: stamps increase monotonically. wall: ISO-8601
wall clock timestamps.
ENVIRONMENT
All tools honor the TMPDIR environment variable when generating temporary files and directories.
BUGS
If you encounter a problem please create an issue at https://github.com/diffblue/cbmc/issues
SEE ALSO
jbmc(1), goto-analyzer(1)
COPYRIGHT
2016-2018, Daniel Kroening, Diffblue
janalyzer-5.59.0 June 2022 JANALYZER(1)