diff --git a/regression/cbmc/simple_assert/main.c b/regression/cbmc/simple_assert/main.c new file mode 100644 index 00000000000..14c6fc0f682 --- /dev/null +++ b/regression/cbmc/simple_assert/main.c @@ -0,0 +1,9 @@ +#include + +int main(int argc, char *argv[]) +{ + int x = 5; + assert(x == 5); + + return 0; +} diff --git a/regression/cbmc/simple_assert/test.desc b/regression/cbmc/simple_assert/test.desc new file mode 100644 index 00000000000..57c877afe23 --- /dev/null +++ b/regression/cbmc/simple_assert/test.desc @@ -0,0 +1,13 @@ +CORE +main.c +--cover location +^EXIT=0$ +^SIGNAL=0$ +^\[main\.coverage\.1\] .* function main block 1: SATISFIED$ +(1 of 1|3 of 3) covered \(100\.0%\)$ +-- +^warning: ignoring +^CONVERSION ERROR$ +^\[main\.coverage\..\] .* function main block .: FAILED$ +-- +On Windows/Visual Studio, "assert" does not introduce any branching. diff --git a/regression/goto-instrument/assert1/main.c b/regression/goto-instrument/assert1/main.c new file mode 100644 index 00000000000..e9cf26ef226 --- /dev/null +++ b/regression/goto-instrument/assert1/main.c @@ -0,0 +1,7 @@ +#include + +int main(int argc, char *argv[]) +{ + assert(0); + return 0; +} diff --git a/regression/goto-instrument/assert1/test.desc b/regression/goto-instrument/assert1/test.desc new file mode 100644 index 00000000000..c2d2fa95ee8 --- /dev/null +++ b/regression/goto-instrument/assert1/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--dump-c +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring +^[[:space:]]*IF diff --git a/src/goto-programs/goto_clean_expr.cpp b/src/goto-programs/goto_clean_expr.cpp index ad5fea6ac5f..8c82a34a582 100644 --- a/src/goto-programs/goto_clean_expr.cpp +++ b/src/goto-programs/goto_clean_expr.cpp @@ -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); } diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp index 7f8095c2a05..2bca47c7723 100644 --- a/src/goto-programs/goto_convert.cpp +++ b/src/goto-programs/goto_convert.cpp @@ -26,13 +26,12 @@ Author: Daniel Kroening, kroening@kroening.com #include "goto_convert_class.h" #include "destructor.h" +#include "remove_skip.h" 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; @@ -1723,6 +1722,11 @@ void goto_convertt::generate_ifthenelse( true_case.instructions.back().guard=boolean_negate(guard); dest.destructive_append(true_case); true_case.instructions.clear(); + if( + is_empty(false_case) || + (is_size_one(false_case) && + is_skip(false_case, false_case.instructions.begin()))) + return; } // similarly, do guarded assertions directly @@ -1736,6 +1740,28 @@ void goto_convertt::generate_ifthenelse( false_case.instructions.back().guard=guard; dest.destructive_append(false_case); false_case.instructions.clear(); + if( + is_empty(true_case) || + (is_size_one(true_case) && + is_skip(true_case, true_case.instructions.begin()))) + 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. diff --git a/src/goto-programs/remove_skip.cpp b/src/goto-programs/remove_skip.cpp index 4ce2a74fb04..a41bb59aa26 100644 --- a/src/goto-programs/remove_skip.cpp +++ b/src/goto-programs/remove_skip.cpp @@ -12,7 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "remove_skip.h" #include "goto_model.h" -static bool is_skip(goto_programt::instructionst::iterator it) +bool is_skip(const goto_programt &body, goto_programt::const_targett it) { // we won't remove labelled statements // (think about error labels or the like) @@ -28,9 +28,12 @@ static bool is_skip(goto_programt::instructionst::iterator it) if(it->guard.is_false()) return true; - goto_programt::instructionst::iterator next_it=it; + goto_programt::const_targett next_it = it; next_it++; + if(next_it == body.instructions.end()) + return false; + // A branch to the next instruction is a skip // We also require the guard to be 'true' return it->guard.is_true() && @@ -92,7 +95,7 @@ void remove_skip(goto_programt &goto_program) // for collecting labels std::list labels; - while(is_skip(it)) + while(is_skip(goto_program, it)) { // don't remove the last skip statement, // it could be a target @@ -144,9 +147,10 @@ void remove_skip(goto_programt &goto_program) // remove the last skip statement unless it's a target goto_program.compute_incoming_edges(); - if(!goto_program.instructions.empty() && - is_skip(--goto_program.instructions.end()) && - !goto_program.instructions.back().is_target()) + if( + !goto_program.instructions.empty() && + is_skip(goto_program, --goto_program.instructions.end()) && + !goto_program.instructions.back().is_target()) goto_program.instructions.pop_back(); } while(goto_program.instructions.size()