From 4ce774750042043fca78f50575f154f68296ab18 Mon Sep 17 00:00:00 2001 From: Daniel Dunbar Date: Thu, 21 May 2009 16:28:43 +0000 Subject: Start basic Regexp.c example for klee. - A few other web page tweaks. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72215 91177308-0d34-0410-b5e6-96231b3b80d8 --- www/resources/Regexp.c.html | 78 +++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 78 insertions(+) create mode 100644 www/resources/Regexp.c.html (limited to 'www/resources') diff --git a/www/resources/Regexp.c.html b/www/resources/Regexp.c.html new file mode 100644 index 00000000..cb3e3d75 --- /dev/null +++ b/www/resources/Regexp.c.html @@ -0,0 +1,78 @@ + + + +Enscript Output + + + + +

Regexp.c

+ +
+/* 
+ * 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;
+}
+
+
+
Generated by GNU enscript 1.6.4.
+ + -- cgit 1.4.1