diff options
author | Cristian Cadar <c.cadar@imperial.ac.uk> | 2019-03-11 14:08:47 +0000 |
---|---|---|
committer | MartinNowack <martin.nowack@gmail.com> | 2019-03-13 10:25:33 +0000 |
commit | 833de7329bc821aacf0ff63b053ae64f12f4bb12 (patch) | |
tree | 4863e2fccd5a21452d895364eb7e6a7aa156409f | |
parent | 92fd446f72136594e6519065fbd5bca3e0aee8e3 (diff) | |
download | klee-833de7329bc821aacf0ff63b053ae64f12f4bb12.tar.gz |
Documented options in ExprPPrinter.cpp and placed them into a new option category for building and printing expressions
-rw-r--r-- | include/klee/Expr.h | 4 | ||||
-rw-r--r-- | lib/Expr/Expr.cpp | 16 | ||||
-rw-r--r-- | lib/Expr/ExprPPrinter.cpp | 48 |
3 files changed, 47 insertions, 21 deletions
diff --git a/include/klee/Expr.h b/include/klee/Expr.h index 212053b4..cdc8474a 100644 --- a/include/klee/Expr.h +++ b/include/klee/Expr.h @@ -13,10 +13,11 @@ #include "klee/util/Bits.h" #include "klee/util/Ref.h" -#include "llvm/ADT/APInt.h" #include "llvm/ADT/APFloat.h" +#include "llvm/ADT/APInt.h" #include "llvm/ADT/DenseSet.h" #include "llvm/ADT/SmallVector.h" +#include "llvm/Support/CommandLine.h" #include "llvm/Support/raw_ostream.h" #include <sstream> @@ -38,6 +39,7 @@ class ObjectState; template<class T> class ref; +extern llvm::cl::OptionCategory ExprCat; /// Class representing symbolic expressions. /** diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp index 65e858c3..e6385136 100644 --- a/lib/Expr/Expr.cpp +++ b/lib/Expr/Expr.cpp @@ -8,22 +8,28 @@ //===----------------------------------------------------------------------===// #include "klee/Expr.h" -#include "klee/Config/Version.h" -#include "llvm/ADT/Hashing.h" -#include "llvm/Support/CommandLine.h" -#include "llvm/Support/raw_ostream.h" +#include "klee/Config/Version.h" // FIXME: We shouldn't need this once fast constant support moves into // Core. If we need to do arithmetic, we probably want to use APInt. #include "klee/Internal/Support/IntEvaluation.h" - #include "klee/util/ExprPPrinter.h" +#include "llvm/ADT/Hashing.h" +#include "llvm/Support/CommandLine.h" +#include "llvm/Support/raw_ostream.h" + #include <sstream> using namespace klee; using namespace llvm; +namespace klee { +llvm::cl::OptionCategory + ExprCat("Expression building and printing options", + "These options impact the way expressions are build and printed."); +} + namespace { cl::opt<bool> ConstArrayOpt("const-array-opt", diff --git a/lib/Expr/ExprPPrinter.cpp b/lib/Expr/ExprPPrinter.cpp index 58b8de7c..114c46b4 100644 --- a/lib/Expr/ExprPPrinter.cpp +++ b/lib/Expr/ExprPPrinter.cpp @@ -7,10 +7,11 @@ // //===----------------------------------------------------------------------===// -#include "klee/util/PrintContext.h" #include "klee/util/ExprPPrinter.h" #include "klee/Constraints.h" +#include "klee/OptionCategories.h" +#include "klee/util/PrintContext.h" #include "llvm/Support/CommandLine.h" #include "llvm/Support/raw_ostream.h" @@ -21,21 +22,38 @@ using namespace klee; namespace { - llvm::cl::opt<bool> - PCWidthAsArg("pc-width-as-arg", llvm::cl::init(true)); - - llvm::cl::opt<bool> - PCAllWidths("pc-all-widths", llvm::cl::init(false)); - llvm::cl::opt<bool> - PCPrefixWidth("pc-prefix-width", llvm::cl::init(true)); - - llvm::cl::opt<bool> - PCMultibyteReads("pc-multibyte-reads", llvm::cl::init(true)); - - llvm::cl::opt<bool> - PCAllConstWidths("pc-all-const-widths", llvm::cl::init(false)); -} +llvm::cl::opt<bool> PCWidthAsArg( + "pc-width-as-arg", llvm::cl::init(true), + llvm::cl::desc( + "Print the width as a separate argument, as opposed to a prefix " + "to the operation (default=true)"), + llvm::cl::cat(klee::ExprCat)); + +llvm::cl::opt<bool> + PCAllWidths("pc-all-widths", llvm::cl::init(false), + llvm::cl::desc("Print the width of all operations, including " + "booleans (default=false)"), + llvm::cl::cat(klee::ExprCat)); + +llvm::cl::opt<bool> + PCPrefixWidth("pc-prefix-width", llvm::cl::init(true), + llvm::cl::desc("Print width with 'w' prefix (default=true)"), + llvm::cl::cat(klee::ExprCat)); + +llvm::cl::opt<bool> + PCMultibyteReads("pc-multibyte-reads", llvm::cl::init(true), + llvm::cl::desc("Print ReadLSB and ReadMSB expressions " + "when possible (default=true)"), + llvm::cl::cat(klee::ExprCat)); + +llvm::cl::opt<bool> PCAllConstWidths( + "pc-all-const-widths", llvm::cl::init(false), + llvm::cl::desc( + "Always print the width of constant expressions (default=false)"), + llvm::cl::cat(klee::ExprCat)); + +} // namespace class PPrinter : public ExprPPrinter { public: |