jdiff - Syntactic diff of goto programs obtained from Java bytecode
show help
jars to be compared
show loaded goto program
list loaded goto functions
show the properties, but don't run analysis
show the loops in the programs
output unified diff
--change-impact |
--forward-impact |
output unified diff with forward&backward/forward/backward dependencies
output dependencies in compact mode
ignore user assertions
ignore user assumptions
Add instrumentation as used with jbmc(1) for creating test-suite with coverage criterion CC, where CC is one of assertion[s], assume[s], branch[es], condition[s], cover, decision[s], location[s], or mcdc.
do not stop coverage checking at failed assertions (this is the default for --cover assertions)
print test suite for coverage criterion (requires --cover)
show version and exit
use JSON-formatted output
verbosity level
Print microsecond-precision timestamps. monotonic: stamps increase monotonically. wall: ISO-8601 wall clock timestamps.
All tools honor the TMPDIR environment variable when generating temporary files and directories.
If you encounter a problem please create an issue at https://github.com/diffblue/cbmc/issues
jbmc(1), goto-analyzer(1)
2016-2018, Daniel Kroening, Peter Schrammel