1 files changed, 17 insertions, 0 deletions
diff --git a/test/DeterministicAllocation/use-after-free.c b/test/DeterministicAllocation/use-after-free.c
new file mode 100644
index 00000000..c4a14435
--- /dev/null
+++ b/test/DeterministicAllocation/use-after-free.c
@@ -0,0 +1,17 @@
+// RUN: %clang %s -emit-llvm -g -c -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee -kdalloc -kdalloc-quarantine=1 -output-dir=%t.klee-out %t.bc -exit-on-error >%t.output 2>&1
+// RUN: FileCheck %s -input-file=%t.output
+
+#include <stdlib.h>
+#include <string.h>
+
+int main() {
+  void *ptr = malloc(8);
+  free(ptr);
+
+  // CHECK: use after free
+  memset(ptr, 0, 8);
+
+  return 0;
+}