Skip to content

Commit 9c086c1

Browse files
authored
Update formal_verification.md
1 parent 98d0bf2 commit 9c086c1

File tree

1 file changed

+3
-2
lines changed

1 file changed

+3
-2
lines changed

formal_verification.md

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -75,7 +75,7 @@ KLEE: done: generated tests = 801298
7575
klee@cc0c26c5b84c:~$
7676
```
7777
78-
Similarly, the code below tests both `re_compile(...)` and `re_match(...)` which should be sufficient.
78+
Similarly, the code below tests both `re_compile(...)` and `re_match(...)` which should be sufficient for coverage of the core logic.
7979
Depending on your hardware, you should be able to increase the sizes of `pat` and `txt` to increase your confidence in the verification.
8080
8181
@@ -108,7 +108,7 @@ int main(int argc, char* argv[])
108108
}
109109
```
110110

111-
My modest hardware completes a check of a 7-char pattern and a 3-char text string in 20-30 minutes (size includes null-termination):
111+
My modest hardware (T420/i5-2520M@2.5GHz/8GB) completes a check of a 7-char pattern and a 3-char text string in 20-30 minutes (size includes null-termination):
112112

113113
```
114114
klee@780432c1aaae0:~$ clang -emit-llvm -g -c -O0 -Xclang -disable-O0-optnone re.c
@@ -137,3 +137,4 @@ user 19m38.438s
137137
sys 9m34.654s
138138
klee@780432c1aaae0:~$
139139
```
140+

0 commit comments

Comments
 (0)