replace assert(false) by UNREACHABLE

src/analyses/constant_propagator.cpp

@@ -79,7 +79,7 @@ void constant_propagator_domaint::assign_rec(
         cond = simplify_expr(cond,ns);
       }
       else
-        assert(0);
+        UNREACHABLE;
 
       assign(values, to_symbol_expr(lhs), cond, ns);
 	}

src/analyses/custom_bitvector_analysis.cpp

@@ -296,7 +296,7 @@ void custom_bitvector_domaint::transform(
             else if(identifier=="__CPROVER_clear_may")
               mode=modet::CLEAR_MAY;
             else
-              assert(false);
+              UNREACHABLE;
 
             exprt lhs=code_function_call.arguments()[0];
 
@@ -411,7 +411,7 @@ void custom_bitvector_domaint::transform(
         else if(statement=="clear_may")
           mode=modet::CLEAR_MAY;
         else
-          assert(false);
+          UNREACHABLE;
 
         exprt lhs=instruction.code.op0();
 

src/analyses/goto_check.cpp

@@ -833,7 +833,7 @@ void goto_checkt::nan_check(
           equal_exprt(expr.op1(), minus_inf)));
   }
   else
-    assert(false);
+    UNREACHABLE;
 
   isnan.make_not();
 

src/analyses/goto_rw.cpp

@@ -713,7 +713,7 @@ void goto_rw(goto_programt::const_targett target,
   switch(target->type)
   {
   case NO_INSTRUCTION_TYPE:
-    assert(false);
+    UNREACHABLE;
     break;
 
   case GOTO:

src/analyses/invariant_set.cpp

@@ -474,7 +474,7 @@ void invariant_sett::strengthen_rec(const exprt &expr)
       }
     }
     else
-      assert(false);
+      UNREACHABLE;
   }
   else if(expr.id()==ID_equal)
   {
@@ -673,7 +673,7 @@ tvt invariant_sett::implies_rec(const exprt &expr) const
     else if(expr.id()==ID_notequal)
       return is_ne(p);
     else
-      assert(false);
+      UNREACHABLE;
   }
 
   return tvt::unknown();

src/ansi-c/ansi_c_convert_type.cpp

@@ -460,7 +460,7 @@ void ansi_c_convert_typet::write(typet &type)
         else
           type=unsigned_long_long_int_type();
       else
-        assert(false);
+        UNREACHABLE;
     }
     else if(gcc_int128_cnt)
     {

src/ansi-c/ansi_c_declaration.cpp

@@ -16,6 +16,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/config.h>
 #include <util/std_types.h>
+#include <util/invariant.h>
 
 void ansi_c_declaratort::build(irept &src)
 {
@@ -36,7 +37,7 @@ void ansi_c_declaratort::build(irept &src)
     else if(t.id().empty() ||
             t.is_nil())
     {
-      assert(0);
+      UNREACHABLE;
     }
     else if(t.id()==ID_abstract)
     {
@@ -108,7 +109,7 @@ typet ansi_c_declarationt::full_type(
       p=&(p->subtypes().back());
     }
     else
-      assert(false);
+      UNREACHABLE;
   }
 
   *p=type();

src/ansi-c/ansi_c_entry_point.cpp

@@ -305,7 +305,7 @@ bool ansi_c_entry_point(
           max=to_unsignedbv_type(envp_size_symbol.type).largest();
         }
         else
-          assert(false);
+          UNREACHABLE;
 
         exprt max_minus_one=from_integer(max-1, envp_size_symbol.type);
 
@@ -431,7 +431,7 @@ bool ansi_c_entry_point(
       }
     }
     else
-      assert(false);
+      UNREACHABLE;
   }
   else
   {

src/ansi-c/c_preprocess.cpp

@@ -106,7 +106,7 @@ static std::string type_max(const typet &src)
     return integer2string(
       power(2, to_unsignedbv_type(src).get_width()-1)-1);
   else
-    assert(false);
+    UNREACHABLE;
 }
 
 /// quote a string for bash and CMD
@@ -766,7 +766,7 @@ bool c_preprocess_gcc_clang(
     else if(config.ansi_c.wchar_t_width==config.ansi_c.char_width)
       command+=" -D__WCHAR_TYPE__=\""+sig+" char\"";
     else
-      assert(false);
+      UNREACHABLE;
   }
 
   if(config.ansi_c.char_is_unsigned)
@@ -804,7 +804,7 @@ bool c_preprocess_gcc_clang(
     break;
 
   default:
-    assert(false);
+    UNREACHABLE;
   }
 
   // Standard Defines, ANSI9899 6.10.8

src/ansi-c/c_typecast.cpp

@@ -378,11 +378,11 @@ void c_typecastt::implicit_typecast_arithmetic(
     }
     return;
 
-  case BOOL:       assert(false); // should always be promoted to int
-  case CHAR:       assert(false); // should always be promoted to int
-  case UCHAR:      assert(false); // should always be promoted to int
-  case SHORT:      assert(false); // should always be promoted to int
-  case USHORT:     assert(false); // should always be promoted to int
+  case BOOL:       UNREACHABLE; // should always be promoted to int
+  case CHAR:       UNREACHABLE; // should always be promoted to int
+  case UCHAR:      UNREACHABLE; // should always be promoted to int
+  case SHORT:      UNREACHABLE; // should always be promoted to int
+  case USHORT:     UNREACHABLE; // should always be promoted to int
   case INT:        new_type=signed_int_type(); break;
   case UINT:       new_type=unsigned_int_type(); break;
   case LONG:       new_type=signed_long_int_type(); break;

src/ansi-c/c_typecheck_expr.cpp

@@ -77,7 +77,7 @@ void c_typecheck_baset::add_rounding_mode(exprt &expr)
       else if(expr.id()==ID_minus)
         expr.id(ID_floatbv_minus);
       else
-        assert(false);
+        UNREACHABLE;
 
       expr.op2()=from_integer(0, unsigned_int_type());
     }
@@ -875,7 +875,7 @@ void c_typecheck_baset::typecheck_side_effect_statement_expression(
   else if(last_statement==ID_function_call)
   {
     // this is suspected to be dead
-    assert(false);
+    UNREACHABLE;
 
     // make the last statement an expression
 
@@ -2852,7 +2852,7 @@ void c_typecheck_baset::typecheck_expr_binary_arithmetic(exprt &expr)
         else if(expr.id()==ID_bitxor)
           expr.id(ID_xor);
         else
-          assert(false);
+          UNREACHABLE;
         expr.type()=type0;
         return;
       }
@@ -3010,7 +3010,7 @@ void c_typecheck_baset::typecheck_expr_pointer_arithmetic(exprt &expr)
     else
     {
       p_op=int_op=nullptr;
-      assert(false);
+      UNREACHABLE;
     }
 
     const typet &int_op_type=follow(int_op->type());

src/ansi-c/c_typecheck_initializer.cpp

@@ -344,7 +344,7 @@ void c_typecheck_baset::designator_enter(
     entry.subtype=vector_type.subtype();
   }
   else
-    assert(false);
+    UNREACHABLE;
 
   designator.push_entry(entry);
 }
@@ -478,7 +478,7 @@ exprt::operandst::const_iterator c_typecheck_baset::do_designated_initializer(
       dest=&(dest->op0());
     }
     else
-      assert(false);
+      UNREACHABLE;
   }
 
   // second phase: assign value

src/ansi-c/c_typecheck_type.cpp

@@ -380,7 +380,7 @@ void c_typecheck_baset::typecheck_custom_type(typet &type)
     type.set(ID_f, integer2string(f_int));
   }
   else
-    assert(false);
+    UNREACHABLE;
 }
 
 void c_typecheck_baset::typecheck_code_type(code_typet &type)
@@ -759,7 +759,7 @@ void c_typecheck_baset::typecheck_compound_type(struct_union_typet &type)
       else if(compound_symbol.type.id()==ID_union)
         compound_symbol.type.id(ID_incomplete_union);
       else
-        assert(false);
+        UNREACHABLE;
 
       symbolt *new_symbol;
       move_symbol(compound_symbol, new_symbol);

src/ansi-c/expr2c.cpp

@@ -114,7 +114,7 @@ void expr2ct::get_shorthands(const exprt &expr)
     ns_collision[symbol->location.get_function()].insert(sh);
 
     if(!shorthands.insert(std::make_pair(*it, sh)).second)
-      assert(false);
+      UNREACHABLE;
   }
 
   for(find_symbols_sett::const_iterator

src/cbmc/all_properties_class.h

@@ -56,7 +56,7 @@ class bmc_all_propertiest:
       }
 
       // make some poor compilers happy
-      assert(false);
+      UNREACHABLE;
       return "";
     }
 

src/cbmc/counterexample_beautification.cpp

@@ -74,7 +74,7 @@ counterexample_beautificationt::get_failed_property(
        prop_conv.l_get(it->cond_literal).is_false())
       return it;
 
-  assert(false);
+  UNREACHABLE;
   return equation.SSA_steps.end();
 }
 

src/cbmc/fault_localization.cpp

@@ -73,7 +73,7 @@ fault_localizationt::get_failed_property()
        bmc.prop_conv.l_get(it->cond_literal).is_false())
       return it;
 
-  assert(false);
+  UNREACHABLE;
   return bmc.equation.SSA_steps.end();
 }
 

src/cbmc/symex_coverage.cpp

@@ -247,7 +247,7 @@ void goto_program_coverage_recordt::compute_coverage_lines(
       branches_total+=2;
       if(!entry.first->second.conditions.insert(
           {it, coverage_conditiont()}).second)
-        assert(false);
+        UNREACHABLE;
     }
 
     symex_coveraget::coveraget::const_iterator c_entry=

src/clobber/clobber_parse_options.cpp

@@ -433,7 +433,7 @@ void clobber_parse_optionst::report_success()
     break;
 
   default:
-    assert(false);
+    UNREACHABLE;
   }
 }
 
@@ -458,7 +458,7 @@ void clobber_parse_optionst::show_counterexample(
     break;
 
   default:
-    assert(false);
+    UNREACHABLE;
   }
 }
 
@@ -481,7 +481,7 @@ void clobber_parse_optionst::report_failure()
     break;
 
   default:
-    assert(false);
+    UNREACHABLE;
   }
 }
 

src/cpp/cpp_constructor.cpp

@@ -183,7 +183,7 @@ codet cpp_typecheckt::cpp_constructor(
   }
   else if(tmp_type.id()==ID_union)
   {
-    assert(0); // Todo: union
+    UNREACHABLE; // Todo: union
   }
   else if(tmp_type.id()==ID_struct)
   {
@@ -301,7 +301,7 @@ codet cpp_typecheckt::cpp_constructor(
     }
   }
   else
-    assert(false);
+    UNREACHABLE;
 
   codet nil;
   nil.make_nil();

src/cpp/cpp_convert_type.cpp

@@ -13,11 +13,11 @@ Author: Daniel Kroening, [email protected]
 
 #include <cassert>
 
-#include <util/config.h>
 #include <util/arith_tools.h>
-#include <util/std_types.h>
-
 #include <util/c_types.h>
+#include <util/config.h>
+#include <util/invariant.h>
+#include <util/std_types.h>
 
 #include "cpp_declaration.h"
 #include "cpp_name.h"
@@ -285,7 +285,7 @@ void cpp_convert_typet::read_function_type(const typet &type)
       throw "ellipsis only allowed as last parameter";
     }
     else
-      assert(false);
+      UNREACHABLE;
   }
 
   // if we just have one parameter of type void, remove it

src/cpp/cpp_declarator_converter.cpp

@@ -91,7 +91,7 @@ symbolt &cpp_declarator_convertert::convert(
     // adjust template type
     if(final_type.id()==ID_template)
     {
-      assert(0);
+      UNREACHABLE;
       typet tmp;
       tmp.swap(final_type.subtype());
       final_type.swap(tmp);

src/cpp/cpp_scope.cpp

@@ -20,7 +20,7 @@ std::ostream &operator << (std::ostream &out, cpp_scopet::lookup_kindt kind)
   case cpp_scopet::QUALIFIED: return out << "QUALIFIED";
   case cpp_scopet::SCOPE_ONLY: return out << "SCOPE_ONLY";
   case cpp_scopet::RECURSIVE: return out << "RECURSIVE";
-  default: assert(false);
+  default: UNREACHABLE;
   }
 
   return out;

src/cpp/cpp_typecheck.cpp

@@ -250,7 +250,7 @@ void cpp_typecheckt::do_not_typechecked()
           cont=true;
         }
         else
-          assert(0); // Don't know what to do!
+          UNREACHABLE; // Don't know what to do!
       }
     }
   }

src/cpp/cpp_typecheck.h

@@ -380,7 +380,7 @@ class cpp_typecheckt:public c_typecheck_baset
 
   void put_compound_into_scope(const struct_union_typet::componentt &component);
   void typecheck_compound_body(symbolt &symbol);
-  void typecheck_compound_body(struct_union_typet &type) { assert(false); }
+  void typecheck_compound_body(struct_union_typet &type) { UNREACHABLE; }
   void typecheck_enum_body(symbolt &symbol);
   void typecheck_method_bodies(method_bodiest &);
   void typecheck_compound_bases(struct_typet &type);

src/cpp/cpp_typecheck_bases.cpp

@@ -209,7 +209,7 @@ void cpp_typecheckt::add_base_components(
         component.set_access(ID_private);
     }
     else
-      assert(false);
+      UNREACHABLE;
 
     // put into scope
   }

src/cpp/cpp_typecheck_conversions.cpp

@@ -1750,7 +1750,7 @@ bool cpp_typecheckt::dynamic_typecast(
     {
       if(!e.get_bool(ID_C_lvalue))
         return false;
-      assert(0); // currently not supported
+      UNREACHABLE; // currently not supported
     }
     else if(follow(type.subtype()).id()==ID_struct)
     {