Added a new test case that checks the --rewrite-equalities optimisation. The test contains the program proposed by Eric Rizzi in https://github.com/klee/klee/issues/227, and shows a case in which a constant constraint results after the optimisation.

1 files changed, 37 insertions, 0 deletions

diff --git a/test/Feature/RewriteEqualities.c b/test/Feature/RewriteEqualities.c
new file mode 100644
index 00000000..dcffa797
--- /dev/null
+++ b/test/Feature/RewriteEqualities.c
@@ -0,0 +1,37 @@
+// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --search=dfs --write-pcs --rewrite-equalities=false %t.bc
+// RUN: grep "(Read w8 (Extract w32 0 (SExt w64 (ZExt w32 N0)))" %t.klee-out/test000003.pc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --search=dfs --write-pcs --rewrite-equalities %t.bc
+// RUN: grep "(Read w8 8 const_arr1)" %t.klee-out/test000003.pc
+
+#include <stdio.h>
+#include <klee/klee.h>
+
+int run(unsigned char * x, char * y) {
+  y[6] = 15;
+
+  if(x[2] >= 10){
+    return 1;
+  }
+
+  if(y[x[2]] < 11){
+    if(x[2] == 8){
+      return 2;
+    } else{
+      return 3;
+    }
+  } else{
+    return 4;
+  }
+}
+
+unsigned char y[255];
+
+int main() {
+  unsigned char x[4];
+  klee_make_symbolic(&x, sizeof x, "x");
+
+  return run(x, y);
+}