diff --git a/src/util/expr_cast.h b/src/util/expr_cast.h index 18d6a933bdc..52992f0c5ea 100644 --- a/src/util/expr_cast.h +++ b/src/util/expr_cast.h @@ -170,8 +170,8 @@ optionalt type_try_dynamic_cast(TType &&base) static_assert(!std::is_const::value, "Attempted to move from const."); if(!can_cast_type(base)) return {}; + TType::check(base); optionalt ret{static_cast(base)}; - validate_type(*ret); return ret; } diff --git a/src/util/std_types.h b/src/util/std_types.h index d1edcfe9e82..454925b2275 100644 --- a/src/util/std_types.h +++ b/src/util/std_types.h @@ -1130,7 +1130,8 @@ class bv_typet:public bitvector_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"); } }; @@ -1241,7 +1242,7 @@ class signedbv_typet:public bitvector_typet const validation_modet vm = validation_modet::INVARIANT) { DATA_CHECK( - !type.get(ID_width).empty(), "signed bitvector type must have width"); + vm, !type.get(ID_width).empty(), "signed bitvector type must have width"); } }; @@ -1305,7 +1306,7 @@ class fixedbv_typet:public bitvector_typet const validation_modet vm = validation_modet::INVARIANT) { DATA_CHECK( - !type.get(ID_width).empty(), "fixed bitvector type must have width"); + vm, !type.get(ID_width).empty(), "fixed bitvector type must have width"); } }; @@ -1367,7 +1368,7 @@ class floatbv_typet:public bitvector_typet const validation_modet vm = validation_modet::INVARIANT) { DATA_CHECK( - !type.get(ID_width).empty(), "float bitvector type must have width"); + vm, !type.get(ID_width).empty(), "float bitvector type must have width"); } }; @@ -1469,7 +1470,7 @@ class pointer_typet:public bitvector_typet const typet &type, const validation_modet vm = validation_modet::INVARIANT) { - DATA_CHECK(!type.get(ID_width).empty(), "pointer must have width"); + DATA_CHECK(vm, !type.get(ID_width).empty(), "pointer must have width"); } }; @@ -1567,7 +1568,7 @@ class c_bool_typet:public bitvector_typet const typet &type, const validation_modet vm = validation_modet::INVARIANT) { - DATA_CHECK(!type.get(ID_width).empty(), "C bool type must have width"); + DATA_CHECK(vm, !type.get(ID_width).empty(), "C bool type must have width"); } }; diff --git a/src/util/type.h b/src/util/type.h index 6d45c282fd7..910a06952bf 100644 --- a/src/util/type.h +++ b/src/util/type.h @@ -88,7 +88,8 @@ class typet:public irept /// /// The validation mode indicates whether well-formedness check failures are /// reported via DATA_INVARIANT violations or exceptions. - static void check(const typet &, const validation_modet) + static void + check(const typet &, const validation_modet = validation_modet::INVARIANT) { }