Verilog: separate ID for explicit typecast expressions

This is to avoid any confusion with automatically generated, implicit typecasts.
diffblue · Apr 21, 2024 · d9f3402 · d9f3402
1 parent d3071f4
commit d9f3402
Show file tree

Hide file tree

Showing 3 changed files with 6 additions and 2 deletions.
diff --git 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
@@ -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
@@ -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
   {