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

jbmc/src/java_bytecode/character_refine_preprocess.cpp

@@ -27,7 +27,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();
@@ -111,7 +111,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();
@@ -223,7 +223,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();
@@ -586,7 +586,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);
@@ -600,7 +600,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(
@@ -758,7 +758,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);
@@ -895,7 +895,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();