Also simplify assert structure found on alpine linux

Author: tautschnig

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);
       }
 

src/goto-programs/goto_convert.cpp

@@ -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;
@@ -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(