about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
authorCristian Cadar <c.cadar@imperial.ac.uk>2019-03-11 14:08:47 +0000
committerMartinNowack <martin.nowack@gmail.com>2019-03-13 10:25:33 +0000
commit833de7329bc821aacf0ff63b053ae64f12f4bb12 (patch)
tree4863e2fccd5a21452d895364eb7e6a7aa156409f
parent92fd446f72136594e6519065fbd5bca3e0aee8e3 (diff)
downloadklee-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.h4
-rw-r--r--lib/Expr/Expr.cpp16
-rw-r--r--lib/Expr/ExprPPrinter.cpp48
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: