fixup! Replace assert(...) by macros from invariant.h

tautschnig · tautschnig · commit 25c4445d245e · 2022-03-25T14:36:47.000Z
diff --git a/src/ansi-c/c_typecheck_initializer.cpp b/src/ansi-c/c_typecheck_initializer.cpp
@@ -356,18 +356,18 @@ exprt::operandst::const_iterator c_typecheck_baset::do_designated_initializer(
   // copy the value, we may need to adjust it
   exprt value=*init_it;
 
-  assert(!designator.empty());
+  PRECONDITION(!designator.empty());
 
   if(value.id()==ID_designated_initializer)
   {
-    assert(value.operands().size()==1);
+    PRECONDITION(value.operands().size()==1);
 
     designator=
       make_designator(
         designator.front().type,
         static_cast<const exprt &>(value.find(ID_designator)));
 
-    assert(!designator.empty());
+    CHECK_RETURN(!designator.empty());
 
     // discard the return value
     do_designated_initializer(
@@ -587,7 +587,7 @@ exprt::operandst::const_iterator c_typecheck_baset::do_designated_initializer(
       else
         *dest=do_initializer_rec(value, type, force_constant);
 
-      assert(full_type==follow(dest->type()));
+      DATA_INVARIANT(full_type==follow(dest->type()), "matching types");
 
       return ++init_it; // done
     }
@@ -655,10 +655,10 @@ exprt::operandst::const_iterator c_typecheck_baset::do_designated_initializer(
       }
     }
 
-    assert(full_type.id()==ID_struct ||
+    DATA_INVARIANT(full_type.id()==ID_struct ||
            full_type.id()==ID_union ||
            full_type.id()==ID_array ||
-           full_type.id()==ID_vector);
+           full_type.id()==ID_vector, "full type must be composite");
 
     // we are initializing a compound type, and enter it!
     // this may change the type, full_type might not be valid any more
@@ -709,7 +709,7 @@ exprt::operandst::const_iterator c_typecheck_baset::do_designated_initializer(
 
 void c_typecheck_baset::increment_designator(designatort &designator)
 {
-  assert(!designator.empty());
+  PRECONDITION(!designator.empty());
 
   while(true)
   {
@@ -730,7 +730,7 @@ void c_typecheck_baset::increment_designator(designatort &designator)
         to_struct_type(full_type);
       const struct_typet::componentst &components=
         struct_type.components();
-      assert(components.size()==entry.size);
+      DATA_INVARIANT(components.size()==entry.size, "matching component numbers");
 
       // we skip over any padding or code
       // we also skip over anonymous members
@@ -757,15 +757,15 @@ void c_typecheck_baset::increment_designator(designatort &designator)
     // pop entry
     designator.pop_entry();
 
-    assert(!designator.empty());
+    INVARIANT(!designator.empty(), "designator had more than one entry");
   }
 }
 
 designatort c_typecheck_baset::make_designator(
   const typet &src_type,
   const exprt &src)
 {
-  assert(!src.operands().empty());
+  PRECONDITION(!src.operands().empty());
 
   typet type=src_type;
   designatort designator;
@@ -904,7 +904,7 @@ designatort c_typecheck_baset::make_designator(
     designator.push_entry(entry);
   }
 
-  assert(!designator.empty());
+  INVARIANT(!designator.empty(), "expected an entry to be added");
 
   return designator;
 }
@@ -914,7 +914,7 @@ exprt c_typecheck_baset::do_initializer_list(
   const typet &type,
   bool force_constant)
 {
-  assert(value.id()==ID_initializer_list);
+  PRECONDITION(value.id()==ID_initializer_list);
 
   const typet &full_type=follow(type);
 
diff --git a/src/cpp/cpp_instantiate_template.cpp b/src/cpp/cpp_instantiate_template.cpp
@@ -152,7 +152,7 @@ const symbolt &cpp_typecheckt::class_template_symbol(
   const cpp_template_args_tct &full_template_args)
 {
   // we should never get 'unassigned' here
-  assert(!full_template_args.has_unassigned());
+  PRECONDITION(!full_template_args.has_unassigned());
 
   // do we have args?
   if(full_template_args.arguments().empty())
@@ -283,8 +283,8 @@ const symbolt &cpp_typecheckt::instantiate_template(
   bool specialization_given=specialization.is_not_nil();
 
   // we should never get 'unassigned' here
-  assert(!specialization_template_args.has_unassigned());
-  assert(!full_template_args.has_unassigned());
+  DATA_INVARIANT(!specialization_template_args.has_unassigned(), "should never get 'unassigned' here");
+  DATA_INVARIANT(!full_template_args.has_unassigned(), "should never get 'unassigned' here");
 
 #ifdef DEBUG
   std::cout << "A: <";
@@ -368,8 +368,8 @@ const symbolt &cpp_typecheckt::instantiate_template(
       // It has already been instantiated!
       const cpp_idt &cpp_id = **id_set.begin();
 
-      assert(cpp_id.id_class == cpp_idt::id_classt::CLASS ||
-             cpp_id.id_class == cpp_idt::id_classt::SYMBOL);
+      DATA_INVARIANT(cpp_id.id_class == cpp_idt::id_classt::CLASS ||
+             cpp_id.id_class == cpp_idt::id_classt::SYMBOL, "id must be class or symbol");
 
       const symbolt &symb=lookup(cpp_id.identifier);
 
@@ -482,7 +482,7 @@ const symbolt &cpp_typecheckt::instantiate_template(
   {
     symbolt &symb = symbol_table.get_writeable_ref(class_name);
 
-    assert(new_decl.declarators().size() == 1);
+    PRECONDITION(new_decl.declarators().size() == 1);
 
     if(new_decl.member_spec().is_virtual())
     {
@@ -513,8 +513,8 @@ const symbolt &cpp_typecheckt::instantiate_template(
     bool is_static=new_decl.storage_spec().is_static();
     irep_idt access = new_decl.get(ID_C_access);
 
-    assert(!access.empty());
-    assert(symb.type.id()==ID_struct);
+    CHECK_RETURN(!access.empty());
+    PRECONDITION(symb.type.id()==ID_struct);
 
     typecheck_compound_declarator(
       symb,
@@ -532,7 +532,7 @@ const symbolt &cpp_typecheckt::instantiate_template(
   // not a class template, not a class template method,
   // it must be a function template!
 
-  assert(new_decl.declarators().size()==1);
+  PRECONDITION(new_decl.declarators().size()==1);
 
   convert_non_template_declaration(new_decl);
 
diff --git a/src/cpp/cpp_typecheck.cpp b/src/cpp/cpp_typecheck.cpp
@@ -67,11 +67,11 @@ const struct_typet &cpp_typecheckt::this_struct_type()
   const exprt &this_expr=
     cpp_scopes.current_scope().this_expr;
 
-  assert(this_expr.is_not_nil());
-  assert(this_expr.type().id()==ID_pointer);
+  CHECK_RETURN(this_expr.is_not_nil());
+  CHECK_RETURN(this_expr.type().id()==ID_pointer);
 
   const typet &t = follow(to_pointer_type(this_expr.type()).base_type());
-  assert(t.id()==ID_struct);
+  CHECK_RETURN(t.id()==ID_struct);
   return to_struct_type(t);
 }
 
@@ -164,9 +164,9 @@ void cpp_typecheckt::static_and_dynamic_initialization()
     if(cpp_is_pod(symbol.type))
       continue;
 
-    assert(symbol.is_static_lifetime);
-    assert(!symbol.is_type);
-    assert(symbol.type.id()!=ID_code);
+    DATA_INVARIANT(symbol.is_static_lifetime, "should be static");
+    DATA_INVARIANT(!symbol.is_type, "should not be a type");
+    DATA_INVARIANT(symbol.type.id()!=ID_code, "should not be code");
 
     exprt symbol_expr=cpp_symbol_expr(symbol);
 
@@ -228,7 +228,7 @@ void cpp_typecheckt::do_not_typechecked()
         symbol.value.id() == ID_cpp_not_typechecked &&
         symbol.value.get_bool(ID_is_used))
       {
-        assert(symbol.type.id()==ID_code);
+        DATA_INVARIANT(symbol.type.id()==ID_code, "must be code");
         exprt value = symbol.value;
 
         if(symbol.base_name=="operator=")
diff --git a/src/cpp/cpp_typecheck_compound_type.cpp b/src/cpp/cpp_typecheck_compound_type.cpp
@@ -312,7 +312,7 @@ void cpp_typecheckt::typecheck_compound_declarator(
 
   if(is_cast_operator)
   {
-    assert(declarator.name().get_sub().size()==2 &&
+    PRECONDITION(declarator.name().get_sub().size()==2 &&
            declarator.name().get_sub().front().id()==ID_operator);
 
     typet type=static_cast<typet &>(declarator.name().get_sub()[1]);
@@ -522,9 +522,9 @@ void cpp_typecheckt::typecheck_compound_declarator(
         {
           is_virtual=true;
           const code_typet &code_type=to_code_type(comp.type());
-          assert(!code_type.parameters().empty());
+          DATA_INVARIANT(!code_type.parameters().empty(), "must have parameters");
           const typet &pointer_type=code_type.parameters()[0].type();
-          assert(pointer_type.id()==ID_pointer);
+          DATA_INVARIANT(pointer_type.id()==ID_pointer, "this must be pointer");
           virtual_bases.insert(
             to_pointer_type(pointer_type).base_type().get(ID_identifier));
         }
@@ -951,7 +951,7 @@ void cpp_typecheckt::typecheck_compound_body(symbolt &symbol)
   // enter scope of compound
   cpp_scopes.set_scope(symbol.name);
 
-  assert(symbol.type.id()==ID_struct ||
+  PRECONDITION(symbol.type.id()==ID_struct ||
          symbol.type.id()==ID_union);
 
   struct_union_typet &type=
@@ -1195,7 +1195,7 @@ void cpp_typecheckt::typecheck_compound_body(symbolt &symbol)
       // build declaration
       cpp_declarationt cpctor;
       default_cpctor(symbol, cpctor);
-      assert(cpctor.declarators().size()==1);
+      CHECK_RETURN(cpctor.declarators().size()==1);
 
       exprt value(ID_cpp_not_typechecked);
       value.copy_to_operands(cpctor.declarators()[0].value());
@@ -1213,7 +1213,7 @@ void cpp_typecheckt::typecheck_compound_body(symbolt &symbol)
       // build declaration
       cpp_declarationt assignop;
       default_assignop(symbol, assignop);
-      assert(assignop.declarators().size()==1);
+      CHECK_RETURN(assignop.declarators().size()==1);
 
       // The value will be typechecked only if the operator
       // is actually used
@@ -1497,7 +1497,7 @@ bool cpp_typecheckt::get_component(
 {
   const typet &followed_type=follow(object.type());
 
-  assert(followed_type.id()==ID_struct ||
+  PRECONDITION(followed_type.id()==ID_struct ||
          followed_type.id()==ID_union);
 
   struct_union_typet final_type=
@@ -1599,7 +1599,7 @@ bool cpp_typecheckt::check_component_access(
   if(access==ID_public)
     return false; // ok
 
-  assert(access==ID_private ||
+  PRECONDITION(access==ID_private ||
          access==ID_protected);
 
   const irep_idt &struct_identifier=
@@ -1703,8 +1703,8 @@ void cpp_typecheckt::make_ptr_typecast(
 {
   typet src_type=expr.type();
 
-  assert(src_type.id()==  ID_pointer);
-  assert(dest_type.id()== ID_pointer);
+  PRECONDITION(src_type.id()==  ID_pointer);
+  PRECONDITION(dest_type.id()== ID_pointer);
 
   const struct_typet &src_struct = to_struct_type(
     static_cast<const typet &>(follow(to_pointer_type(src_type).base_type())));
diff --git a/src/cpp/cpp_typecheck_conversions.cpp b/src/cpp/cpp_typecheck_conversions.cpp
@@ -49,7 +49,7 @@ bool cpp_typecheckt::standard_conversion_lvalue_to_rvalue(
   const exprt &expr,
   exprt &new_expr) const
 {
-  assert(expr.get_bool(ID_C_lvalue));
+  PRECONDITION(expr.get_bool(ID_C_lvalue));
 
   if(expr.type().id() == ID_code)
     return false;
@@ -80,7 +80,7 @@ bool cpp_typecheckt::standard_conversion_array_to_pointer(
   const exprt &expr,
   exprt &new_expr) const
 {
-  assert(expr.type().id()==ID_array);
+  PRECONDITION(expr.type().id()==ID_array);
 
   index_exprt index(expr, from_integer(0, c_index_type()));
 
@@ -577,13 +577,13 @@ bool cpp_typecheckt::standard_conversion_pointer_to_member(
       to_pointer_type(expr.type()).base_type().id() == ID_code)
     {
       code_typet code1=to_code_type(expr.type().subtype());
-      assert(!code1.parameters().empty());
+      DATA_INVARIANT(!code1.parameters().empty(), "must have parameters");
       code_typet::parametert this1=code1.parameters()[0];
       INVARIANT(this1.get_this(), "first parameter should be `this'");
       code1.parameters().erase(code1.parameters().begin());
 
       code_typet code2=to_code_type(type.subtype());
-      assert(!code2.parameters().empty());
+      DATA_INVARIANT(!code2.parameters().empty(), "must have parameters");
       code_typet::parametert this2=code2.parameters()[0];
       INVARIANT(this2.get_this(), "first parameter should be `this'");
       code2.parameters().erase(code2.parameters().begin());
@@ -683,7 +683,7 @@ bool cpp_typecheckt::standard_conversion_sequence(
   exprt &new_expr,
   unsigned &rank)
 {
-  assert(!is_reference(expr.type()) && !is_reference(type));
+  PRECONDITION(!is_reference(expr.type()) && !is_reference(type));
 
   exprt curr_expr=expr;
 
@@ -859,8 +859,8 @@ bool cpp_typecheckt::user_defined_conversion_sequence(
   exprt &new_expr,
   unsigned &rank)
 {
-  assert(!is_reference(expr.type()));
-  assert(!is_reference(type));
+  PRECONDITION(!is_reference(expr.type()));
+  PRECONDITION(!is_reference(type));
 
   const typet &from=follow(expr.type());
   const typet &to=follow(type);
@@ -982,9 +982,9 @@ bool cpp_typecheckt::user_defined_conversion_sequence(
                 uninitialized_typet{},
                 expr.source_location());
               typecheck_side_effect_function_call(ctor_expr);
+              CHECK_RETURN(ctor_expr.get(ID_statement)==ID_temporary_object);
 
               new_expr.swap(ctor_expr);
-              assert(new_expr.get(ID_statement)==ID_temporary_object);
 
               if(to.get_bool(ID_C_constant))
                 new_expr.type().set(ID_C_constant, true);
@@ -1116,8 +1116,8 @@ bool cpp_typecheckt::reference_related(
   const exprt &expr,
   const typet &type) const
 {
-  assert(is_reference(type));
-  assert(!is_reference(expr.type()));
+  PRECONDITION(is_reference(type));
+  PRECONDITION(!is_reference(expr.type()));
 
   typet from=follow(expr.type());
   typet to=follow(type.subtype());
@@ -1154,8 +1154,8 @@ bool cpp_typecheckt::reference_compatible(
   const typet &type,
   unsigned &rank) const
 {
-  assert(is_reference(type));
-  assert(!is_reference(expr.type()));
+  PRECONDITION(is_reference(type));
+  PRECONDITION(!is_reference(expr.type()));
 
   if(!reference_related(expr, type))
     return false;
@@ -1218,8 +1218,8 @@ bool cpp_typecheckt::reference_binding(
   exprt &new_expr,
   unsigned &rank)
 {
-  assert(is_reference(type));
-  assert(!is_reference(expr.type()));
+  PRECONDITION(is_reference(type));
+  PRECONDITION(!is_reference(expr.type()));
 
   unsigned backup_rank=rank;
 
@@ -1298,7 +1298,7 @@ bool cpp_typecheckt::reference_binding(
       if(!is_reference(component_type.return_type()))
         continue;
 
-      assert(component_type.parameters().size()==1);
+      DATA_INVARIANT(component_type.parameters().size()==1, "exactly one parameter");
 
       typet this_type =
         component_type.parameters().front().type();
@@ -1552,7 +1552,7 @@ void cpp_typecheckt::reference_initializer(
   exprt &expr,
   const typet &type)
 {
-  assert(is_reference(type));
+  PRECONDITION(is_reference(type));
   add_implicit_dereference(expr);
 
   unsigned rank=0;
@@ -1572,7 +1572,7 @@ bool cpp_typecheckt::cast_away_constness(
   const typet &t1,
   const typet &t2) const
 {
-  assert(t1.id()==ID_pointer && t2.id()==ID_pointer);
+  PRECONDITION(t1.id()==ID_pointer && t2.id()==ID_pointer);
   typet nt1=t1;
   typet nt2=t2;
 
diff --git a/src/cpp/cpp_typecheck_expr.cpp b/src/cpp/cpp_typecheck_expr.cpp
