Replace assert(...) by macros from invariant.h [blocks: #6749]

jbmc/src/java_bytecode/character_refine_preprocess.cpp

@@ -29,7 +29,7 @@ codet character_refine_preprocesst::convert_char_function(
   conversion_inputt &target)
 {
   const code_function_callt &function_call=target;
-  assert(function_call.arguments().size()==1);
+  PRECONDITION(function_call.arguments().size() == 1);
   const exprt &arg=function_call.arguments()[0];
   const exprt &result=function_call.lhs();
   const typet &type=result.type();
@@ -113,7 +113,7 @@ codet character_refine_preprocesst::convert_char_value(
 codet character_refine_preprocesst::convert_compare(conversion_inputt &target)
 {
   const code_function_callt &function_call=target;
-  assert(function_call.arguments().size()==2);
+  PRECONDITION(function_call.arguments().size() == 2);
   const exprt &char1=function_call.arguments()[0];
   const exprt &char2=function_call.arguments()[1];
   const exprt &result=function_call.lhs();
@@ -225,7 +225,7 @@ codet character_refine_preprocesst::convert_digit_int(conversion_inputt &target)
 codet character_refine_preprocesst::convert_for_digit(conversion_inputt &target)
 {
   const code_function_callt &function_call=target;
-  assert(function_call.arguments().size()==2);
+  PRECONDITION(function_call.arguments().size() == 2);
   const exprt &digit=function_call.arguments()[0];
   const exprt &result=function_call.lhs();
   const typet &type=result.type();
@@ -588,7 +588,7 @@ codet character_refine_preprocesst::convert_is_ideographic(
   conversion_inputt &target)
 {
   const code_function_callt &function_call=target;
-  assert(function_call.arguments().size()==1);
+  PRECONDITION(function_call.arguments().size() == 1);
   const exprt &arg=function_call.arguments()[0];
   const exprt &result=function_call.lhs();
   exprt is_ideograph=in_interval_expr(arg, 0x4E00, 0x9FFF);
@@ -602,7 +602,7 @@ codet character_refine_preprocesst::convert_is_ISO_control_char(
   conversion_inputt &target)
 {
   const code_function_callt &function_call=target;
-  assert(function_call.arguments().size()==1);
+  PRECONDITION(function_call.arguments().size() == 1);
   const exprt &arg=function_call.arguments()[0];
   const exprt &result=function_call.lhs();
   or_exprt iso(
@@ -760,7 +760,7 @@ codet character_refine_preprocesst::convert_is_low_surrogate(
   conversion_inputt &target)
 {
   const code_function_callt &function_call=target;
-  assert(function_call.arguments().size()==1);
+  PRECONDITION(function_call.arguments().size() == 1);
   const exprt &arg=function_call.arguments()[0];
   const exprt &result=function_call.lhs();
   exprt is_low_surrogate=in_interval_expr(arg, 0xDC00, 0xDFFF);
@@ -897,7 +897,7 @@ codet character_refine_preprocesst::convert_is_surrogate_pair(
   conversion_inputt &target)
 {
   const code_function_callt &function_call=target;
-  assert(function_call.arguments().size()==2);
+  PRECONDITION(function_call.arguments().size() == 2);
   const exprt &arg0=function_call.arguments()[0];
   const exprt &arg1=function_call.arguments()[1];
   const exprt &result=function_call.lhs();

jbmc/src/java_bytecode/expr2java.cpp

@@ -117,7 +117,9 @@ std::string expr2javat::convert_struct(
   const struct_typet::componentst &components=
     struct_type.components();
 
-  assert(components.size()==src.operands().size());
+  DATA_INVARIANT(
+    components.size() == src.operands().size(),
+    "inconsistent number of components");
 
   exprt::operandst::const_iterator o_it=src.operands().begin();
 

jbmc/src/java_bytecode/java_bytecode_convert_class.cpp

@@ -763,8 +763,8 @@ void java_bytecode_convert_classt::convert(
     if(s_it!=symbol_table.symbols.end())
       symbol_table.erase(s_it); // erase, we stubbed it
 
-    if(symbol_table.add(new_symbol))
-      assert(false && "failed to add static field symbol");
+    const bool failed = symbol_table.add(new_symbol);
+    CHECK_RETURN_WITH_DIAGNOSTICS(!failed, "failed to add static field symbol");
   }
   else
   {

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -773,20 +773,20 @@ code_blockt &java_bytecode_convert_methodt::get_or_create_block_for_pcrange(
   bool allow_merge)
 {
   // Check the tree shape invariant:
-  assert(tree.branch.size()==tree.branch_addresses.size());
+  PRECONDITION(tree.branch.size() == tree.branch_addresses.size());
 
   // If there are no child blocks, return this.
   if(tree.leaf)
     return this_block;
-  assert(!tree.branch.empty());
+  PRECONDITION(!tree.branch.empty());
 
   // Find child block starting > address_start:
   const auto afterstart=
     std::upper_bound(
       tree.branch_addresses.begin(),
       tree.branch_addresses.end(),
       address_start);
-  assert(afterstart!=tree.branch_addresses.begin());
+  CHECK_RETURN(afterstart != tree.branch_addresses.begin());
   auto findstart=afterstart;
   --findstart;
   auto child_offset=
@@ -814,9 +814,9 @@ code_blockt &java_bytecode_convert_methodt::get_or_create_block_for_pcrange(
   while(child_iter != this_block.statements().end() &&
         child_iter->get_statement() == ID_decl)
     ++child_iter;
-  assert(child_iter != this_block.statements().end());
+  CHECK_RETURN(child_iter != this_block.statements().end());
   std::advance(child_iter, child_offset);
-  assert(child_iter != this_block.statements().end());
+  CHECK_RETURN(child_iter != this_block.statements().end());
   auto &child_label=to_code_label(*child_iter);
   auto &child_block=to_code_block(child_label.code());
 
@@ -848,7 +848,7 @@ code_blockt &java_bytecode_convert_methodt::get_or_create_block_for_pcrange(
   // Check for incoming control-flow edges targeting non-header
   // blocks of the new proposed block range:
   auto checkit=amap.find(*findstart);
-  assert(checkit!=amap.end());
+  CHECK_RETURN(checkit != amap.end());
   ++checkit; // Skip the header, which can have incoming edges from outside.
   for(;
       checkit!=amap.end() && (checkit->first)<(findlim_block_start_address);
@@ -880,15 +880,15 @@ code_blockt &java_bytecode_convert_methodt::get_or_create_block_for_pcrange(
   code_labelt newlabel(child_label_name, code_blockt());
   code_blockt &newblock=to_code_block(newlabel.code());
   auto nblocks=std::distance(findstart, findlim);
-  assert(nblocks>=2);
+  CHECK_RETURN(nblocks >= 2);
   log.debug() << "Generating codet:  combining "
               << std::distance(findstart, findlim) << " blocks for addresses "
               << (*findstart) << "-" << findlim_block_start_address
               << messaget::eom;
 
   // Make a new block containing every child of interest:
   auto &this_block_children = this_block.statements();
-  assert(tree.branch.size()==this_block_children.size());
+  CHECK_RETURN(tree.branch.size() == this_block_children.size());
   for(auto blockidx=child_offset, blocklim=child_offset+nblocks;
       blockidx!=blocklim;
       ++blockidx)
@@ -918,7 +918,7 @@ code_blockt &java_bytecode_convert_methodt::get_or_create_block_for_pcrange(
   ++branchstart;
   tree.branch.erase(branchstart, branchlim);
 
-  assert(tree.branch.size()==this_block_children.size());
+  CHECK_RETURN(tree.branch.size() == this_block_children.size());
 
   auto branchaddriter=tree.branch_addresses.begin();
   std::advance(branchaddriter, child_offset);
@@ -934,7 +934,7 @@ code_blockt &java_bytecode_convert_methodt::get_or_create_block_for_pcrange(
 
   tree.branch[child_offset]=std::move(newnode);
 
-  assert(tree.branch.size()==tree.branch_addresses.size());
+  CHECK_RETURN(tree.branch.size() == tree.branch_addresses.size());
 
   return
     to_code_block(
@@ -1074,10 +1074,10 @@ java_bytecode_convert_methodt::convert_instructions(const methodt &method)
     converted_instructiont ins=converted_instructiont(i_it, code_skipt());
     std::pair<address_mapt::iterator, bool> a_entry=
       address_map.insert(std::make_pair(i_it->address, ins));
-    assert(a_entry.second);
+    CHECK_RETURN(a_entry.second);
     // addresses are strictly increasing, hence we must have inserted
     // a new maximal key
-    assert(a_entry.first==--address_map.end());
+    CHECK_RETURN(a_entry.first == --address_map.end());
 
     const auto bytecode = i_it->bytecode;
     const std::string statement = bytecode_info[i_it->bytecode].mnemonic;
@@ -1217,9 +1217,10 @@ java_bytecode_convert_methodt::convert_instructions(const methodt &method)
     instruction.stack.clear();
     codet &c = instruction.code;
 
-    assert(
+    INVARIANT(
       stack.empty() || instruction.predecessors.size() <= 1 ||
-      has_prefix(stack.front().get_string(ID_C_base_name), "$stack"));
+        has_prefix(stack.front().get_string(ID_C_base_name), "$stack"),
+      "inconsistent stack");
 
     exprt arg0=i_it->args.size()>=1?i_it->args[0]:nil_exprt();
     exprt arg1=i_it->args.size()>=2?i_it->args[1]:nil_exprt();
@@ -1288,7 +1289,7 @@ java_bytecode_convert_methodt::convert_instructions(const methodt &method)
 
     if(bytecode == BC_aconst_null)
     {
-      assert(results.size()==1);
+      PRECONDITION(results.size() == 1);
       results[0] = null_pointer_exprt(java_reference_type(java_void_type()));
     }
     else if(bytecode == BC_athrow)
@@ -1428,23 +1429,23 @@ java_bytecode_convert_methodt::convert_instructions(const methodt &method)
       // and write something like:
       // if(retaddr==5) goto 5; else if(retaddr==10) goto 10; ...
       PRECONDITION(op.empty() && results.empty());
-      assert(!jsr_ret_targets.empty());
+      PRECONDITION(!jsr_ret_targets.empty());
       c = convert_ret(
         jsr_ret_targets, arg0, i_it->source_location, i_it->address);
     }
     else if(bytecode == BC_iconst_m1)
     {
-      assert(results.size()==1);
+      CHECK_RETURN(results.size() == 1);
       results[0]=from_integer(-1, java_int_type());
     }
     else if(bytecode == patternt("?const_?"))
     {
-      assert(results.size()==1);
+      CHECK_RETURN(results.size() == 1);
       results = convert_const(statement, to_constant_expr(arg0), results);
     }
     else if(bytecode == patternt("?ipush"))
     {
-      PRECONDITION(results.size()==1);
+      CHECK_RETURN(results.size() == 1);
       DATA_INVARIANT(
         arg0.id()==ID_constant,
         "ipush argument expected to be constant");
@@ -1737,7 +1738,7 @@ java_bytecode_convert_methodt::convert_instructions(const methodt &method)
         numeric_cast_v<std::size_t>(to_constant_expr(arg1));
 
       op=pop(dimension);
-      assert(results.size()==1);
+      CHECK_RETURN(results.size() == 1);
       c = convert_multianewarray(i_it->source_location, arg0, op, results);
     }
     else if(bytecode == BC_arraylength)
@@ -1848,7 +1849,9 @@ java_bytecode_convert_methodt::convert_instructions(const methodt &method)
           stackt::const_iterator os_it=a_it2->second.stack.begin();
           for(auto &expr : stack)
           {
-            assert(has_prefix(os_it->get_string(ID_C_base_name), "$stack"));
+            INVARIANT(
+              has_prefix(os_it->get_string(ID_C_base_name), "$stack"),
+              "invalid base name");
             symbol_exprt lhs=to_symbol_expr(*os_it);
             code_assignt a(lhs, expr);
             more_code.add(a);
@@ -1917,7 +1920,7 @@ java_bytecode_convert_methodt::convert_instructions(const methodt &method)
   for(const auto &address_pair : address_map)
   {
     const method_offsett address = address_pair.first;
-    assert(address_pair.first==address_pair.second.source->address);
+    CHECK_RETURN(address_pair.first == address_pair.second.source->address);
     const codet &c=address_pair.second.code;
 
     // Start a new lexical block if this is a branch target:
@@ -1946,9 +1949,10 @@ java_bytecode_convert_methodt::convert_instructions(const methodt &method)
       root_block.add(
         code_labelt{label(std::to_string(address)), code_blockt{}});
       root.branch.push_back(block_tree_nodet::get_leaf());
-      assert((root.branch_addresses.empty() ||
-              root.branch_addresses.back()<address) &&
-             "Block addresses should be unique and increasing");
+      INVARIANT(
+        (root.branch_addresses.empty() ||
+         root.branch_addresses.back() < address),
+        "Block addresses should be unique and increasing");
       root.branch_addresses.push_back(address);
     }
 

jbmc/src/java_bytecode/java_bytecode_typecheck.cpp

@@ -25,7 +25,7 @@ std::string java_bytecode_typecheckt::to_string(const typet &type)
 
 void java_bytecode_typecheckt::typecheck_non_type_symbol(symbolt &symbol)
 {
-  assert(!symbol.is_type);
+  PRECONDITION(!symbol.is_type);
   typecheck_type(symbol.type);
   typecheck_expr(symbol.value);
 }

jbmc/src/java_bytecode/java_class_loader_limit.cpp

@@ -62,7 +62,7 @@ void java_class_loader_limitt::setup_class_load_limit(
   }
   else
   {
-    assert(java_cp_include_files.length()>1);
+    PRECONDITION(java_cp_include_files.length() > 1);
     jsont json_cp_config;
     if(parse_json(
          java_cp_include_files.substr(1),
@@ -76,7 +76,7 @@ void java_class_loader_limitt::setup_class_load_limit(
       throw "the JSON file has a wrong format";
     for(const jsont &file_entry : to_json_array(include_files))
     {
-      assert(file_entry.is_string());
+      PRECONDITION(file_entry.is_string());
       set_matcher.insert(file_entry.value);
     }
   }

jbmc/src/java_bytecode/java_entry_point.cpp

@@ -621,7 +621,7 @@ bool java_entry_point(
     return true;
   symbolt symbol=res.main_function;
 
-  assert(symbol.type.id()==ID_code);
+  DATA_INVARIANT(symbol.type.id() == ID_code, "expected code-typed symbol");
 
   return generate_java_start_function(
     symbol,

jbmc/src/java_bytecode/java_local_variable_table.cpp

@@ -488,7 +488,7 @@ static java_bytecode_convert_methodt::method_offsett get_common_dominator(
       ++domit;
       ++repeats;
     }
-    assert(repeats<=merge_vars.size());
+    INVARIANT(repeats <= merge_vars.size(), "out of bounds");
     if(repeats==merge_vars.size())
       return dom;
   }

jbmc/src/java_bytecode/java_pointer_casts.cpp

@@ -34,7 +34,7 @@ bool find_superclass_with_type(
   const typet &target_type,
   const namespacet &ns)
 {
-  assert(ptr.type().id()==ID_pointer);
+  PRECONDITION(ptr.type().id() == ID_pointer);
   while(true)
   {
     const typet ptr_base = ns.follow(to_pointer_type(ptr.type()).base_type());
@@ -93,15 +93,15 @@ exprt make_clean_pointer_cast(
   exprt bare_ptr=ptr;
   while(bare_ptr.id()==ID_typecast)
   {
-    assert(
-      bare_ptr.type().id()==ID_pointer &&
+    INVARIANT(
+      bare_ptr.type().id() == ID_pointer,
       "Non-pointer in make_clean_pointer_cast?");
     if(to_pointer_type(bare_ptr.type()).base_type() == java_void_type())
       bare_ptr = to_typecast_expr(bare_ptr).op();
   }
 
-  assert(
-    bare_ptr.type().id()==ID_pointer &&
+  INVARIANT(
+    bare_ptr.type().id() == ID_pointer,
     "Non-pointer in make_clean_pointer_cast?");
 
   if(bare_ptr.type()==target_type)

jbmc/src/java_bytecode/java_types.h

@@ -581,13 +581,13 @@ class java_class_typet:public class_typet
 
 inline const java_class_typet &to_java_class_type(const typet &type)
 {
-  assert(type.id()==ID_struct);
+  PRECONDITION(type.id() == ID_struct);
   return static_cast<const java_class_typet &>(type);
 }
 
 inline java_class_typet &to_java_class_type(typet &type)
 {
-  assert(type.id()==ID_struct);
+  PRECONDITION(type.id() == ID_struct);
   return static_cast<java_class_typet &>(type);
 }
 

src/analyses/custom_bitvector_analysis.cpp

@@ -579,7 +579,7 @@ void custom_bitvector_domaint::output(
     for(unsigned i=0; b!=0; i++, b>>=1)
       if(b&1)
       {
-        assert(i<cba.bits.size());
+        INVARIANT(i < cba.bits.size(), "inconsistent bit widths");
         out << ' '
             << cba.bits[i];
       }
@@ -595,7 +595,7 @@ void custom_bitvector_domaint::output(
     for(unsigned i=0; b!=0; i++, b>>=1)
       if(b&1)
       {
-        assert(i<cba.bits.size());
+        INVARIANT(i < cba.bits.size(), "inconsistent bit widths");
         out << ' '
             << cba.bits[i];
       }