Add NonConstantExpr, so it is possible to statically type an expression that is

known to be not-constant.


git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73352 91177308-0d34-0410-b5e6-96231b3b80d8

1 files changed, 15 insertions, 7 deletions

diff --git a/include/klee/Expr.h b/include/klee/Expr.h
index 9df9a699..79a8ec6f 100644
--- a/include/klee/Expr.h
+++ b/include/klee/Expr.h
@@ -427,7 +427,15 @@ public:
   
 // Utility classes
 
-class BinaryExpr : public Expr {
+class NonConstantExpr : public Expr {
+public:
+  static bool classof(const Expr *E) {
+    return E->getKind() != Expr::Constant;
+  }
+  static bool classof(const NonConstantExpr *) { return true; }
+};
+
+class BinaryExpr : public NonConstantExpr {
 public:
   ref<Expr> left, right;
 
@@ -470,7 +478,7 @@ public:
 
 // Special
 
-class NotOptimizedExpr : public Expr {
+class NotOptimizedExpr : public NonConstantExpr {
 public:
   static const Kind kind = NotOptimized;
   static const unsigned numKids = 1;
@@ -612,7 +620,7 @@ public:
 };
 
 /// Class representing a one byte read from an array. 
-class ReadExpr : public Expr {
+class ReadExpr : public NonConstantExpr {
 public:
   static const Kind kind = Read;
   static const unsigned numKids = 1;
@@ -657,7 +665,7 @@ public:
 
 
 /// Class representing an if-then-else expression.
-class SelectExpr : public Expr {
+class SelectExpr : public NonConstantExpr {
 public:
   static const Kind kind = Select;
   static const unsigned numKids = 3;
@@ -714,7 +722,7 @@ public:
 /** Children of a concat expression can have arbitrary widths.  
     Kid 0 is the left kid, kid 1 is the right kid.
 */
-class ConcatExpr : public Expr { 
+class ConcatExpr : public NonConstantExpr { 
 public: 
   static const Kind kind = Concat;
   static const unsigned numKids = 2;
@@ -772,7 +780,7 @@ public:
     bit offset {\tt offset} of width {\tt width}.  Bit 0 is the right most 
     bit of the expression.
  */
-class ExtractExpr : public Expr { 
+class ExtractExpr : public NonConstantExpr { 
 public:
   static const Kind kind = Extract;
   static const unsigned numKids = 1;
@@ -825,7 +833,7 @@ public:
 
 // Casting
 
-class CastExpr : public Expr {
+class CastExpr : public NonConstantExpr {
 public:
   ref<Expr> src;
   Width width;