Fix after re-basing

Author: Petr Bauch

src/goto-programs/goto_program.cpp

@@ -683,24 +683,24 @@ void goto_programt::instructiont::validate(
   case NO_INSTRUCTION_TYPE:
     break;
   case GOTO:
-    DATA_CHECK_WITH_DIAGNOSTICS(
+    DATA_CHECK_WITH_DIAGNOSTICS(vm,
       has_target(),
       "goto instruction expects at least one target",
       source_location);
     // get_target checks that targets.size()==1
-    DATA_CHECK_WITH_DIAGNOSTICS(
+    DATA_CHECK_WITH_DIAGNOSTICS(vm,
       get_target()->is_target() && get_target()->target_number != 0,
       "goto target has to be a target",
       source_location);
     break;
   case ASSUME:
-    DATA_CHECK_WITH_DIAGNOSTICS(
+    DATA_CHECK_WITH_DIAGNOSTICS(vm,
       targets.empty(),
       "assume instruction should not have a target",
       source_location);
     break;
   case ASSERT:
-    DATA_CHECK_WITH_DIAGNOSTICS(
+    DATA_CHECK_WITH_DIAGNOSTICS(vm,
       targets.empty(),
       "assert instruction should not have a target",
       source_location);
@@ -722,7 +722,7 @@ void goto_programt::instructiont::validate(
   case ATOMIC_END:
     break;
   case RETURN:
-    DATA_CHECK_WITH_DIAGNOSTICS(
+    DATA_CHECK_WITH_DIAGNOSTICS(vm,
       code.get_statement() == ID_return,
       "return instruction should contain a return statement",
       source_location);
@@ -736,29 +736,29 @@ void goto_programt::instructiont::validate(
       vm, targets.empty(), "assign instruction should not have a target");
     break;
   case DECL:
-    DATA_CHECK_WITH_DIAGNOSTICS(
+    DATA_CHECK_WITH_DIAGNOSTICS(vm,
       code.get_statement() == ID_decl,
       "declaration instructions should contain a declaration statement",
       source_location);
-    DATA_CHECK_WITH_DIAGNOSTICS(
+    DATA_CHECK_WITH_DIAGNOSTICS(vm,
       !ns.lookup(to_code_decl(code).get_identifier(), table_symbol),
       "declaring unknown symbol: " +
         id2string(to_code_decl(code).get_identifier()),
       source_location);
     break;
   case DEAD:
-    DATA_CHECK_WITH_DIAGNOSTICS(
+    DATA_CHECK_WITH_DIAGNOSTICS(vm,
       code.get_statement() == ID_dead,
       "dead instructions should contain a dead statement",
       source_location);
-    DATA_CHECK_WITH_DIAGNOSTICS(
+    DATA_CHECK_WITH_DIAGNOSTICS(vm,
       !ns.lookup(to_code_dead(code).get_identifier(), table_symbol),
       "removing unknown symbol: " +
         id2string(to_code_dead(code).get_identifier()) + " from scope",
       source_location);
     break;
   case FUNCTION_CALL:
-    DATA_CHECK_WITH_DIAGNOSTICS(
+    DATA_CHECK_WITH_DIAGNOSTICS(vm,
       code.get_statement() == ID_function_call,
       "function call instruction should contain a call statement",
       source_location);

src/util/std_code.h

@@ -377,8 +377,9 @@ class code_declt:public codet
     const validation_modet vm = validation_modet::INVARIANT)
   {
     DATA_CHECK(
-      code.operands().size() == 1, "declaration must have one operand");
+      vm, code.operands().size() == 1, "declaration must have one operand");
     DATA_CHECK(
+      vm,
       code.op0().id() == ID_symbol,
       "declaring a non-symbol: " +
         id2string(to_symbol_expr(code.op0()).get_identifier()));
@@ -448,9 +449,11 @@ class code_deadt:public codet
     const validation_modet vm = validation_modet::INVARIANT)
   {
     DATA_CHECK(
+      vm,
       code.operands().size() == 1,
       "removal (code_deadt) must have one operand");
     DATA_CHECK(
+      vm,
       code.op0().id() == ID_symbol,
       "removing a non-symbol: " +
         id2string(to_symbol_expr(code.op0()).get_identifier()) + "from scope");
@@ -1087,6 +1090,7 @@ class code_function_callt:public codet
     const validation_modet vm = validation_modet::INVARIANT)
   {
     DATA_CHECK(
+      vm,
       code.operands().size() == 3,
       "function calls must have three operands:\n1) expression to store the "
       "returned values\n2) the function being called\n3) the vector of "
@@ -1102,10 +1106,12 @@ class code_function_callt:public codet
 
     if(code.op0().id() == ID_nil)
       DATA_CHECK(
+        vm,
         to_code_type(code.op1().type()).return_type().id() == ID_empty,
         "void function should not return value");
     else
       DATA_CHECK(
+        vm,
         base_type_eq(
           code.op0().type(), to_code_type(code.op1().type()).return_type(), ns),
         "function returns expression of wrong type");
@@ -1186,7 +1192,7 @@ class code_returnt:public codet
     const codet &code,
     const validation_modet vm = validation_modet::INVARIANT)
   {
-    DATA_CHECK(code.operands().size() == 1, "return must have one operand");
+    DATA_CHECK(vm, code.operands().size() == 1, "return must have one operand");
   }
 };