From d9f340268befffc0e587778cd2c96192df4a46fe Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Thu, 21 Mar 2024 15:39:42 -0700 Subject: [PATCH] Verilog: separate ID for explicit typecast expressions This is to avoid any confusion with automatically generated, implicit typecasts. --- src/hw_cbmc_irep_ids.h | 1 + src/verilog/parser.y | 4 +++- src/verilog/verilog_typecheck_expr.cpp | 3 ++- 3 files changed, 6 insertions(+), 2 deletions(-) diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h index f7a3ff5a6..38366d368 100644 --- a/src/hw_cbmc_irep_ids.h +++ b/src/hw_cbmc_irep_ids.h @@ -35,6 +35,7 @@ IREP_ID_TWO(C_little_endian, #little_endian) IREP_ID_ONE(ports) IREP_ID_ONE(inst) IREP_ID_ONE(Verilog) +IREP_ID_ONE(verilog_explicit_cast) IREP_ID_ONE(verilog_non_indexed_part_select) IREP_ID_ONE(verilog_indexed_part_select_plus) IREP_ID_ONE(verilog_indexed_part_select_minus) diff --git a/src/verilog/parser.y b/src/verilog/parser.y index cced4ddb1..aa3fff981 100644 --- a/src/verilog/parser.y +++ b/src/verilog/parser.y @@ -3140,7 +3140,9 @@ time_literal: TOK_TIME_LITERAL cast: casting_type '\'' '(' expression ')' - { init($$, ID_typecast); stack_expr($$).type() = stack_type($1); mto($$, $4); } + { init($$, ID_verilog_explicit_cast); + stack_expr($$).type() = stack_type($1); + mto($$, $4); } ; // System Verilog standard 1800-2017 diff --git a/src/verilog/verilog_typecheck_expr.cpp b/src/verilog/verilog_typecheck_expr.cpp index 7ce309264..56952ed54 100644 --- a/src/verilog/verilog_typecheck_expr.cpp +++ b/src/verilog/verilog_typecheck_expr.cpp @@ -1877,12 +1877,13 @@ exprt verilog_typecheck_exprt::convert_unary_expr(unary_exprt expr) make_boolean(expr.op()); expr.type()=bool_typet(); } - else if(expr.id() == ID_typecast) + else if(expr.id() == ID_verilog_explicit_cast) { // System Verilog has got type'(expr). This is an explicit // type cast. expr.type() = convert_type(expr.type()); convert_expr(expr.op()); + expr.id(ID_typecast); } else {