#include "klee/Expr/ExprSMTLIBPrinter.h"
#include "klee/Support/Casting.h"
#include "llvm/Support/CommandLine.h"
#include "llvm/Support/ErrorHandling.h"
#include <stack>

Include dependency graph for ExprSMTLIBPrinter.cpp:

Go to the source code of this file.

Namespaces
namespace	ExprSMTLIBOptions

namespace	klee

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

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

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

Namespaces

Functions