Add checks to the seed concretization tests about the expected number of queries

4 files changed, 18 insertions, 2 deletions

diff --git a/test/Feature/SeedConcretizeExtendFP.c b/test/Feature/SeedConcretizeExtendFP.c
index 6a8de589..3ecd3bc3 100644
--- a/test/Feature/SeedConcretizeExtendFP.c
+++ b/test/Feature/SeedConcretizeExtendFP.c
@@ -8,6 +8,7 @@
 
 // RUN: rm -rf %t.klee-out-2
 // RUN: %klee --exit-on-error --output-dir=%t.klee-out-2 --seed-file %t.klee-out/test000001.ktest --allow-seed-extension %t.bc 2>&1 | FileCheck %s
+// RUN: %klee-stats --print-columns 'SolverQueries' --table-format=csv %t.klee-out-2 | FileCheck --check-prefix=CHECK-STATS %s
 
 #include "klee/klee.h"
 
@@ -30,4 +31,7 @@ int main() {
     // CHECK: concretizing (reason: floating point)
     assert((unsigned) d < 5001);
   }
+
+  // CHECK-STATS: 3
+  // These is similar to SeedConcretizeFP.c (1 query) plus the extra queries due to an incomplete seed
 }
diff --git a/test/Feature/SeedConcretizeExternalCall.c b/test/Feature/SeedConcretizeExternalCall.c
index 7eb69698..afc7fb6a 100644
--- a/test/Feature/SeedConcretizeExternalCall.c
+++ b/test/Feature/SeedConcretizeExternalCall.c
@@ -6,6 +6,7 @@
 
 // RUN: rm -rf %t.klee-out-2
 // RUN: %klee --external-calls=all --exit-on-error --output-dir=%t.klee-out-2 --seed-file %t.klee-out/test000001.ktest %t.bc
+// RUN: %klee-stats --print-columns 'SolverQueries' --table-format=csv %t.klee-out-2 | FileCheck --check-prefix=CHECK-STATS %s
 
 #include "klee/klee.h"
 
@@ -22,4 +23,7 @@ int main() {
   int x;
   klee_make_symbolic(&x, sizeof(x), "x");
   assert(abs(x) == 12345678);
+
+  // CHECK-STATS: 0
+  // No queries, but this will change once https://github.com/klee/klee/pull/1520 is merged
 }
diff --git a/test/Feature/SeedConcretizeFP.c b/test/Feature/SeedConcretizeFP.c
index bc5246ad..bde6b329 100644
--- a/test/Feature/SeedConcretizeFP.c
+++ b/test/Feature/SeedConcretizeFP.c
@@ -6,6 +6,7 @@
 
 // RUN: rm -rf %t.klee-out-2
 // RUN: %klee --exit-on-error --output-dir=%t.klee-out-2 --seed-file %t.klee-out/test000001.ktest %t.bc 2>&1 | FileCheck %s
+// RUN: %klee-stats --print-columns 'SolverQueries' --table-format=csv %t.klee-out-2 | FileCheck --check-prefix=CHECK-STATS %s
 
 #include "klee/klee.h"
 
@@ -24,4 +25,7 @@ int main() {
   double d = i;
   // CHECK: concretizing (reason: floating point)
   assert((unsigned) d == 12345678);
+
+  // CHECK-STATS: 1
+  // This one query involves the constraint that i == 12345678
 }
diff --git a/test/Feature/SeedConcretizeMalloc.c b/test/Feature/SeedConcretizeMalloc.c
index 1f916723..87748846 100644
--- a/test/Feature/SeedConcretizeMalloc.c
+++ b/test/Feature/SeedConcretizeMalloc.c
@@ -6,6 +6,7 @@
 
 // RUN: rm -rf %t.klee-out-2
 // RUN: %klee --output-dir=%t.klee-out-2 --seed-file %t.klee-out/test000001.ktest %t.bc | FileCheck --allow-empty %s
+// RUN: %klee-stats --print-columns 'SolverQueries' --table-format=csv %t.klee-out-2 | FileCheck --check-prefix=CHECK-STATS %s
 
 #include "klee/klee.h"
 
@@ -14,13 +15,13 @@
 #include <stdlib.h>
 
 void SeedGen() {
-  unsigned x;
+  size_t x;
   klee_make_symbolic(&x, sizeof(x), "x");
   klee_assume(x == 100);
 }
 
 int main(int argc, char **argv) {
-  unsigned s;
+  size_t s;
   klee_make_symbolic(&s, sizeof(s), "size");
   char *p = (char *)malloc(s);
   if (!p)
@@ -29,4 +30,7 @@ int main(int argc, char **argv) {
   if (s != 100)
     printf("Error\n");
     // CHECK-NOT: Error
+
+  // CHECK-STATS: 4
+  // These queries are due to the explicit constraint asserting that s is 100 and the implicit one checking if we have a huge malloc
 }