aboutsummaryrefslogtreecommitdiffhomepage
path: root/test
diff options
context:
space:
mode:
authorLukas Wölfer <lukas.woelfer@rwth-aachen.de>2018-04-05 15:56:05 +0200
committerCristian Cadar <c.cadar@imperial.ac.uk>2018-05-15 15:18:36 +0100
commit8f2bc3a7188d93edd9a131bfd2101c2ec5adab9e (patch)
tree6228802a03ce503879b4e41ce643912afe512f04 /test
parente5a18f47a8cdd37a5c2721e89df68ea7aafed8a0 (diff)
downloadklee-8f2bc3a7188d93edd9a131bfd2101c2ec5adab9e.tar.gz
Improved code quality
Diffstat (limited to 'test')
-rw-r--r--test/Merging/incomplete_merge.c20
1 files changed, 17 insertions, 3 deletions
diff --git a/test/Merging/incomplete_merge.c b/test/Merging/incomplete_merge.c
index 1962cfaa..bb5e4f37 100644
--- a/test/Merging/incomplete_merge.c
+++ b/test/Merging/incomplete_merge.c
@@ -16,6 +16,11 @@
// CHECK: close merge:
// CHECK: close merge:
+// This test merges branches with vastly different instruction counts.
+// The incomplete merging heuristic merges preemptively if a branch takes too long.
+// It might occur that the random branch selection completes the heavy branch first,
+// which results in the branches being merged completely.
+
#include <klee/klee.h>
int main(int argc, char **args) {
@@ -31,15 +36,24 @@ int main(int argc, char **args) {
if (a == 0) {
klee_open_merge();
+ for (int i = 0; i < 5; ++i){
+ foo += 2;
+ }
if (x == 1) {
- foo = 5;
+ foo += 5;
} else if (x == 2) {
- foo = 6;
+ for (int i = 0; i < 10; ++i) {
+ foo += foo;
+ }
} else {
- foo = 7;
+ foo += 7;
}
klee_close_merge();
+ } else if (a == 1) {
+ foo = 4;
+ } else {
+ foo = 3;
}
klee_close_merge();