More constant Array support.

 - The are parsed, printed, and solved now.

 - Remove some members of ArrayDecl which are only duplicates of Array members.

 - KLEE still doesn't create these, but you can write them by hand.

The EXE style constant array optimization for STP (turning the initial writes
into asserts) is now only a stones throw away, but I need to leave something fun
to do tomorrow. :)


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

1 files changed, 7 insertions, 0 deletions

diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp
index 71516c24..7a1b356c 100644
--- a/lib/Solver/Solver.cpp
+++ b/lib/Solver/Solver.cpp
@@ -675,6 +675,13 @@ STPSolverImpl::computeInitialValues(const Query &query,
 
   ExprHandle stp_e = builder->construct(query.expr);
      
+  if (0) {
+    char *buf;
+    unsigned long len;
+    vc_printQueryStateToBuffer(vc, stp_e, &buf, &len, false);
+    fprintf(stderr, "note: STP query: %.*s\n", (unsigned) len, buf);
+  }
+
   bool success;
   if (useForkedSTP) {
     success = runAndGetCexForked(vc, builder, stp_e, objects, values,