Remove some preconditions and appropriately type the expressions.

Author: NlightNFotis

src/goto-programs/goto_convert_exceptions.cpp

@@ -18,10 +18,10 @@ void goto_convertt::convert_msc_try_finally(
   goto_programt &dest,
   const irep_idt &mode)
 {
-  DATA_INVARIANT(
+  INVARIANT_WITH_DIAGNOSTICS(
     code.operands().size() == 2,
-    code.find_source_location().as_string() +
-      ": msc_try_finally expects two arguments");
+    "msc_try_finally expects two arguments",
+    code.find_source_location());
 
   goto_programt tmp;
   tmp.add_instruction(SKIP)->source_location=code.source_location();
@@ -55,10 +55,10 @@ void goto_convertt::convert_msc_try_except(
   goto_programt &dest,
   const irep_idt &mode)
 {
-  DATA_INVARIANT(
+  INVARIANT_WITH_DIAGNOSTICS(
     code.operands().size() == 3,
-    code.find_source_location().as_string() +
-      ": msc_try_except expects three arguments");
+    "msc_try_except expects three arguments",
+    code.find_source_location());
 
   convert(to_code(code.op0()), dest, mode);
 
@@ -70,9 +70,8 @@ void goto_convertt::convert_msc_leave(
   goto_programt &dest,
   const irep_idt &mode)
 {
-  DATA_INVARIANT(
-    targets.leave_set,
-    code.find_source_location().as_string() + ": leave without target");
+  INVARIANT_WITH_DIAGNOSTICS(
+    targets.leave_set, "leave without target", code.find_source_location());
 
   // need to process destructor stack
   for(std::size_t d=targets.destructor_stack.size();
@@ -94,10 +93,10 @@ void goto_convertt::convert_try_catch(
   goto_programt &dest,
   const irep_idt &mode)
 {
-  DATA_INVARIANT(
+  INVARIANT_WITH_DIAGNOSTICS(
     code.operands().size() >= 2,
-    code.find_source_location().as_string() +
-      ": try_catch expects at least two arguments");
+    "try_catch expects at least two arguments",
+    code.find_source_location());
 
   // add the CATCH-push instruction to 'dest'
   goto_programt::targett catch_push_instruction=dest.add_instruction();
@@ -155,10 +154,10 @@ void goto_convertt::convert_CPROVER_try_catch(
   goto_programt &dest,
   const irep_idt &mode)
 {
-  DATA_INVARIANT(
+  INVARIANT_WITH_DIAGNOSTICS(
     code.operands().size() == 2,
-    code.find_source_location().as_string() +
-      ": CPROVER_try_catch expects two arguments");
+    "CPROVER_try_catch expects two arguments",
+    code.find_source_location());
 
   // this is where we go after 'throw'
   goto_programt tmp;
@@ -229,10 +228,10 @@ void goto_convertt::convert_CPROVER_try_finally(
   goto_programt &dest,
   const irep_idt &mode)
 {
-  DATA_INVARIANT(
+  INVARIANT_WITH_DIAGNOSTICS(
     code.operands().size() == 2,
-    code.find_source_location().as_string() +
-      ": CPROVER_try_finally expects two arguments");
+    "CPROVER_try_finally expects two arguments",
+    code.find_source_location());
 
   // first put 'finally' code onto destructor stack
   targets.destructor_stack.push_back(to_code(code.op1()));

src/goto-programs/goto_convert_side_effect.cpp

@@ -60,10 +60,10 @@ void goto_convertt::remove_assignment(
           statement==ID_assign_bitxor ||
           statement==ID_assign_bitor)
   {
-    INVARIANT(
+    INVARIANT_WITH_DIAGNOSTICS(
       expr.operands().size() == 2,
-      expr.find_source_location().as_string() + ": " + id2string(statement) +
-        " takes two arguments");
+      id2string(statement) + " expects two arguments",
+      expr.find_source_location());
 
     irep_idt new_id;
 
@@ -138,16 +138,16 @@ void goto_convertt::remove_pre(
   bool result_is_used,
   const irep_idt &mode)
 {
-  DATA_INVARIANT(
+  INVARIANT_WITH_DIAGNOSTICS(
     expr.operands().size() == 1,
-    expr.find_source_location().as_string() +
-      ": preincrement/predecrement must have one operand");
+    "preincrement/predecrement must have one operand",
+    expr.find_source_location());
 
   const irep_idt statement=expr.get_statement();
 
   DATA_INVARIANT(
     statement == ID_preincrement || statement == ID_predecrement,
-    " expected preincrement or predecrement");
+    "expects preincrement or predecrement");
 
   exprt rhs;
   rhs.add_source_location()=expr.source_location();
@@ -227,16 +227,16 @@ void goto_convertt::remove_post(
 
   // we have ...(op++)...
 
-  DATA_INVARIANT(
+  INVARIANT_WITH_DIAGNOSTICS(
     expr.operands().size() == 1,
-    expr.find_source_location().as_string() +
-      ": postincrement/postdecrement must have one operand");
+    "postincrement/postdecrement must have one operand",
+    expr.find_source_location());
 
   const irep_idt statement=expr.get_statement();
 
   DATA_INVARIANT(
     statement == ID_postincrement || statement == ID_postdecrement,
-    " expected postincrement or postdecrement");
+    "expects postincrement or postdecrement");
 
   exprt rhs;
   rhs.add_source_location()=expr.source_location();
@@ -326,12 +326,13 @@ void goto_convertt::remove_function_call(
   const irep_idt &mode,
   bool result_is_used)
 {
+  INVARIANT_WITH_DIAGNOSTICS(
+    expr.operands().size() == 2,
+    "function_call expects two operands",
+    expr.find_source_location());
+
   if(!result_is_used)
   {
-    DATA_INVARIANT(
-      expr.operands().size() == 2,
-      expr.find_source_location().as_string() +
-        ": function_call expects two operands");
     code_function_callt call(nil_exprt(), expr.op0(), expr.op1().operands());
     call.add_source_location()=expr.source_location();
     convert_function_call(call, dest, mode);
@@ -341,14 +342,10 @@ void goto_convertt::remove_function_call(
 
   // get name of function, if available
 
-  DATA_INVARIANT(
+  INVARIANT_WITH_DIAGNOSTICS(
     expr.id() == ID_side_effect && expr.get(ID_statement) == ID_function_call,
-    expr.find_source_location().as_string() + ": expected function call");
-
-  DATA_INVARIANT(
-    !expr.operands().empty(),
-    expr.find_source_location().as_string() +
-      ": function_call expects at least one operand");
+    "expects function call",
+    expr.find_source_location());
 
   std::string new_base_name = "return_value";
   irep_idt new_symbol_mode = mode;
@@ -430,7 +427,7 @@ void goto_convertt::remove_cpp_delete(
   side_effect_exprt &expr,
   goto_programt &dest)
 {
-  DATA_INVARIANT(expr.operands().size() == 1, "cpp_delete expected 1 operand");
+  DATA_INVARIANT(expr.operands().size() == 1, "cpp_delete expects one operand");
 
   codet tmp(expr.get_statement());
   tmp.add_source_location()=expr.source_location();
@@ -483,10 +480,10 @@ void goto_convertt::remove_temporary_object(
   goto_programt &dest)
 {
   const irep_idt &mode = expr.get(ID_mode);
-  DATA_INVARIANT(
+  INVARIANT_WITH_DIAGNOSTICS(
     expr.operands().size() <= 1,
-    expr.find_source_location().as_string() +
-      ": temporary_object takes 0 or 1 operands");
+    "temporary_object takes zero or one operands",
+    expr.find_source_location());
 
   symbolt &new_symbol = new_tmp_symbol(
     expr.type(), "obj", dest, expr.find_source_location(), mode);
@@ -500,10 +497,10 @@ void goto_convertt::remove_temporary_object(
 
   if(expr.find(ID_initializer).is_not_nil())
   {
-    INVARIANT(
+    INVARIANT_WITH_DIAGNOSTICS(
       expr.operands().empty(),
-      expr.find_source_location().as_string() +
-        ": temporary_object takes 0 operands");
+      "temporary_object takes zero operands",
+      expr.find_source_location());
     exprt initializer=static_cast<const exprt &>(expr.find(ID_initializer));
     replace_new_object(new_symbol.symbol_expr(), initializer);
 
@@ -524,15 +521,15 @@ void goto_convertt::remove_statement_expression(
   // The expression is copied into a temporary before the
   // scope is destroyed.
 
-  DATA_INVARIANT(
+  INVARIANT_WITH_DIAGNOSTICS(
     expr.operands().size() == 1,
-    expr.find_source_location().as_string() +
-      ": statement_expression takes 1 operand");
+    "statement_expression takes one operand",
+    expr.find_source_location());
 
-  DATA_INVARIANT(
+  INVARIANT_WITH_DIAGNOSTICS(
     expr.op0().id() == ID_code,
-    expr.find_source_location().as_string() +
-      ": statement_expression takes code as operand");
+    "statement_expression takes code as operand",
+    expr.find_source_location());
 
   codet &code=to_code(expr.op0());
 
@@ -543,15 +540,15 @@ void goto_convertt::remove_statement_expression(
     return;
   }
 
-  DATA_INVARIANT(
+  INVARIANT_WITH_DIAGNOSTICS(
     code.get_statement() == ID_block,
-    code.find_source_location().as_string() +
-      ": statement_expression takes block as operand");
+    "statement_expression takes block as operand",
+    code.find_source_location());
 
-  DATA_INVARIANT(
+  INVARIANT_WITH_DIAGNOSTICS(
     !code.operands().empty(),
-    expr.find_source_location().as_string() +
-      ": statement_expression takes non-empty block as operand");
+    "statement_expression takes non-empty block as operand",
+    expr.find_source_location());
 
   // get last statement from block, following labels
   codet &last=to_code_block(code).find_last_statement();

src/goto-programs/goto_inline_class.cpp

@@ -54,7 +54,7 @@ void goto_inlinet::parameter_assignments(
 
     const irep_idt &identifier=parameter.get_identifier();
 
-    INVARIANT(
+    DATA_INVARIANT(
       !identifier.empty(),
       source_location.as_string() + ": no identifier for function parameter");
 
@@ -842,7 +842,7 @@ void goto_inlinet::goto_inline_logt::copy_from(
   {
     DATA_INVARIANT(
       it2 != to.instructions.end(),
-      "'to' target function is not alllowed to be empty");
+      "'to' target function is not allowed to be empty");
     DATA_INVARIANT(
       it1->location_number == it2->location_number,
       "both functions' instruction should point to the same source");

src/goto-programs/goto_program.cpp

@@ -165,7 +165,8 @@ std::ostream &goto_programt::output_instruction(
         instruction.code.find(ID_exception_list).get_sub();
       DATA_INVARIANT(
         instruction.targets.size() == exception_list.size(),
-        "size of target list");
+        "unexpected discrepancy between sizes of instruction"
+        "targets and exception list");
       for(instructiont::targetst::const_iterator
             gt_it=instruction.targets.begin();
           gt_it!=instruction.targets.end();
@@ -223,10 +224,11 @@ void goto_programt::get_decl_identifiers(
     if(it->is_decl())
     {
       DATA_INVARIANT(
-        it->code.get_statement() == ID_decl, "declaration statements");
+        it->code.get_statement() == ID_decl,
+        "expected statement to be declaration statement");
       DATA_INVARIANT(
         it->code.operands().size() == 1,
-        "declaration statement expects 1 operand");
+        "declaration statement expects one operand");
       const symbol_exprt &symbol_expr=to_symbol_expr(it->code.op0());
       decl_identifiers.insert(symbol_expr.get_identifier());
     }
@@ -237,26 +239,24 @@ void parse_lhs_read(const exprt &src, std::list<exprt> &dest)
 {
   if(src.id()==ID_dereference)
   {
-    PRECONDITION(src.operands().size() == 1);
-    dest.push_back(src.op0());
+    dest.push_back(to_dereference_expr(src).pointer());
   }
   else if(src.id()==ID_index)
   {
-    PRECONDITION(src.operands().size() == 2);
-    dest.push_back(src.op1());
-    parse_lhs_read(src.op0(), dest);
+    auto &index_expr = to_index_expr(src);
+    dest.push_back(index_expr.index());
+    parse_lhs_read(index_expr.array(), dest);
   }
   else if(src.id()==ID_member)
   {
-    PRECONDITION(src.operands().size() == 1);
-    parse_lhs_read(src.op0(), dest);
+    parse_lhs_read(to_member_expr(src).compound(), dest);
   }
   else if(src.id()==ID_if)
   {
-    PRECONDITION(src.operands().size() == 3);
-    dest.push_back(src.op0());
-    parse_lhs_read(src.op1(), dest);
-    parse_lhs_read(src.op2(), dest);
+    auto &if_expr = to_if_expr(src);
+    dest.push_back(if_expr.cond());
+    parse_lhs_read(if_expr.true_case(), dest);
+    parse_lhs_read(if_expr.false_case(), dest);
   }
 }
 
@@ -346,9 +346,9 @@ void objects_read(
   else if(src.id()==ID_dereference)
   {
     // this reads what is pointed to plus the pointer
-    PRECONDITION(src.operands().size() == 1);
-    dest.push_back(src);
-    objects_read(src.op0(), dest);
+    auto &deref = to_dereference_expr(src);
+    dest.push_back(deref);
+    objects_read(deref.pointer(), dest);
   }
   else
   {
@@ -376,9 +376,9 @@ void objects_written(
 {
   if(src.id()==ID_if)
   {
-    PRECONDITION(src.operands().size() == 3);
-    objects_written(src.op1(), dest);
-    objects_written(src.op2(), dest);
+    auto &if_expr = to_if_expr(src);
+    objects_written(if_expr.true_case(), dest);
+    objects_written(if_expr.false_case(), dest);
   }
   else
     dest.push_back(src);
@@ -557,7 +557,8 @@ void goto_programt::compute_target_numbers()
     if(i.is_target())
     {
       i.target_number=++cnt;
-      DATA_INVARIANT(i.target_number != 0, "instruction's number cannot be 0");
+      DATA_INVARIANT(
+        i.target_number != 0, "GOTO instruction target cannot be zero");
     }
   }
 
@@ -571,10 +572,10 @@ void goto_programt::compute_target_numbers()
       if(t!=instructions.end())
       {
         DATA_INVARIANT(
-          t->target_number != 0, "instruction's number cannot be 0");
+          t->target_number != 0, "instruction's number cannot be zero");
         DATA_INVARIANT(
           t->target_number != instructiont::nil_target,
-          "instruction cannot be an invalid target");
+          "GOTO instruction target cannot be nil_target");
       }
     }
   }