From 85bd1737f2d47aa23264c998489f1ae7ee4fdef9 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Tue, 6 Feb 2024 04:58:32 -0800 Subject: [PATCH] relax bitvector constant check for Verilog bitvectors Verilog bitvectors use a four-valued logic, and hence do not meet the requirements of their binary counterparts. --- src/util/std_expr.cpp | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/util/std_expr.cpp b/src/util/std_expr.cpp index 3b95e3e96b9..e78505633c9 100644 --- a/src/util/std_expr.cpp +++ b/src/util/std_expr.cpp @@ -36,13 +36,17 @@ void constant_exprt::check(const exprt &expr, const validation_modet vm) vm, !can_cast_type(expr.type()) || can_cast_type(expr.type()) || + expr.type().id() == ID_verilog_unsignedbv || + expr.type().id() == ID_verilog_signedbv || id2string(value).find_first_not_of("0123456789ABCDEF") == std::string::npos, "negative bitvector constant must use two's complement"); DATA_CHECK( vm, - !can_cast_type(expr.type()) || value == ID_0 || + !can_cast_type(expr.type()) || + expr.type().id() == ID_verilog_unsignedbv || + expr.type().id() == ID_verilog_signedbv || value == ID_0 || id2string(value)[0] != '0', "bitvector constant must not have leading zeros"); }