ExprSMTLIBOptions Namespace Reference

Functions
llvm::cl::opt< klee::ExprSMTLIBPrinter::ConstantDisplayMode >	argConstantDisplayMode ("smtlib-display-constants", llvm::cl::desc("Sets how bitvector constants are written in generated " "SMT-LIBv2 files (default=dec)"), llvm::cl::values(clEnumValN(klee::ExprSMTLIBPrinter::BINARY, "bin", "Use binary form (e.g. #b00101101)"), clEnumValN(klee::ExprSMTLIBPrinter::HEX, "hex", "Use Hexadecimal form (e.g. #x2D)"), clEnumValN(klee::ExprSMTLIBPrinter::DECIMAL, "dec", "Use decimal form (e.g. (_ bv45 8) )")), llvm::cl::init(klee::ExprSMTLIBPrinter::DECIMAL), llvm::cl::cat(klee::ExprCat))
llvm::cl::opt< bool >	humanReadableSMTLIB ("smtlib-human-readable", llvm::cl::desc("Enables generated SMT-LIBv2 files to " "be human readable (default=false)"), llvm::cl::init(false), llvm::cl::cat(klee::ExprCat))
llvm::cl::opt< klee::ExprSMTLIBPrinter::AbbreviationMode >	abbreviationMode ("smtlib-abbreviation-mode", llvm::cl::desc("Choose abbreviation mode to use in SMT-LIBv2 files (default=let)"), llvm::cl::values(clEnumValN(klee::ExprSMTLIBPrinter::ABBR_NONE, "none", "Do not abbreviate"), clEnumValN(klee::ExprSMTLIBPrinter::ABBR_LET, "let", "Abbreviate with let"), clEnumValN(klee::ExprSMTLIBPrinter::ABBR_NAMED, "named", "Abbreviate with :named annotations")), llvm::cl::init(klee::ExprSMTLIBPrinter::ABBR_LET), llvm::cl::cat(klee::ExprCat))

Function Documentation

abbreviationMode()

llvm::cl::opt< klee::ExprSMTLIBPrinter::AbbreviationMode > ExprSMTLIBOptions::abbreviationMode	(	"smtlib-abbreviation-mode"	,
		llvm::cl::desc("Choose abbreviation mode to use in SMT-LIBv2 files (default=let)")	,
		llvm::cl::values(clEnumValN(klee::ExprSMTLIBPrinter::ABBR_NONE, "none", "Do not abbreviate"), clEnumValN(klee::ExprSMTLIBPrinter::ABBR_LET, "let", "Abbreviate with let"), clEnumValN(klee::ExprSMTLIBPrinter::ABBR_NAMED, "named", "Abbreviate with :named annotations"))	,
		llvm::cl::init(klee::ExprSMTLIBPrinter::ABBR_LET)	,
		llvm::cl::cat(klee::ExprCat)
	)

Referenced by klee::ExprSMTLIBPrinter::ExprSMTLIBPrinter().

Here is the caller graph for this function:

argConstantDisplayMode()

llvm::cl::opt< klee::ExprSMTLIBPrinter::ConstantDisplayMode > ExprSMTLIBOptions::argConstantDisplayMode	(	"smtlib-display-constants"	,
		llvm::cl::desc("Sets how bitvector constants are written in generated " "SMT-LIBv2 files (default=dec)")	,
		llvm::cl::values(clEnumValN(klee::ExprSMTLIBPrinter::BINARY, "bin", "Use binary form (e.g. #b00101101)"), clEnumValN(klee::ExprSMTLIBPrinter::HEX, "hex", "Use Hexadecimal form (e.g. #x2D)"), clEnumValN(klee::ExprSMTLIBPrinter::DECIMAL, "dec", "Use decimal form (e.g. (_ bv45 8) )"))	,
		llvm::cl::init(klee::ExprSMTLIBPrinter::DECIMAL)	,
		llvm::cl::cat(klee::ExprCat)
	)

Referenced by klee::ExprSMTLIBPrinter::ExprSMTLIBPrinter().

Here is the caller graph for this function:

humanReadableSMTLIB()

llvm::cl::opt< bool > ExprSMTLIBOptions::humanReadableSMTLIB	(	"smtlib-human-readable"	,
		llvm::cl::desc("Enables generated SMT-LIBv2 files to " "be human readable (default=false)")	,
		llvm::cl::init(false)	,
		llvm::cl::cat(klee::ExprCat)
	)