From 6f290d8f9e9d7faac295cb51fc96884a18f4ded4 Mon Sep 17 00:00:00 2001
From: Daniel Dunbar <daniel@zuster.org>
Date: Thu, 21 May 2009 04:36:41 +0000
Subject: Initial KLEE checkin.  - Lots more tweaks, documentation, and web
 page content is needed,    but this should compile & work on OS X & Linux.

git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72205 91177308-0d34-0410-b5e6-96231b3b80d8
---
 examples/regexp/Regexp.c  | 62 +++++++++++++++++++++++++++++++++++++++++++++++
 examples/regexp/notes.txt | 26 ++++++++++++++++++++
 2 files changed, 88 insertions(+)
 create mode 100644 examples/regexp/Regexp.c
 create mode 100644 examples/regexp/notes.txt

(limited to 'examples/regexp')

diff --git a/examples/regexp/Regexp.c b/examples/regexp/Regexp.c
new file mode 100644
index 00000000..f3e751f9
--- /dev/null
+++ b/examples/regexp/Regexp.c
@@ -0,0 +1,62 @@
+/* 
+ * Simple regular expression matching.
+ *
+ * From:
+ *   The Practice of Programming
+ *   Brian W. Kernighan, Rob Pike
+ *
+ */ 
+
+#include <klee/klee.h>
+
+static int matchhere(char*,char*);
+
+static int matchstar(int c, char *re, char *text) {
+  do {
+    if (matchhere(re, text))
+      return 1;
+  } while (*text != '\0' && (*text++ == c || c== '.'));
+  return 0;
+}
+
+static int matchhere(char *re, char *text) {
+  if (re[0] == '\0')
+     return 0;
+  if (re[1] == '*')
+    return matchstar(re[0], re+2, text);
+  if (re[0] == '$' && re[1]=='\0')
+    return *text == '\0';
+  if (*text!='\0' && (re[0]=='.' || re[0]==*text))
+    return matchhere(re+1, text+1);
+  return 0;
+}
+
+int match(char *re, char *text) {
+  if (re[0] == '^')
+    return matchhere(re+1, text);
+  do {
+    if (matchhere(re, text))
+      return 1;
+  } while (*text++ != '\0');
+  return 0;
+}
+
+/*
+ * Harness for testing with KLEE.
+ */
+
+// The size of the buffer to test with.
+#define SIZE 7
+
+int main() {
+  // The input regular expression.
+  char re[SIZE];
+  
+  // Make the input symbolic. 
+  klee_make_symbolic_name(re, sizeof re, "re");
+
+  // Try to match against a constant string "hello".
+  match(re, "hello");
+
+  return 0;
+}
diff --git a/examples/regexp/notes.txt b/examples/regexp/notes.txt
new file mode 100644
index 00000000..7d25585c
--- /dev/null
+++ b/examples/regexp/notes.txt
@@ -0,0 +1,26 @@
+clang -m32 -I ~/private/klee/include -c -emit-llvm Regexp.c
+
+klee Regexp.o
+klee --only-output-states-covering-new Regexp.o
+ls -l klee-out-0
+ls -l klee-out-1
+ls -l klee-last
+
+cd klee-last
+klee-bout-tool *.bout
+klee-bout-tool --trim-zeros *.bout
+
+Stuff to show:
+Adding klee_prefer_cex
+
+PrintStats.py klee-last
+
+PrintStats.py klee-last
+Why not 100% coverage?
+
+clang -g -m32 -I ~/private/klee/include -c -emit-llvm Regexp.c
+
+KCachegrind?
+
+Disable klee_assume, show coverage again (why is klee-check-div getting pulled
+in?)
-- 
cgit 1.4.1