remove assert()

Author: Daniel Kroening

src/goto-programs/goto_inline.cpp

@@ -49,40 +49,42 @@ void goto_inline(
 
   typedef goto_functionst::goto_functiont goto_functiont;
 
-    // find entry point
-    goto_functionst::function_mapt::iterator it=
-      goto_functions.function_map.find(goto_functionst::entry_point());
+  // find entry point
+  goto_functionst::function_mapt::iterator it=
+    goto_functions.function_map.find(goto_functionst::entry_point());
 
-    if(it==goto_functions.function_map.end())
-      return;
+  if(it==goto_functions.function_map.end())
+    return;
 
-    goto_functiont &goto_function=it->second;
-    assert(goto_function.body_available());
+  goto_functiont &goto_function=it->second;
+  DATA_INVARIANT(
+    goto_function.body_available(),
+    "body of entry point function must be available");
 
-    // gather all calls
-    // we use non-transitive inlining to avoid the goto program
-    // copying that goto_inlinet would do otherwise
-    goto_inlinet::inline_mapt inline_map;
+  // gather all calls
+  // we use non-transitive inlining to avoid the goto program
+  // copying that goto_inlinet would do otherwise
+  goto_inlinet::inline_mapt inline_map;
 
-    Forall_goto_functions(f_it, goto_functions)
-    {
-      goto_functiont &goto_function=f_it->second;
+  Forall_goto_functions(f_it, goto_functions)
+  {
+    goto_functiont &goto_function=f_it->second;
 
-      if(!goto_function.body_available())
-        continue;
+    if(!goto_function.body_available())
+      continue;
 
-      goto_inlinet::call_listt &call_list=inline_map[f_it->first];
+    goto_inlinet::call_listt &call_list=inline_map[f_it->first];
 
-      goto_programt &goto_program=goto_function.body;
+    goto_programt &goto_program=goto_function.body;
 
-      Forall_goto_program_instructions(i_it, goto_program)
-      {
-        if(!i_it->is_function_call())
-          continue;
+    Forall_goto_program_instructions(i_it, goto_program)
+    {
+      if(!i_it->is_function_call())
+        continue;
 
-        call_list.push_back(goto_inlinet::callt(i_it, false));
-      }
+      call_list.push_back(goto_inlinet::callt(i_it, false));
     }
+  }
 
   goto_inline.goto_inline(
     goto_functionst::entry_point(), goto_function, inline_map, true);
@@ -198,7 +200,7 @@ void goto_partial_inline(
       if(goto_function.is_inlined() ||
          goto_program.instructions.size()<=smallfunc_limit)
       {
-        assert(i_it->is_function_call());
+        INVARIANT(i_it->is_function_call(), "is a call");
         call_list.push_back(goto_inlinet::callt(i_it, false));
       }
     }

src/goto-programs/goto_inline_class.cpp

@@ -17,12 +17,13 @@ Author: Daniel Kroening, [email protected]
 
 #include <cassert>
 
-#include <util/prefix.h>
-#include <util/cprover_prefix.h>
 #include <util/base_type.h>
+#include <util/cprover_prefix.h>
+#include <util/expr_util.h>
+#include <util/invariant.h>
+#include <util/prefix.h>
 #include <util/std_code.h>
 #include <util/std_expr.h>
-#include <util/expr_util.h>
 
 #include "remove_skip.h"
 #include "goto_inline.h"
@@ -34,8 +35,8 @@ void goto_inlinet::parameter_assignments(
   const exprt::operandst &arguments, // arguments of call
   goto_programt &dest)
 {
-  assert(target->is_function_call());
-  assert(dest.empty());
+  PRECONDITION(target->is_function_call());
+  PRECONDITION(dest.empty());
 
   const source_locationt &source_location=target->source_location;
 
@@ -160,8 +161,8 @@ void goto_inlinet::parameter_destruction(
   const code_typet &code_type, // type of called function
   goto_programt &dest)
 {
-  assert(target->is_function_call());
-  assert(dest.empty());
+  PRECONDITION(target->is_function_call());
+  PRECONDITION(dest.empty());
 
   const source_locationt &source_location=target->source_location;
 
@@ -204,51 +205,6 @@ void goto_inlinet::replace_return(
   {
     if(it->is_return())
     {
-      #if 0
-      if(lhs.is_not_nil())
-      {
-        if(it->code.operands().size()!=1)
-        {
-          error().source_location=it->code.find_source_location();
-          str << "return expects one operand!";
-          warning_msg();
-          continue;
-        }
-
-        goto_programt tmp;
-        goto_programt::targett assignment=tmp.add_instruction(ASSIGN);
-
-        code_assignt code_assign(lhs, it->code.op0());
-
-        // this may happen if the declared return type at the call site
-        // differs from the defined return type
-        if(code_assign.lhs().type()!=
-           code_assign.rhs().type())
-          code_assign.rhs().make_typecast(code_assign.lhs().type());
-
-        assignment->code=code_assign;
-        assignment->source_location=it->source_location;
-        assignment->function=it->function;
-
-        dest.insert_before_swap(it, *assignment);
-        it++;
-      }
-      else if(!it->code.operands().empty())
-      {
-        goto_programt tmp;
-        goto_programt::targett expression=tmp.add_instruction(OTHER);
-
-        expression->code=codet(ID_expression);
-        expression->code.move_to_operands(it->code.op0());
-        expression->source_location=it->source_location;
-        expression->function=it->function;
-
-        dest.insert_before_swap(it, *expression);
-        it++;
-      }
-
-      it->make_goto(--dest.instructions.end());
-      #else
       if(lhs.is_not_nil())
       {
         if(it->code.operands().size()!=1)
@@ -280,7 +236,6 @@ void goto_inlinet::replace_return(
         it->type=OTHER;
         it++;
       }
-      #endif
     }
   }
 }
@@ -327,9 +282,9 @@ void goto_inlinet::insert_function_body(
   const symbol_exprt &function,
   const exprt::operandst &arguments)
 {
-  assert(target->is_function_call());
-  assert(!dest.empty());
-  assert(goto_function.body_available());
+  PRECONDITION(target->is_function_call());
+  PRECONDITION(!dest.empty());
+  PRECONDITION(goto_function.body_available());
 
   const irep_idt identifier=function.get_identifier();
 
@@ -338,7 +293,9 @@ void goto_inlinet::insert_function_body(
   inline_log.copy_from(goto_function.body, body);
 
   goto_programt::instructiont &end=body.instructions.back();
-  assert(end.is_end_function());
+  DATA_INVARIANT(
+    end.is_end_function(),
+    "final instruction of a function must be an END_FUNCTION");
   end.type=LOCATION;
 
   if(adjust_function)
@@ -367,7 +324,9 @@ void goto_inlinet::insert_function_body(
   t_it=goto_function.body.instructions.begin();
   unsigned begin_location_number=t_it->location_number;
   t_it=--goto_function.body.instructions.end();
-  assert(t_it->is_end_function());
+  DATA_INVARIANT(
+    t_it->is_end_function(),
+    "final instruction of a function must be an END_FUNCTION");
   unsigned end_location_number=t_it->location_number;
 
   unsigned call_location_number=target->location_number;
@@ -426,8 +385,8 @@ void goto_inlinet::insert_function_nobody(
   const symbol_exprt &function,
   const exprt::operandst &arguments)
 {
-  assert(target->is_function_call());
-  assert(!dest.empty());
+  PRECONDITION(target->is_function_call());
+  PRECONDITION(!dest.empty());
 
   const irep_idt identifier=function.get_identifier();
 
@@ -479,9 +438,9 @@ void goto_inlinet::expand_function_call(
   const bool force_full,
   goto_programt::targett target)
 {
-  assert(target->is_function_call());
-  assert(!dest.empty());
-  assert(!transitive || inline_map.empty());
+  PRECONDITION(target->is_function_call());
+  PRECONDITION(!dest.empty());
+  PRECONDITION(!transitive || inline_map.empty());
 
 #ifdef DEBUG
   std::cout << "Expanding call:\n";
@@ -600,7 +559,7 @@ void goto_inlinet::get_call(
   exprt &function,
   exprt::operandst &arguments)
 {
-  assert(it->is_function_call());
+  PRECONDITION(it->is_function_call());
 
   const code_function_callt &call=to_code_function_call(it->code);
 
@@ -613,12 +572,12 @@ void goto_inlinet::goto_inline(
   const inline_mapt &inline_map,
   const bool force_full)
 {
-  assert(check_inline_map(inline_map));
+  PRECONDITION(check_inline_map(inline_map));
 
   Forall_goto_functions(f_it, goto_functions)
   {
     const irep_idt identifier=f_it->first;
-    assert(!identifier.empty());
+    DATA_INVARIANT(!identifier.empty(), "function name must not be empty");
     goto_functiont &goto_function=f_it->second;
 
     if(!goto_function.body_available())
@@ -649,14 +608,14 @@ void goto_inlinet::goto_inline_nontransitive(
   const inline_mapt &inline_map,
   const bool force_full)
 {
-  assert(goto_function.body_available());
+  PRECONDITION(goto_function.body_available());
 
   finished_sett::const_iterator f_it=finished_set.find(identifier);
 
   if(f_it!=finished_set.end())
     return;
 
-  assert(check_inline_map(identifier, inline_map));
+  PRECONDITION(check_inline_map(identifier, inline_map));
 
   goto_programt &goto_program=goto_function.body;
 
@@ -700,19 +659,23 @@ const goto_inlinet::goto_functiont &goto_inlinet::goto_inline_transitive(
   const goto_functiont &goto_function,
   const bool force_full)
 {
-  assert(goto_function.body_available());
+  PRECONDITION(goto_function.body_available());
 
   cachet::const_iterator c_it=cache.find(identifier);
 
   if(c_it!=cache.end())
   {
     const goto_functiont &cached=c_it->second;
-    assert(cached.body_available());
+    DATA_INVARIANT(
+      cached.body_available(),
+      "body of cached functions must be available");
     return cached;
   }
 
   goto_functiont &cached=cache[identifier];
-  assert(cached.body.empty());
+  INVARIANT(
+    cached.body.empty(),
+    "body of new function in cache must be empty");
 
   progress() << "Creating copy of " << identifier << eom;
   progress() << "Number of instructions: "
@@ -772,7 +735,7 @@ bool goto_inlinet::check_inline_map(
   goto_functionst::function_mapt::const_iterator f_it=
     goto_functions.function_map.find(identifier);
 
-  assert(f_it!=goto_functions.function_map.end());
+  PRECONDITION(f_it!=goto_functions.function_map.end());
 
   inline_mapt::const_iterator im_it=inline_map.find(identifier);
 
@@ -824,11 +787,11 @@ void goto_inlinet::output_inline_map(
   std::ostream &out,
   const inline_mapt &inline_map)
 {
-  assert(check_inline_map(inline_map));
+  PRECONDITION(check_inline_map(inline_map));
 
   for(const auto &it : inline_map)
   {
-    const irep_idt id=it.first;
+    const irep_idt &id=it.first;
     const call_listt &call_list=it.second;
 
     out << "Function: " << id << "\n";
@@ -842,7 +805,7 @@ void goto_inlinet::output_inline_map(
        !call_list.empty())
     {
       const goto_functiont &goto_function=f_it->second;
-      assert(goto_function.body_available());
+      PRECONDITION(goto_function.body_available());
 
       const goto_programt &goto_program=goto_function.body;
 
@@ -903,12 +866,12 @@ void goto_inlinet::goto_inline_logt::add_segment(
   const unsigned call_location_number,
   const irep_idt function)
 {
-  assert(!goto_program.empty());
-  assert(!function.empty());
-  assert(end_location_number>=begin_location_number);
+  PRECONDITION(!goto_program.empty());
+  PRECONDITION(!function.empty());
+  PRECONDITION(end_location_number>=begin_location_number);
 
   goto_programt::const_targett start=goto_program.instructions.begin();
-  assert(log_map.find(start)==log_map.end());
+  PRECONDITION(log_map.find(start)==log_map.end());
 
   goto_programt::const_targett end=goto_program.instructions.end();
   end--;
@@ -927,7 +890,7 @@ void goto_inlinet::goto_inline_logt::copy_from(
   const goto_programt &from,
   const goto_programt &to)
 {
-  assert(from.instructions.size()==to.instructions.size());
+  PRECONDITION(from.instructions.size()==to.instructions.size());
 
   goto_programt::const_targett it1=from.instructions.begin();
   goto_programt::const_targett it2=to.instructions.begin();