Skip site navigation (1)Skip section navigation (2)

FreeBSD Manual Pages

  
 
  

home | help 
GOTO-DIFF(1)			 User Commands			  GOTO-DIFF(1)

NAME
       goto-diff - Syntactic diff of goto binaries

SYNOPSIS
       goto-diff [-?] [-h] [--help]
	      show help

       goto-diff old new
	      goto binaries to be compared

DESCRIPTION
OPTIONS
   Diff	options:
       --show-goto-functions
	      show loaded goto program

       --list-goto-functions
	      list loaded goto functions

       --show-properties
	      show the properties, but don't run analysis

       --show-loops
	      show the loops in	the programs

       -u | --unified
	      output unified diff

       --change-impact |

       --forward-impact	|

       --backward-impact
	      output  unified  diff with forward&backward/forward/backward de-
	      pendencies

       --compact-output
	      output dependencies in compact mode

   Program instrumentation options:
       --bounds-check
	      enable array bounds checks

       --pointer-check
	      enable pointer checks

       --memory-leak-check
	      enable memory leak checks

       --memory-cleanup-check
	      Enable memory cleanup checks: assert that	all dynamically	 allo-
	      cated memory is explicitly freed before terminating the program.

       --div-by-zero-check
	      enable division by zero checks for integer division

       --float-div-by-zero-check
	      enable division by zero checks for floating-point	division

       --signed-overflow-check
	      enable signed arithmetic over- and underflow checks

       --unsigned-overflow-check
	      enable arithmetic	over- and underflow checks

       --pointer-overflow-check
	      enable pointer arithmetic	over- and underflow checks

       --conversion-check
	      check whether values can be represented after type cast

       --undefined-shift-check
	      check shift greater than bit-width

       --float-overflow-check
	      check floating-point for +/-Inf

       --nan-check
	      check floating-point for NaN

       --enum-range-check
	      checks  that  all	 enum type expressions have values in the enum
	      range

       --pointer-primitive-check
	      checks that all pointers in pointer primitives are valid or null

       --retain-trivial-checks
	      include checks that are trivially	true

       --error-label label
	      check that label is unreachable

       --no-built-in-assertions
	      ignore assertions	in built-in library

       --no-assertions
	      ignore user assertions

       --no-assumptions
	      ignore user assumptions

       --assert-to-assume
	      convert user assertions to assumptions

       --cover CC
	      create test-suite	with coverage criterion	CC, where CC is	one of
	      assertion[s], assume[s], branch[es], condition[s], cover,	 deci-
	      sion[s], location[s], or mcdc

       --cover-failed-assertions
	      do  not stop coverage checking at	failed assertions (this	is the
	      default for --cover assertions)

       --show-test-suite
	      print test suite for coverage criterion (requires	--cover)

   Other options:
       --version
	      show version and exit

       --json-ui
	      use JSON-formatted output

       --flush
	      flush every line of output

       --verbosity n
	      verbosity	level

       --timestamp [monotonic|wall]
	      Print microsecond-precision timestamps.  monotonic:  stamps  in-
	      crease monotonically.  wall: ISO-8601 wall clock timestamps.

ENVIRONMENT
       All  tools honor	the TMPDIR environment variable	when generating	tempo-
       rary files and directories.

BUGS
       If   you	  encounter   a	  problem   please   create   an   issue    at
       https://github.com/diffblue/cbmc/issues

SEE ALSO
       cbmc(1),	goto-analyzer(1)

COPYRIGHT
       2016, Daniel Kroening, Peter Schrammel

jdiff-5.59.0			   June	2022			  GOTO-DIFF(1)

Want to link to this manual page? Use this URL:
<https://man.freebsd.org/cgi/man.cgi?query=goto-diff&sektion=1&manpath=FreeBSD+Ports+15.0>

home | help