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

       --cvc3 use CVC3

       --cvc4 use CVC4

       --cvc5 use CVC5

       --mathsat
              use MathSAT

       --yices
              use Yices

       --z3   use Z3

       --fpa  use theory of floating-point arithmetic

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