From 8f2bc3a7188d93edd9a131bfd2101c2ec5adab9e Mon Sep 17 00:00:00 2001 From: Lukas Wölfer Date: Thu, 5 Apr 2018 15:56:05 +0200 Subject: Improved code quality --- test/Merging/incomplete_merge.c | 20 +++++++++++++++++--- 1 file changed, 17 insertions(+), 3 deletions(-) (limited to 'test') 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 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(); -- cgit 1.4.1