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 dependen-
	    cies

     --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 allocated
	    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 as-
	    sertion[s], assume[s], branch[es], condition[s], cover, decision[s],
	    location[s], or mcdc

     --cover-failed-assertions
	    do not stop coverage checking at failed assertions (this is the  de-
	    fault 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 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
     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.1.quarterly>

home | help