Skip to content

Commit 41c797a

Browse files
Do not generate redundant if statements in assert expansions
Fixes: diffblue#755
1 parent 70c1e61 commit 41c797a

File tree

3 files changed

+26
-0
lines changed

3 files changed

+26
-0
lines changed
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
#include <assert.h>
2+
3+
int main(int argc, char *argv[])
4+
{
5+
assert(0);
6+
return 0;
7+
}
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main.c
3+
--dump-c
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
--
7+
^warning: ignoring
8+
^[[:space:]]*IF

src/goto-programs/goto_convert.cpp

+11
Original file line numberDiff line numberDiff line change
@@ -26,6 +26,7 @@ Author: Daniel Kroening, [email protected]
2626

2727
#include "goto_convert_class.h"
2828
#include "destructor.h"
29+
#include "remove_skip.h"
2930

3031
static bool is_empty(const goto_programt &goto_program)
3132
{
@@ -1825,6 +1826,11 @@ void goto_convertt::generate_ifthenelse(
18251826
true_case.instructions.back().guard=boolean_negate(guard);
18261827
dest.destructive_append(true_case);
18271828
true_case.instructions.clear();
1829+
if(
1830+
is_empty(false_case) ||
1831+
(is_size_one(false_case) &&
1832+
is_skip(false_case, false_case.instructions.begin())))
1833+
return;
18281834
}
18291835

18301836
// similarly, do guarded assertions directly
@@ -1838,6 +1844,11 @@ void goto_convertt::generate_ifthenelse(
18381844
false_case.instructions.back().guard=guard;
18391845
dest.destructive_append(false_case);
18401846
false_case.instructions.clear();
1847+
if(
1848+
is_empty(true_case) ||
1849+
(is_size_one(true_case) &&
1850+
is_skip(true_case, true_case.instructions.begin())))
1851+
return;
18411852
}
18421853

18431854
// Flip around if no 'true' case code.

0 commit comments

Comments
 (0)