Merge pull request #7409 from tautschnig/cleanup/assert-to-invariant2

Replace remaining uses of assert(...) by macros from invariant.h

Author: kroening

src/goto-cc/as86_cmdline.cpp

@@ -11,10 +11,11 @@ Author: Michael Tautschnig
 
 #include "as86_cmdline.h"
 
-#include <iostream>
-
+#include <util/invariant.h>
 #include <util/prefix.h>
 
+#include <iostream>
+
 // non-as86 options
 const char *goto_as86_options_with_argument[]=
 {
@@ -56,7 +57,7 @@ const char *as86_options_with_argument[]=
 
 bool as86_cmdlinet::parse(int argc, const char **argv)
 {
-  assert(argc>0);
+  PRECONDITION(argc > 0);
   add_arg(argv[0]);
 
   for(int i=1; i<argc; i++)

src/goto-cc/as_cmdline.cpp

@@ -11,10 +11,11 @@ Author: Michael Tautschnig
 
 #include "as_cmdline.h"
 
-#include <iostream>
-
+#include <util/invariant.h>
 #include <util/prefix.h>
 
+#include <iostream>
+
 // non-as options
 const char *goto_as_options_with_argument[]=
 {
@@ -78,7 +79,7 @@ const char *as_options_with_argument[]=
 
 bool as_cmdlinet::parse(int argc, const char **argv)
 {
-  assert(argc>0);
+  PRECONDITION(argc > 0);
   add_arg(argv[0]);
 
   for(int i=1; i<argc; i++)

src/goto-cc/as_mode.cpp

@@ -201,7 +201,7 @@ int as_modet::doit()
       {
         if(outputs>0)
         {
-          assert(!dest.empty());
+          PRECONDITION(!dest.empty());
           compiler.add_input_file(dest);
           os.close();
         }
@@ -230,7 +230,7 @@ int as_modet::doit()
 
     if(outputs>0)
     {
-      assert(!dest.empty());
+      PRECONDITION(!dest.empty());
       compiler.add_input_file(dest);
     }
     else
@@ -260,7 +260,7 @@ int as_modet::doit()
 /// run as or as86 with original command line
 int as_modet::run_as()
 {
-  assert(!cmdline.parsed_argv.empty());
+  PRECONDITION(!cmdline.parsed_argv.empty());
 
   // build new argv
   std::vector<std::string> new_argv;

src/goto-cc/bcc_cmdline.cpp

@@ -11,10 +11,11 @@ Author: Michael Tautschnig
 
 #include "bcc_cmdline.h"
 
-#include <iostream>
-
+#include <util/invariant.h>
 #include <util/prefix.h>
 
+#include <iostream>
+
 // non-bcc options
 const char *goto_bcc_options_with_argument[]=
 {
@@ -68,7 +69,7 @@ const char *bcc_options_with_argument[]=
 
 bool bcc_cmdlinet::parse(int argc, const char **argv)
 {
-  assert(argc>0);
+  PRECONDITION(argc > 0);
   add_arg(argv[0]);
 
   for(int i=1; i<argc; i++)

src/goto-cc/gcc_cmdline.cpp

@@ -11,6 +11,7 @@ Author: CM Wintersteiger, 2006
 
 #include "gcc_cmdline.h"
 
+#include <util/invariant.h>
 #include <util/prefix.h>
 
 #include <cstring>
@@ -228,7 +229,7 @@ const char *gcc_options_without_argument[]=
 /// \return none
 bool gcc_cmdlinet::parse(int argc, const char **argv)
 {
-  assert(argc>0);
+  PRECONDITION(argc > 0);
   add_arg(argv[0]);
 
   argst current_args;
@@ -447,8 +448,8 @@ bool gcc_cmdlinet::parse_arguments(
 void gcc_cmdlinet::parse_specs_line(const std::string &line, bool in_spec_file)
 {
   // initial whitespace has been stripped
-  assert(!line.empty());
-  assert(line[0]!=' ' && line[0]!='\t');
+  PRECONDITION(!line.empty());
+  PRECONDITION(line[0] != ' ' && line[0] != '\t');
 
   argst args_from_specs;
 

src/goto-cc/ld_cmdline.cpp

@@ -11,10 +11,11 @@ Author: Daniel Kroening, 2013
 
 #include "ld_cmdline.h"
 
-#include <iostream>
-
+#include <util/invariant.h>
 #include <util/prefix.h>
 
+#include <iostream>
+
 // clang-format off
 const char *goto_ld_options_with_argument[]=
 {
@@ -253,7 +254,7 @@ const char *ld_options_without_argument[]=
 /// \return none
 bool ld_cmdlinet::parse(int argc, const char **argv)
 {
-  assert(argc>0);
+  PRECONDITION(argc > 0);
   add_arg(argv[0]);
 
   for(int i=1; i<argc; i++)

src/jsil/jsil_parse_tree.cpp

@@ -31,7 +31,7 @@ static bool insert_at_label(
     if(l.get_label()!=label)
       continue;
 
-    assert(l.code().get_statement()==ID_skip);
+    DATA_INVARIANT(l.code().get_statement() == ID_skip, "code should be skip");
     l.code()=code;
 
     return false;

src/jsil/jsil_typecheck.cpp

@@ -167,8 +167,9 @@ void jsil_typecheckt::typecheck_expr_main(exprt &expr)
   }
   else
   {
-    // expressions are expected not to have type set just yet
-    assert(expr.type().is_nil() || expr.type().id().empty());
+    DATA_INVARIANT(
+      expr.type().is_nil() || expr.type().id().empty(),
+      "expressions are expected not to have type set just yet");
 
     if(expr.id()==ID_null ||
         expr.id()=="undefined" ||
@@ -273,7 +274,7 @@ void jsil_typecheckt::typecheck_expr_side_effect_throw(
   side_effect_expr_throwt &expr)
 {
   irept &excep_list=expr.add(ID_exception_list);
-  assert(excep_list.id()==ID_symbol);
+  PRECONDITION(excep_list.id() == ID_symbol);
   symbol_exprt &s=static_cast<symbol_exprt &>(excep_list);
   typecheck_symbol_expr(s);
 }
@@ -622,7 +623,7 @@ void jsil_typecheckt::typecheck_symbol_expr(symbol_exprt &symbol_expr)
     else
     {
       // symbol already exists
-      assert(!s_it->second.is_type);
+      DATA_INVARIANT(!s_it->second.is_type, "non-type symbol expected");
 
       const symbolt &symbol=s_it->second;
 
@@ -837,7 +838,7 @@ void jsil_typecheckt::typecheck_assign(code_assignt &code)
 /// \par parameters: any symbol
 void jsil_typecheckt::typecheck_non_type_symbol(symbolt &symbol)
 {
-  assert(!symbol.is_type);
+  PRECONDITION(!symbol.is_type);
 
   // Using is_extern to check if symbol was already typechecked
   if(symbol.is_extern)

src/jsil/jsil_types.h

@@ -47,7 +47,7 @@ class jsil_builtin_code_typet:public code_typet
 inline jsil_builtin_code_typet &to_jsil_builtin_code_type(
   code_typet &code)
 {
-  assert(code.get_bool("jsil_builtin_proceduret"));
+  PRECONDITION(code.get_bool("jsil_builtin_proceduret"));
   return static_cast<jsil_builtin_code_typet &>(code);
 }
 
@@ -70,7 +70,7 @@ class jsil_spec_code_typet:public code_typet
 inline jsil_spec_code_typet &to_jsil_spec_code_type(
   code_typet &code)
 {
-  assert(code.get_bool("jsil_spec_proceduret"));
+  PRECONDITION(code.get_bool("jsil_spec_proceduret"));
   return static_cast<jsil_spec_code_typet &>(code);
 }
 
@@ -101,13 +101,13 @@ class jsil_union_typet:public union_typet
 
 inline jsil_union_typet &to_jsil_union_type(typet &type)
 {
-  assert(type.id()==ID_union);
+  PRECONDITION(type.id() == ID_union);
   return static_cast<jsil_union_typet &>(type);
 }
 
 inline const jsil_union_typet &to_jsil_union_type(const typet &type)
 {
-  assert(type.id()==ID_union);
+  PRECONDITION(type.id() == ID_union);
   return static_cast<const jsil_union_typet &>(type);
 }
 

src/linking/linking.cpp

@@ -1215,7 +1215,7 @@ void linkingt::duplicate_type_symbol(
   symbolt &old_symbol,
   const symbolt &new_symbol)
 {
-  assert(new_symbol.is_type);
+  PRECONDITION(new_symbol.is_type);
 
   if(!old_symbol.is_type)
   {
@@ -1310,7 +1310,7 @@ bool linkingt::needs_renaming_type(
   const symbolt &old_symbol,
   const symbolt &new_symbol)
 {
-  assert(new_symbol.is_type);
+  PRECONDITION(new_symbol.is_type);
 
   if(!old_symbol.is_type)
     return true;