Skip to content

Commit c5cde18

Browse files
committed
Do not generate redundant if statements in assert expansions
Fixes: #755
1 parent 4fb0603 commit c5cde18

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
{
@@ -1723,6 +1724,11 @@ void goto_convertt::generate_ifthenelse(
17231724
true_case.instructions.back().guard=boolean_negate(guard);
17241725
dest.destructive_append(true_case);
17251726
true_case.instructions.clear();
1727+
if(
1728+
is_empty(false_case) ||
1729+
(is_size_one(false_case) &&
1730+
is_skip(false_case, false_case.instructions.begin())))
1731+
return;
17261732
}
17271733

17281734
// similarly, do guarded assertions directly
@@ -1736,6 +1742,11 @@ void goto_convertt::generate_ifthenelse(
17361742
false_case.instructions.back().guard=guard;
17371743
dest.destructive_append(false_case);
17381744
false_case.instructions.clear();
1745+
if(
1746+
is_empty(true_case) ||
1747+
(is_size_one(true_case) &&
1748+
is_skip(true_case, true_case.instructions.begin())))
1749+
return;
17391750
}
17401751

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

0 commit comments

Comments
 (0)