diff --git a/regression/cbmc-cover/block-coverage-report1/test.desc b/regression/cbmc-cover/block-coverage-report1/test.desc index c978f5fab29..49e7fea82e9 100644 --- a/regression/cbmc-cover/block-coverage-report1/test.desc +++ b/regression/cbmc-cover/block-coverage-report1/test.desc @@ -3,9 +3,8 @@ main.c --cover location block 1 \(lines main.c:main:3,5\): SATISFIED block 2 \(lines main.c:main:6\): SATISFIED -block 3 \(lines main.c:main:6,9\): FAILED -block 4 \(lines main.c:main:8\): SATISFIED -block 5 \(lines main.c:main:9\): SATISFIED +block 3 \(lines main.c:main:8\): SATISFIED +block 4 \(lines main.c:main:9\): SATISFIED ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/cbmc-cover/built-ins1/test.desc b/regression/cbmc-cover/built-ins1/test.desc index d80a20e49ef..89ed6bb1617 100644 --- a/regression/cbmc-cover/built-ins1/test.desc +++ b/regression/cbmc-cover/built-ins1/test.desc @@ -3,7 +3,7 @@ main.c --cover location --unwind 1 ^EXIT=0$ ^SIGNAL=0$ -^\*\* 5 of 8 covered +^\*\* 5 of 7 covered -- ^warning: ignoring ^\[.*\/\/ [0-9]+ file main\.c line [0-9]+ function main)[\s]*DEAD .*newAlloc0[\s]*(?P>comment_block)[\s]*DEAD .*pc[\s]*(?P>comment_block)[\s]*DEAD .*literal[\s]*(?P>comment_block)[\s]*9: END_FUNCTION +(?P\/\/ [0-9]+ file main\.c line [0-9]+ function main)[\s]*DEAD .*newAlloc0[\s]*(?P>comment_block)[\s]*DEAD .*pc[\s]*(?P>comment_block)[\s]*DEAD .*literal[\s]*(?P>comment_block)[\s]*8: END_FUNCTION ^EXIT=0$ ^SIGNAL=0$ -- @@ -16,7 +16,7 @@ Checks for: // 51 file main.c line 44 function main DEAD main::$tmp::literal // 52 file main.c line 45 function main - 9: END_FUNCTION + 8: END_FUNCTION This asserts that when you've created a compound literal that both temp and real variable gets killed. diff --git a/regression/cbmc/destructors/enter_lexical_block.desc b/regression/cbmc/destructors/enter_lexical_block.desc index b088d95998f..ac1cf8d6eda 100644 --- a/regression/cbmc/destructors/enter_lexical_block.desc +++ b/regression/cbmc/destructors/enter_lexical_block.desc @@ -2,7 +2,7 @@ CORE new-smt-backend main.c --unwind 10 --show-goto-functions activate-multi-line-match -(?P\/\/ [0-9]+ file main\.c line [0-9]+ function main)[\s]*6: .*newAlloc4 : struct tag-test[\s]*(?P>comment_block)[\s]*.*newAlloc4 := \{ 4 \}[\s]*(?P>comment_block)[\s]*.*newAlloc6 : struct tag-test[\s]*(?P>comment_block)[\s]*.*newAlloc6 := \{ 6 \}[\s]*(?P>comment_block)[\s]*.*newAlloc7 : struct tag-test[\s]*(?P>comment_block)[\s]*.*newAlloc7 := \{ 7 \}[\s]*(?P>comment_block)[\s]*GOTO 3 +(?P\/\/ [0-9]+ file main\.c line [0-9]+ function main)[\s]*5: .*newAlloc4 : struct tag-test[\s]*(?P>comment_block)[\s]*.*newAlloc4 := \{ 4 \}[\s]*(?P>comment_block)[\s]*.*newAlloc6 : struct tag-test[\s]*(?P>comment_block)[\s]*.*newAlloc6 := \{ 6 \}[\s]*(?P>comment_block)[\s]*.*newAlloc7 : struct tag-test[\s]*(?P>comment_block)[\s]*.*newAlloc7 := \{ 7 \}[\s]*(?P>comment_block)[\s]*GOTO 3 ^EXIT=0$ ^SIGNAL=0$ -- @@ -10,7 +10,7 @@ activate-multi-line-match Checks for: // 37 file main.c line 36 function main - 6: DECL main::1::2::2::newAlloc4 : struct tag-test + 5: DECL main::1::2::2::newAlloc4 : struct tag-test // 38 file main.c line 36 function main ASSIGN main::1::2::2::newAlloc4 := { 4 } // 39 file main.c line 37 function main diff --git a/regression/cprover/loops/while-break1.desc b/regression/cprover/loops/while-break1.desc index 1f65f79fdb4..fb089d04d42 100644 --- a/regression/cprover/loops/while-break1.desc +++ b/regression/cprover/loops/while-break1.desc @@ -3,15 +3,15 @@ while-break1.c --text --solve --inline ^EXIT=0$ ^SIGNAL=0$ -^\(\d+\) ∀ ς : state \. S18\(ς\) ⇒ S12in\(ς\)$ +^\(\d+\) ∀ ς : state \. S15T\(ς\) ⇒ S12in\(ς\)$ ^\(\d+\) ∀ ς : state \. S11\(ς\) ⇒ S12in\(ς\)$ ^\(\d+\) ∀ ς : state \. \(S12in\(ς\) ∧ ¬\(1 ≠ 0\)\) ⇒ S12T\(ς\)$ ^\(\d+\) ∀ ς : state \. \(S12in\(ς\) ∧ 1 ≠ 0\) ⇒ S12\(ς\)$ -^\(\d+\) ∀ ς : state \. \(S12\(ς\) ∧ ¬\(ς\(❝main::1::x❞\) = 0\)\) ⇒ S13T\(ς\)$ -^\(\d+\) ∀ ς : state \. \(S12\(ς\) ∧ ς\(❝main::1::x❞\) = 0\) ⇒ S13\(ς\)$ -^\(\d+\) ∀ ς : state \. S12T\(ς\) ⇒ S19in\(ς\)$ -^\(\d+\) ∀ ς : state \. S14\(ς\) ⇒ S19in\(ς\)$ -^\(\d+\) ∀ ς : state \. S16\(ς\) ⇒ S19in\(ς\)$ +^\(\d+\) ∀ ς : state \. \(S12\(ς\) ∧ ς\(❝main::1::x❞\) = 0\) ⇒ S13T\(ς\)$ +^\(\d+\) ∀ ς : state \. \(S12\(ς\) ∧ ¬\(ς\(❝main::1::x❞\) = 0\)\) ⇒ S13\(ς\)$ +^\(\d+\) ∀ ς : state \. S12T\(ς\) ⇒ S17in\(ς\)$ +^\(\d+\) ∀ ς : state \. S13T\(ς\) ⇒ S17in\(ς\)$ +^\(\d+\) ∀ ς : state \. S16\(ς\) ⇒ S17in\(ς\)$ ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$ -- -- diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp index c9120bf28b8..172f1b3f0dc 100644 --- a/src/goto-programs/goto_convert.cpp +++ b/src/goto-programs/goto_convert.cpp @@ -1639,13 +1639,28 @@ void goto_convertt::generate_ifthenelse( dest.destructive_append(tmp_v); dest.destructive_append(tmp_w); + // When the `then` branch of a balanced `if` condition ends with a `return` or + // a `goto` statement, it is not necessary to add the `goto z` and `z:` goto + // elements as they are never used. + // This helps for example when using `--cover location` as such command are + // marked unreachable, but are not part of the user-provided code to analyze. + bool then_branch_returns = dest.instructions.rbegin()->is_goto(); + if(has_else) { - dest.destructive_append(tmp_x); + // Don't add the `goto` at the end of the `then` branch if not needed + if(!then_branch_returns) + { + dest.destructive_append(tmp_x); + } dest.destructive_append(tmp_y); } - dest.destructive_append(tmp_z); + // Don't add the `z` label at the end of the `if` when not needed. + if(!has_else || !then_branch_returns) + { + dest.destructive_append(tmp_z); + } } /// if(guard) goto target;