about summary refs log tree commit diff homepage
path: root/test
diff options
context:
space:
mode:
authorCristian Cadar <c.cadar@imperial.ac.uk>2023-11-14 15:06:06 +0000
committerMartinNowack <2443641+MartinNowack@users.noreply.github.com>2024-01-30 17:30:11 +0000
commit3e006dbfacd06e12818d97ae5aab1960324b27f9 (patch)
tree73337291c3dd372e11b0ebf03ceabe23c6cc4030 /test
parent3f65d6e9e41b5a5b458fb4642d8ac5bf684f3bc7 (diff)
downloadklee-3e006dbfacd06e12818d97ae5aab1960324b27f9.tar.gz
Add checks to the seed concretization tests about the expected number of queries
Diffstat (limited to 'test')
-rw-r--r--test/Feature/SeedConcretizeExtendFP.c4
-rw-r--r--test/Feature/SeedConcretizeExternalCall.c4
-rw-r--r--test/Feature/SeedConcretizeFP.c4
-rw-r--r--test/Feature/SeedConcretizeMalloc.c8
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
 }