Make validation mode parameter explicit in DATA_CHECK() macros

Author: danpoe

src/util/std_code.h

@@ -291,7 +291,7 @@ class code_assignt:public codet
     const validation_modet vm = validation_modet::INVARIANT)
   {
     DATA_CHECK(
-      code.operands().size() == 2, "assignment must have two operands");
+      vm, code.operands().size() == 2, "assignment must have two operands");
   }
 
   static void validate(
@@ -302,6 +302,7 @@ class code_assignt:public codet
     check(code, vm);
 
     DATA_CHECK(
+      vm,
       base_type_eq(code.op0().type(), code.op1().type(), ns),
       "lhs and rhs of assignment must have same type");
   }

src/util/std_expr.h

@@ -777,7 +777,9 @@ class binary_exprt:public exprt
     const validation_modet vm = validation_modet::INVARIANT)
   {
     DATA_CHECK(
-      expr.operands().size() == 2, "binary expression must have two operands");
+      vm,
+      expr.operands().size() == 2,
+      "binary expression must have two operands");
   }
 
   static void validate(
@@ -859,6 +861,7 @@ class binary_predicate_exprt:public binary_exprt
     binary_exprt::validate(expr, ns, vm);
 
     DATA_CHECK(
+      vm,
       expr.type().id() == ID_bool,
       "result of binary predicate expression should be of type bool");
   }
@@ -901,6 +904,7 @@ class binary_relation_exprt:public binary_predicate_exprt
 
     // check types
     DATA_CHECK(
+      vm,
       base_type_eq(expr.op0().type(), expr.op1().type(), ns),
       "lhs and rhs of binary relation expression should have same type");
   }

src/util/std_types.h

@@ -1149,7 +1149,8 @@ class bitvector_typet : public typet
     const typet &type,
     const validation_modet vm = validation_modet::INVARIANT)
   {
-    DATA_CHECK(!type.get(ID_width).empty(), "bitvector type must have width");
+    DATA_CHECK(
+      vm, !type.get(ID_width).empty(), "bitvector type must have width");
   }
 };
 

src/util/symbol_table.cpp

@@ -130,6 +130,7 @@ void symbol_tablet::validate(const validation_modet vm) const
 
     // Check that symbols[id].name == id
     DATA_CHECK_WITH_DIAGNOSTICS(
+      vm,
       symbol.name == symbol_key,
       "Symbol table entry must map to a symbol with the correct identifier",
       "Symbol table key '",
@@ -152,6 +153,7 @@ void symbol_tablet::validate(const validation_modet vm) const
           }) != symbol_base_map.end();
 
       DATA_CHECK_WITH_DIAGNOSTICS(
+        vm,
         base_map_matches_symbol,
         "The base_name of a symbol should map to itself",
         "Symbol table key '",
@@ -174,6 +176,7 @@ void symbol_tablet::validate(const validation_modet vm) const
           }) != symbol_module_map.end();
 
       DATA_CHECK_WITH_DIAGNOSTICS(
+        vm,
         module_map_matches_symbol,
         "Symbol table module map should map to symbol",
         "Symbol table key '",
@@ -188,6 +191,7 @@ void symbol_tablet::validate(const validation_modet vm) const
   for(auto base_map_entry : symbol_base_map)
   {
     DATA_CHECK_WITH_DIAGNOSTICS(
+      vm,
       has_symbol(base_map_entry.second),
       "Symbol table base_name map entries must map to a symbol name",
       "base_name map entry '",
@@ -201,6 +205,7 @@ void symbol_tablet::validate(const validation_modet vm) const
   for(auto module_map_entry : symbol_module_map)
   {
     DATA_CHECK_WITH_DIAGNOSTICS(
+      vm,
       has_symbol(module_map_entry.second),
       "Symbol table module map entries must map to a symbol name",
       "base_name map entry '",

src/util/validate.h

@@ -15,18 +15,13 @@ Author: Daniel Poetzl
 #include "validation_mode.h"
 
 /// This macro takes a condition which denotes a well-formedness criterion on
-/// goto programs, expressions, instructions, etc. When invoking the macro, a
-/// variable named `vm` of type `const validation_modet` should be in scope. It
-/// indicates whether DATA_INVARIANT() is used to check the condition, or if an
-/// exception is thrown when the condition does not hold.
-#define DATA_CHECK(condition, message)                                         \
+/// goto programs, expressions, instructions, etc. The first parameter should be
+/// of type `validate_modet` and indicates whether DATA_INVARIANT() is used to
+/// check the condition, or if an exception is thrown when the condition does
+/// not hold.
+#define DATA_CHECK(vm, condition, message)                                     \
   do                                                                           \
   {                                                                            \
-    static_assert(                                                             \
-      std::is_same<decltype(vm), const validation_modet>::value,               \
-      "when invoking the macro DATA_CHECK(), a variable named `vm` of type "   \
-      "`const validation_modet` should be in scope which indicates the "       \
-      "validation mode (see `validate.h`");                                    \
     switch(vm)                                                                 \
     {                                                                          \
     case validation_modet::INVARIANT:                                          \
@@ -39,14 +34,9 @@ Author: Daniel Poetzl
     }                                                                          \
   } while(0)
 
-#define DATA_CHECK_WITH_DIAGNOSTICS(condition, message, ...)                   \
+#define DATA_CHECK_WITH_DIAGNOSTICS(vm, condition, message, ...)               \
   do                                                                           \
   {                                                                            \
-    static_assert(                                                             \
-      std::is_same<decltype(vm), const validation_modet>::value,               \
-      "when invoking the macro DATA_CHECK_WITH_DIAGNOSTICS(), a variable "     \
-      "named `vm` of type `const validation_modet` should be in scope which "  \
-      "indicates the validation mode (see `validate.h`");                      \
     switch(vm)                                                                 \
     {                                                                          \
     case validation_modet::INVARIANT:                                          \