CONTRACTS: use INVARIANT instead of exit(0)

Author: Remi Delmas

src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.cpp

@@ -118,12 +118,10 @@ void dfcc_spec_functionst::generate_havoc_function(
   const irep_idt &havoc_function_id,
   int &nof_targets)
 {
-  if(goto_model.symbol_table.has_symbol(havoc_function_id))
-  {
-    log.error() << "dfcc_spec_functionst::generate_havoc_function: '"
-                << havoc_function_id << "' already exists" << messaget::eom;
-    exit(0);
-  }
+  INVARIANT(
+    !goto_model.symbol_table.has_symbol(havoc_function_id),
+    "DFCC: havoc function id '" + id2string(havoc_function_id) +
+      "' already exists");
 
   const auto &function_symbol = utils.get_function_symbol(function_id);
 
@@ -153,14 +151,11 @@ void dfcc_spec_functionst::generate_havoc_function(
   havoc_function_symbol.module = function_symbol.module;
   havoc_function_symbol.location = function_symbol.location;
   havoc_function_symbol.set_compiled();
-
-  if(goto_model.symbol_table.add(havoc_function_symbol))
-  {
-    log.error() << "dfcc_spec_functionst::generate_havoc_function: could not "
-                   "insert symbol '"
-                << havoc_function_id << "' in symbol table" << messaget::eom;
-    exit(0);
-  }
+  bool add_function_failed = goto_model.symbol_table.add(havoc_function_symbol);
+  INVARIANT(
+    !add_function_failed,
+    "DFCC: could not insert havoc function '" + id2string(havoc_function_id) +
+      "' in the symbol table");
 
   // create new goto_function
   goto_functiont dummy_havoc_function;

src/goto-instrument/contracts/dynamic-frames/dfcc_utils.cpp

@@ -456,7 +456,8 @@ exprt dfcc_utilst::make_sizeof_expr(const exprt &expr)
 exprt dfcc_utilst::make_map_start_address(const exprt &expr)
 {
   return typecast_exprt::conditional_cast(
-    address_of_exprt(index_exprt(expr, from_integer(0, c_index_type()))),
+    address_of_exprt(index_exprt(
+      expr, from_integer(0, to_array_type(expr.type()).index_type()))),
     pointer_type(bool_typet()));
 }