1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
|
diff --git a/src/dfasearch.c b/src/dfasearch.c
index a43f822aafa0..36db6965b0c3 100644
--- a/src/dfasearch.c
+++ b/src/dfasearch.c
@@ -18,6 +18,46 @@
/* Written August 1992 by Mike Haertel. */
+#include <stdbool.h>
+#include <stdint.h>
+#include <stdlib.h>
+
+void klee_make_symbolic(void *addr, size_t nbytes, const char *name) {}
+void klee_assume(uintptr_t x) {}
+int __choose(const char *switch_id)
+{
+ char *env = getenv("KLEE_META");
+ if (env == NULL)
+ return 0;
+ int result=atoi(env);
+ return result;
+}
+
+#define MAX_NAME_LENGTH 1000
+#define SYMBOLIC_OUTPUT_PROTO(type) \
+ type __klee_symbolic_output_##type(type expr, char* id) { \
+ static int instance = 0; \
+ char name[MAX_NAME_LENGTH]; \
+ sprintf(name, "out!%s!%d", id, instance++); \
+ type s; \
+ klee_make_symbolic(&s, sizeof(s), name); \
+ klee_assume(s == expr); \
+ return expr; \
+}
+SYMBOLIC_OUTPUT_PROTO(int)
+SYMBOLIC_OUTPUT_PROTO(long)
+SYMBOLIC_OUTPUT_PROTO(bool)
+SYMBOLIC_OUTPUT_PROTO(char)
+#undef SYMBOLIC_OUTPUT_PROTO
+
+#ifdef KLEE_RUNTIME
+#define KLEE_OUTPUT(type, expr, name) \
+ __klee_symbolic_output_##type((expr), (name))
+int printf (const char *__restrict __format, ...) { return 0; }
+#else
+#define KLEE_OUTPUT(type, expr, name) (expr)
+#endif
+
#include <config.h>
#include "search.h"
#include "dfa.h"
@@ -357,8 +397,14 @@ EGexecute (char const *buf, size_t size, size_t *match_size,
{
/* Good enough for a non-exact match.
No need to look at further patterns, if any. */
+int __choose0 = __choose("__SWITCH0");
+klee_make_symbolic(&__choose0, sizeof(__choose0), "__choose0");
+if (__choose0 == 0) {
beg = match;
goto success_in_len;
+} else if (__choose0 == 1) {
+ goto success;
+}
}
if (match < best_match || (match == best_match && len > best_len))
{
|
