jsil: Replace assert(...) by macros from invariant.h

While new/modified code shouldn't use assert(...) anyway, we had several
existing uses of assert. Once we remove nonstd/optional.h, we will no
longer implicitly include cassert, implying that a lot of #include
<cassert> changes will be necessary. Instead of adding these, go all the
way and fix the undesired uses of assert.

Author: tautschnig

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);
 }