Implement array declarations.

 - Printing current prints all declarations, and we allow redefinition, since
   the printer doesn't know what has already been printed.

 - Names don't print right yet, since the Array* object doesn't have the name.

 - Various things are unsupported.
   o Array domain/range must be w32/w8.
   o Concrete initializers for arrays are unsupported.


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

1 files changed, 7 insertions, 1 deletions

diff --git a/lib/Core/ExecutorUtil.cpp b/lib/Core/ExecutorUtil.cpp
index 1e346e89..a1e030a5 100644
--- a/lib/Core/ExecutorUtil.cpp
+++ b/lib/Core/ExecutorUtil.cpp
@@ -46,7 +46,10 @@ Executor::evalConstantExpr(llvm::ConstantExpr *ce) {
   
   switch (ce->getOpcode()) {
     default :
-      assert(0 && "unknown ConstantExpr type");
+      ce->dump();
+      llvm::cerr << "error: unknown ConstantExpr type\n"
+                 << "opcode: " << ce->getOpcode() << "\n";
+      abort();
 
     case Instruction::Trunc: return ExtractExpr::createByteOff(op1, 
 							       0,
@@ -128,6 +131,9 @@ Executor::evalConstantExpr(llvm::ConstantExpr *ce) {
       return SelectExpr::create(op1, op2, op3);
     }
 
+    case Instruction::FAdd:
+    case Instruction::FSub:
+    case Instruction::FMul:
     case Instruction::FDiv:
     case Instruction::FRem:
     case Instruction::FPTrunc: