From 58d454647ff1465128423fa02896f84e5d3b989a Mon Sep 17 00:00:00 2001
From: Frank Busse <bb0xfb@gmail.com>
Date: Tue, 11 Jan 2022 19:28:24 +0000
Subject: tests: add Feature/KleeStatsTermClasses.c

---
 test/Feature/KleeStatsTermClasses.c | 89 +++++++++++++++++++++++++++++++++++++
 1 file changed, 89 insertions(+)
 create mode 100644 test/Feature/KleeStatsTermClasses.c

(limited to 'test')

diff --git a/test/Feature/KleeStatsTermClasses.c b/test/Feature/KleeStatsTermClasses.c
new file mode 100644
index 00000000..1606128c
--- /dev/null
+++ b/test/Feature/KleeStatsTermClasses.c
@@ -0,0 +1,89 @@
+// RUN: %clang %s -fsanitize=unsigned-integer-overflow -emit-llvm -g %O0opt -c -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --max-stack-frames=15 --switch-type=simple --search=dfs --use-merge --ubsan-runtime --write-no-tests --output-dir=%t.klee-out %t.bc 2> %t.log
+// RUN: %klee-stats --print-columns 'TermExit,TermEarly,TermSolverErr,TermProgrErr,TermUserErr,TermExecErr,TermEarlyAlgo,TermEarlyUser' --table-format=csv %t.klee-out > %t.stats
+// RUN: FileCheck -check-prefix=CHECK-STATS -input-file=%t.stats %s
+
+
+#pragma GCC diagnostic ignored "-Wimplicit-function-declaration"
+#pragma GCC diagnostic ignored "-Winfinite-recursion"
+
+// do not #include "klee/klee.h" to misuse API
+
+#include <assert.h>
+#include <limits.h>
+#include <stdint.h>
+#include <stdlib.h>
+
+const char *ro_str = "hi";
+int global[3];
+
+
+void max_depth(int a) {
+  max_depth(a + 1); // Early (MaxDepth)
+}
+
+unsigned mul(unsigned a, unsigned b) {
+  uint32_t r = a * b;
+  return r;
+}
+
+void merge() {
+  int cond;
+  int a = 42;
+  klee_make_symbolic(&cond, sizeof(cond), "merge_cond");
+
+  klee_open_merge();
+  if (cond == 8) a++;
+  else a--;
+  klee_close_merge(); // EarlyAlgorithm (Merge)
+  // (normal) Exit
+}
+
+void bogus_external();
+
+
+int main(void) {
+  int cond;
+  klee_make_symbolic(&cond, sizeof(cond), "cond");
+
+  switch(cond) {
+    case __LINE__:
+      max_depth(17);
+    case __LINE__:
+      assert(0); // ProgErr (Assert)
+      break;
+    case __LINE__:
+      abort(); // ProgErr (Abort)
+    case __LINE__:
+      free(global); // ProgErr (Free)
+    case __LINE__: {
+      unsigned a = UINT_MAX, b = UINT_MAX, c;
+      c = mul(a, b); // ProgErr (Overflow)
+    }
+    case __LINE__:
+      free((void*)0xdeadbeef); // ProgErr (Ptr)
+      break;
+    case __LINE__: {
+      char *p = (char*)ro_str;
+      p[0] = '!'; // ProgErr (ReadOnly)
+    }
+    case __LINE__:
+      klee_report_error(__FILE__, __LINE__, "Report Error", "report.err"); // ProgErr (Report)
+    case __LINE__:
+      klee_make_symbolic(1); // UserErr
+    case __LINE__:
+      bogus_external(); // ExecErr (External)
+    case __LINE__:
+      merge();
+      break;
+    case __LINE__:
+      klee_silent_exit(0); // EarlyUser
+    default:
+      return 0; // (normal) Exit
+  }
+}
+
+// Check termination classes
+// CHECK-STATS: TermExit,TermEarly,TermSolverErr,TermProgrErr,TermUserErr,TermExecErr,TermEarlyAlgo,TermEarlyUser
+// CHECK-STATS: 2,1,0,7,1,1,1,1
-- 
cgit 1.4.1