Remove some preconditions and appropriately type the expressions.

Author: NlightNFotis

src/goto-programs/goto_convert_side_effect.cpp

@@ -60,7 +60,7 @@ void goto_convertt::remove_assignment(
           statement==ID_assign_bitxor ||
           statement==ID_assign_bitor)
   {
-    INVARIANT(
+    DATA_INVARIANT(
       expr.operands().size() == 2,
       expr.find_source_location().as_string() + ": " + id2string(statement) +
         " takes two arguments");
@@ -147,7 +147,7 @@ void goto_convertt::remove_pre(
 
   DATA_INVARIANT(
     statement == ID_preincrement || statement == ID_predecrement,
-    " expected preincrement or predecrement");
+    "expected preincrement or predecrement");
 
   exprt rhs;
   rhs.add_source_location()=expr.source_location();
@@ -236,7 +236,7 @@ void goto_convertt::remove_post(
 
   DATA_INVARIANT(
     statement == ID_postincrement || statement == ID_postdecrement,
-    " expected postincrement or postdecrement");
+    "expected 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)
 {
+  DATA_INVARIANT(
+    expr.operands().size() == 2,
+    expr.find_source_location().as_string() +
+      ": function_call expects two operands");
+
   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);
@@ -345,11 +346,6 @@ void goto_convertt::remove_function_call(
     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");
-
   std::string new_base_name = "return_value";
   irep_idt new_symbol_mode = mode;
 
@@ -430,7 +426,8 @@ 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 expected one operand");
 
   codet tmp(expr.get_statement());
   tmp.add_source_location()=expr.source_location();
@@ -486,7 +483,7 @@ void goto_convertt::remove_temporary_object(
   DATA_INVARIANT(
     expr.operands().size() <= 1,
     expr.find_source_location().as_string() +
-      ": temporary_object takes 0 or 1 operands");
+      ": temporary_object takes zero or one operands");
 
   symbolt &new_symbol = new_tmp_symbol(
     expr.type(), "obj", dest, expr.find_source_location(), mode);
@@ -503,7 +500,7 @@ void goto_convertt::remove_temporary_object(
     INVARIANT(
       expr.operands().empty(),
       expr.find_source_location().as_string() +
-        ": temporary_object takes 0 operands");
+        ": temporary_object takes zero operands");
     exprt initializer=static_cast<const exprt &>(expr.find(ID_initializer));
     replace_new_object(new_symbol.symbol_expr(), initializer);
 
@@ -527,7 +524,7 @@ void goto_convertt::remove_statement_expression(
   DATA_INVARIANT(
     expr.operands().size() == 1,
     expr.find_source_location().as_string() +
-      ": statement_expression takes 1 operand");
+      ": statement_expression takes one operand");
 
   DATA_INVARIANT(
     expr.op0().id() == ID_code,
@@ -564,7 +561,7 @@ void goto_convertt::remove_statement_expression(
   symbol_exprt tmp_symbol_expr(new_symbol.name, new_symbol.type);
   tmp_symbol_expr.add_source_location()=source_location;
 
-  if(last.get(ID_statement)==ID_expression)
+  if(last.get(ID_statement_expressionement)==ID_expression)
   {
     // we turn this into an assignment
     exprt e=to_code_expression(last).expression();

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);
@@ -544,7 +544,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, 
+      	"instruction's number cannot be zero");
     }
   }
 
@@ -558,7 +559,7 @@ 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");