make linter happy

Author: Daniel Kroening

src/goto-programs/goto_program.cpp

@@ -163,7 +163,8 @@ std::ostream &goto_programt::output_instruction(
       unsigned i=0;
       const irept::subt &exception_list=
         instruction.code.find(ID_exception_list).get_sub();
-      assert(instruction.targets.size()==exception_list.size());
+      DATA_INVARIANT(instruction.targets.size()==exception_list.size(),
+                     "size of target list");
       for(instructiont::targetst::const_iterator
             gt_it=instruction.targets.begin();
           gt_it!=instruction.targets.end();
@@ -220,8 +221,10 @@ void goto_programt::get_decl_identifiers(
   {
     if(it->is_decl())
     {
-      assert(it->code.get_statement()==ID_decl);
-      assert(it->code.operands().size()==1);
+      DATA_INVARIANT(it->code.get_statement()==ID_decl,
+                     "declaration statements");
+      DATA_INVARIANT(it->code.operands().size()==1,
+                     "operand of declaration statement");
       const symbol_exprt &symbol_expr=to_symbol_expr(it->code.op0());
       decl_identifiers.insert(symbol_expr.get_identifier());
     }
@@ -539,7 +542,7 @@ void goto_programt::compute_target_numbers()
     if(i.is_target())
     {
       i.target_number=++cnt;
-      assert(i.target_number!=0);
+      DATA_INVARIANT(i.target_number!=0, "target numbers");
     }
   }
 
@@ -552,8 +555,10 @@ void goto_programt::compute_target_numbers()
     {
       if(t!=instructions.end())
       {
-        assert(t->target_number!=0);
-        assert(t->target_number!=instructiont::nil_target);
+        DATA_INVARIANT(t->target_number!=0,
+                       "target numbers");
+        DATA_INVARIANT(t->target_number!=instructiont::nil_target,
+                       "target numbers");
       }
     }
   }

src/goto-programs/goto_program.h

@@ -188,7 +188,7 @@ class goto_programt
     /// target
     targett get_target() const
     {
-      assert(targets.size()==1);
+      PRECONDITION(targets.size()==1);
       return targets.front();
     }
 
@@ -398,7 +398,7 @@ class goto_programt
   static const irep_idt get_function_id(
     const goto_programt &p)
   {
-    assert(!p.empty());
+    PRECONDITION(!p.empty());
 
     return get_function_id(--p.instructions.end());
   }
@@ -411,7 +411,7 @@ class goto_programt
   /// Insertion that preserves jumps to "target".
   void insert_before_swap(targett target)
   {
-    assert(target!=instructions.end());
+    PRECONDITION(target!=instructions.end());
     const auto next=std::next(target);
     instructions.insert(next, instructiont())->swap(*target);
   }
@@ -430,7 +430,7 @@ class goto_programt
     targett target,
     goto_programt &p)
   {
-    assert(target!=instructions.end());
+    PRECONDITION(target!=instructions.end());
     if(p.instructions.empty())
       return;
     insert_before_swap(target, p.instructions.front());
@@ -586,9 +586,10 @@ class goto_programt
 
   targett get_end_function()
   {
-    assert(!instructions.empty());
+    PRECONDITION(!instructions.empty());
     const auto end_function=std::prev(instructions.end());
-    assert(end_function->is_end_function());
+    DATA_INVARIANT(end_function->is_end_function(),
+                   "goto program ends on END_FUNCTION");
     return end_function;
   }
 
@@ -671,6 +672,7 @@ inline bool order_const_target(
   return &_i1<&_i2;
 }
 
+// NOLINTNEXTLINE(readability/identifiers)
 struct const_target_hash
 {
   std::size_t operator()(