about summary refs log tree commit diff homepage
path: root/test/Feature/SeedConcretizeMalloc.c
diff options
context:
space:
mode:
Diffstat (limited to 'test/Feature/SeedConcretizeMalloc.c')
-rw-r--r--test/Feature/SeedConcretizeMalloc.c8
1 files changed, 6 insertions, 2 deletions
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
 }