Man page - goto-synthesizer(1)

Packages contains this manual

Package: cbmc
apt-get install cbmc

Manuals in package:

Documentations in package:

cbmc

Manual

GOTO-SYNTHESIZER

NAME
SYNOPSIS
DESCRIPTION
OPTIONS
Accepts all of cbmc’s options plus the following backend options:
User-interface options:
ENVIRONMENT
BUGS
SEE ALSO
COPYRIGHT

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

COPYRIGHT

2022, Qinheping Hu