klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
ExprSMTLIBOptions Namespace Reference

Functions

llvm::cl::opt< bool > useLetExpressions ("smtlib-use-let-expressions", llvm::cl::desc("Enables generated SMT-LIBv2 files to use ""(let) expressions (default=on)"), llvm::cl::init(true))
 
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) )"), clEnumValEnd), llvm::cl::init(klee::ExprSMTLIBPrinter::DECIMAL))
 
llvm::cl::opt< bool > humanReadableSMTLIB ("smtlib-human-readable", llvm::cl::desc("Enables generated SMT-LIBv2 files to be human readable (default=off)"), llvm::cl::init(false))
 

Function Documentation

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::  valuesclEnumValN(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) )"), clEnumValEnd,
llvm::cl::  initklee::ExprSMTLIBPrinter::DECIMAL 
)

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

Here is the caller graph for this function:

llvm::cl::opt<bool> ExprSMTLIBOptions::humanReadableSMTLIB ( "smtlib-human-readable"  ,
llvm::cl::  desc"Enables generated SMT-LIBv2 files to be human readable (default=off)",
llvm::cl::  initfalse 
)
llvm::cl::opt<bool> ExprSMTLIBOptions::useLetExpressions ( "smtlib-use-let-expressions"  ,
llvm::cl::  desc"Enables generated SMT-LIBv2 files to use ""(let) expressions (default=on)",
llvm::cl::  inittrue 
)

Referenced by klee::createSMTLIBPrinter().

Here is the caller graph for this function: