diff options
author | Lukas Wölfer <lukas.woelfer@rwth-aachen.de> | 2018-04-05 15:56:05 +0200 |
---|---|---|
committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2018-05-15 15:18:36 +0100 |
commit | 8f2bc3a7188d93edd9a131bfd2101c2ec5adab9e (patch) | |
tree | 6228802a03ce503879b4e41ce643912afe512f04 /test/Merging | |
parent | e5a18f47a8cdd37a5c2721e89df68ea7aafed8a0 (diff) | |
download | klee-8f2bc3a7188d93edd9a131bfd2101c2ec5adab9e.tar.gz |
Improved code quality
Diffstat (limited to 'test/Merging')
-rw-r--r-- | test/Merging/incomplete_merge.c | 20 |
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(); |