From 76f0ec7d45c4dc90950a5425fdcb81830206340e Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Thu, 29 Nov 2018 15:03:56 +0000 Subject: [PATCH] Make validation mode parameter explicit in DATA_CHECK() macros --- src/goto-programs/goto_program.cpp | 4 +++- src/util/std_code.h | 3 ++- src/util/std_expr.h | 6 +++++- src/util/std_types.h | 3 ++- src/util/symbol_table.cpp | 5 +++++ src/util/validate.h | 22 ++++++---------------- 6 files changed, 23 insertions(+), 20 deletions(-) diff --git a/src/goto-programs/goto_program.cpp b/src/goto-programs/goto_program.cpp index 79a86c41d1d..f9eecb2238f 100644 --- a/src/goto-programs/goto_program.cpp +++ b/src/goto-programs/goto_program.cpp @@ -706,9 +706,11 @@ void goto_programt::instructiont::validate( break; case ASSIGN: DATA_CHECK( + vm, code.get_statement() == ID_assign, "assign instruction should contain an assign statement"); - DATA_CHECK(targets.empty(), "assign instruction should not have a target"); + DATA_CHECK( + vm, targets.empty(), "assign instruction should not have a target"); break; case DECL: break; diff --git a/src/util/std_code.h b/src/util/std_code.h index b92e933074a..0ac06412e1a 100644 --- a/src/util/std_code.h +++ b/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"); } diff --git a/src/util/std_expr.h b/src/util/std_expr.h index b008a64d012..ec9a35fa853 100644 --- a/src/util/std_expr.h +++ b/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"); } diff --git a/src/util/std_types.h b/src/util/std_types.h index 970549694be..99cb0be3df5 100644 --- a/src/util/std_types.h +++ b/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"); } }; diff --git a/src/util/symbol_table.cpp b/src/util/symbol_table.cpp index e6d058286ec..23ef1e327d7 100644 --- a/src/util/symbol_table.cpp +++ b/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 '", diff --git a/src/util/validate.h b/src/util/validate.h index eaf62c0576c..dc48c601e3d 100644 --- a/src/util/validate.h +++ b/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::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::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: \