Skip to content

Commit

Permalink
Also simplify assert structure found on alpine linux
Browse files Browse the repository at this point in the history
  • Loading branch information
tautschnig committed Apr 15, 2018
1 parent c5cde18 commit d44bfd3
Show file tree
Hide file tree
Showing 2 changed files with 26 additions and 5 deletions.
10 changes: 8 additions & 2 deletions src/goto-programs/goto_clean_expr.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -260,13 +260,19 @@ void goto_convertt::clean_expr(
// preserve the expressions for possible later checks
if(if_expr.true_case().is_not_nil())
{
code_expressiont code_expression(if_expr.true_case());
// add a (void) type cast so that is_skip catches it in case the
// expression is just a constant
code_expressiont code_expression(
typecast_exprt(if_expr.true_case(), empty_typet()));
convert(code_expression, tmp_true);
}

if(if_expr.false_case().is_not_nil())
{
code_expressiont code_expression(if_expr.false_case());
// add a (void) type cast so that is_skip catches it in case the
// expression is just a constant
code_expressiont code_expression(
typecast_exprt(if_expr.false_case(), empty_typet()));
convert(code_expression, tmp_false);
}

Expand Down
21 changes: 18 additions & 3 deletions src/goto-programs/goto_convert.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -31,9 +31,7 @@ Author: Daniel Kroening, [email protected]
static bool is_empty(const goto_programt &goto_program)
{
forall_goto_program_instructions(it, goto_program)
if(!it->is_skip() ||
!it->labels.empty() ||
!it->code.is_nil())
if(!is_skip(goto_program, it))
return false;

return true;
Expand Down Expand Up @@ -1749,6 +1747,23 @@ void goto_convertt::generate_ifthenelse(
return;
}

// a special case for C libraries that use
// (void)((cond) || (assert(0),0))
if(
is_empty(false_case) && true_case.instructions.size() == 2 &&
true_case.instructions.front().is_assert() &&
true_case.instructions.front().guard.is_false() &&
true_case.instructions.front().labels.empty() &&
true_case.instructions.back().labels.empty())
{
true_case.instructions.front().guard = boolean_negate(guard);
true_case.instructions.erase(--true_case.instructions.end());
dest.destructive_append(true_case);
true_case.instructions.clear();

return;
}

// Flip around if no 'true' case code.
if(is_empty(true_case))
return generate_ifthenelse(
Expand Down

0 comments on commit d44bfd3

Please sign in to comment.