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

FreeBSD Manual Pages

  
 
  

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

NAME
     goto-synthesizer - Synthesize and apply loop contracts of goto binaries.

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

     goto-synthesizer --version
	    show version and exit

     goto-synthesizer [options] in [out]
	    perform synthesis and loop-contracts transformation

DESCRIPTION
     goto-synthesis  reads  a GOTO binary, performs loop-contracts synthesis and
     program transformation for the synthesized contracts, and then  writes  the
     resulting program as GOTO binary on disk.

OPTIONS
     -loop-contracts-no-unwind
	    do	not unwind transformed loops after applying the synthesized loop
	    contracts

     --dump-loop-contracts
	    dump the synthesized loop contracts as JSON

     --json-tpt file
	    specify the output destination of the loop-contracts JSON

   Accepts all of cbmc's options plus the following backend options:
     --object-bits n
	    number of bits used for object addresses

     --sat-solver solver
	    use specified SAT solver

     --external-sat-solver cmd
	    command to invoke SAT solver process

     --no-sat-preprocessor
	    disable the SAT solver's simplifier

     --dimacs
	    generate CNF in DIMACS format

     --beautify
	    beautify the counterexample (greedy heuristic)

     --smt1
	    use default SMT1 solver (obsolete)

     --smt2
	    use default SMT2 solver (Z3)

     --bitwuzla
	    use Bitwuzla

     --boolector
	    use Boolector

     --cprover-smt2
	    use CPROVER SMT2 solver

     --cvc5
	    use CVC5

     --mathsat
	    use MathSAT

     --yices
	    use Yices

     --z3   use Z3

     --fpa  use theory of floating-point arithmetic

     --external-smt2-solver cmd
	    Use cmd to invoke the SMT2 solver. Combine with one  of  the  solver
	    choices for solver-specific constraints.

     --refine
	    use refinement procedure (experimental)

     --refine-arrays
	    use refinement for arrays only

     --refine-arithmetic
	    refinement of arithmetic expressions only

     --max-node-refinement
	    maximum refinement iterations for arithmetic expressions

     --incremental-smt2-solver cmd
	    Use  the  incremental SMT backend where cmd is the command to invoke
	    the SMT solver of choice.
	    Example invocations:
	      --incremental-smt2-solver 'z3 -smt2 -in' (use the Z3 solver).
	      --incremental-smt2-solver  'cvc5	--lang=smtlib2.6  --incremental'
	    (use the CVC5 solver).

	    Note that:
	    The  solver name must be in the "PATH" or be an executable with full
	    path.
	    The SMT solver should accept incremental SMTlib v2.6 formatted input
	    from the stdin.
	    The SMT solver should support the QF_AUFBV logic.

     --outfile filename
	    output formula to given file

     --dump-smt-formula filename
	    output smt incremental formula to the given file

     --write-solver-stats-to json-file
	    collect the solver query complexity

     --arrays-uf-never
	    never turn arrays into uninterpreted functions

     --arrays-uf-always
	    always turn arrays into uninterpreted functions

   User-interface options:
     --xml-ui
	    use XML-formatted output

     --json-ui
	    use JSON-formatted output

     --verbosity n
	    verbosity level

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-cc(1) goto-instrument(1)

COPYRIGHT
     2022, Qinheping Hu

goto-synthesizer-5.59.0 	  December 2022 	     GOTO-SYNTHESIZER(1)

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

home | help