Skip to content

Commit 85bd173

Browse files
committed
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.
1 parent 2d96b83 commit 85bd173

File tree

1 file changed

+5
-1
lines changed

1 file changed

+5
-1
lines changed

src/util/std_expr.cpp

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -36,13 +36,17 @@ void constant_exprt::check(const exprt &expr, const validation_modet vm)
3636
vm,
3737
!can_cast_type<bitvector_typet>(expr.type()) ||
3838
can_cast_type<pointer_typet>(expr.type()) ||
39+
expr.type().id() == ID_verilog_unsignedbv ||
40+
expr.type().id() == ID_verilog_signedbv ||
3941
id2string(value).find_first_not_of("0123456789ABCDEF") ==
4042
std::string::npos,
4143
"negative bitvector constant must use two's complement");
4244

4345
DATA_CHECK(
4446
vm,
45-
!can_cast_type<bitvector_typet>(expr.type()) || value == ID_0 ||
47+
!can_cast_type<bitvector_typet>(expr.type()) ||
48+
expr.type().id() == ID_verilog_unsignedbv ||
49+
expr.type().id() == ID_verilog_signedbv || value == ID_0 ||
4650
id2string(value)[0] != '0',
4751
"bitvector constant must not have leading zeros");
4852
}

0 commit comments

Comments
 (0)