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 bina-
       ries.

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 in-
	      voke the SMT solver of choice.
	      Example invocations:
		--incremental-smt2-solver 'z3 -smt2 -in' (use the Z3 solver).
		--incremental-smt2-solver 'cvc5	 --lang=smtlib2.6  --incremen-
	      tal' (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	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-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.0>

home | help