From 53a1b8fde40e0d4b75b05ad15f0628d40008d89a Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Fri, 15 Mar 2024 16:14:46 -0700 Subject: [PATCH 1/5] Verilog: add two KNOWNBUG tests for arrays --- regression/verilog/arrays/packed_real1.desc | 8 ++++++++ regression/verilog/arrays/packed_real1.sv | 9 +++++++++ regression/verilog/arrays/packed_typedef1.desc | 8 ++++++++ regression/verilog/arrays/packed_typedef1.sv | 8 ++++++++ 4 files changed, 33 insertions(+) create mode 100644 regression/verilog/arrays/packed_real1.desc create mode 100644 regression/verilog/arrays/packed_real1.sv create mode 100644 regression/verilog/arrays/packed_typedef1.desc create mode 100644 regression/verilog/arrays/packed_typedef1.sv diff --git a/regression/verilog/arrays/packed_real1.desc b/regression/verilog/arrays/packed_real1.desc new file mode 100644 index 000000000..7a513846c --- /dev/null +++ b/regression/verilog/arrays/packed_real1.desc @@ -0,0 +1,8 @@ +KNOWNBUG +packed_real1.sv +--module main --bound 0 +^EXIT=10$ +^SIGNAL=0$ +-- +-- +A packed array of reals must be rejected. diff --git a/regression/verilog/arrays/packed_real1.sv b/regression/verilog/arrays/packed_real1.sv new file mode 100644 index 000000000..6d261906f --- /dev/null +++ b/regression/verilog/arrays/packed_real1.sv @@ -0,0 +1,9 @@ +module main; + + // Packed arrays can be made of single bit data types + // or other packed types. + typedef real my_real; + my_real [7:0] my_array; + +endmodule + diff --git a/regression/verilog/arrays/packed_typedef1.desc b/regression/verilog/arrays/packed_typedef1.desc new file mode 100644 index 000000000..4ad097bdc --- /dev/null +++ b/regression/verilog/arrays/packed_typedef1.desc @@ -0,0 +1,8 @@ +KNOWNBUG +packed_typedef1.sv +--module main --bound 0 +^EXIT=0$ +^SIGNAL=0$ +-- +-- +The packed array type must not be dropped. diff --git a/regression/verilog/arrays/packed_typedef1.sv b/regression/verilog/arrays/packed_typedef1.sv new file mode 100644 index 000000000..e27e179c1 --- /dev/null +++ b/regression/verilog/arrays/packed_typedef1.sv @@ -0,0 +1,8 @@ +module main; + + typedef bit my_bit; + my_bit [7:0] my_vector; + + always assert p0: ($bits(my_vector) == 8); + +endmodule From f17eeb7baca3143ae0d44c573c63a7d2054c02f7 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Fri, 15 Mar 2024 15:29:03 -0700 Subject: [PATCH 2/5] Verilog: distinguish packed and unpacked arrays This adds two new IDs to distinguish packed and unpacked arrays in the Verilog parse tree. --- src/hw_cbmc_irep_ids.h | 4 +++- src/verilog/parser.y | 31 +++++++++++++++++--------- src/verilog/verilog_elaborate.cpp | 31 +++++++++++++++++++++----- src/verilog/verilog_typecheck.cpp | 2 +- src/verilog/verilog_typecheck_type.cpp | 10 +++++++-- 5 files changed, 58 insertions(+), 20 deletions(-) diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h index 7ca642e29..2f2bd871c 100644 --- a/src/hw_cbmc_irep_ids.h +++ b/src/hw_cbmc_irep_ids.h @@ -110,9 +110,11 @@ IREP_ID_ONE(wire) IREP_ID_ONE(uwire) IREP_ID_ONE(wand) IREP_ID_ONE(automatic) -IREP_ID_ONE(verilog_enum) IREP_ID_TWO(C_verilog_type, #verilog_type) +IREP_ID_ONE(verilog_enum) +IREP_ID_ONE(verilog_packed_array) IREP_ID_ONE(verilog_type_reference) +IREP_ID_ONE(verilog_unpacked_array) IREP_ID_ONE(enum_names) IREP_ID_ONE(var) IREP_ID_ONE(trireg) diff --git a/src/verilog/parser.y b/src/verilog/parser.y index 66b19d97b..2760a0375 100644 --- a/src/verilog/parser.y +++ b/src/verilog/parser.y @@ -826,8 +826,10 @@ module_port_input_declaration: TOK_INPUT net_port_type port_identifier unpacked_dimension_brace { init($$, ID_decl); stack_expr($$).set(ID_class, ID_input); - add_as_subtype(stack_type($4), stack_type($2)); - addswap($$, ID_type, $4); + // The net_port_type goes onto the declaration, + // and the unpacked_array_type goes onto the declarator. + addswap($$, ID_type, $2); + addswap($3, ID_type, $4); mto($$, $3); } ; @@ -835,14 +837,18 @@ module_port_output_declaration: TOK_OUTPUT net_port_type port_identifier unpacked_dimension_brace { init($$, ID_decl); stack_expr($$).set(ID_class, ID_output); - add_as_subtype(stack_type($4), stack_type($2)); - addswap($$, ID_type, $4); + // The data_type goes onto the declaration, + // and the unpacked_array_type goes onto the declarator. + addswap($$, ID_type, $2); + addswap($3, ID_type, $4); mto($$, $3); } | TOK_OUTPUT data_type port_identifier unpacked_dimension_brace { init($$, ID_decl); stack_expr($$).set(ID_class, ID_output_register); - add_as_subtype(stack_type($4), stack_type($2)); - addswap($$, ID_type, $4); + // The data_type goes onto the declaration, + // and the unpacked_array_type goes onto the declarator. + addswap($$, ID_type, $2); + addswap($3, ID_type, $4); mto($$, $3); } ; @@ -1215,7 +1221,7 @@ list_of_net_names: { $$=$1; mto($$, $3); } ; -net_name: net_identifier packed_dimension_brace +net_name: net_identifier unpacked_dimension_brace { $$=$1; stack_expr($$).id(ID_declarator); @@ -1285,7 +1291,9 @@ data_type: | TOK_VIRTUAL interface_opt interface_identifier { init($$, "virtual_interface"); } | /*scope_opt*/ type_identifier packed_dimension_brace - { $$ = $1; stack_expr($$).id(ID_typedef_type); } + { stack_expr($1).id(ID_typedef_type); + add_as_subtype(stack_type($2), stack_type($1)); + $$ = $2; } // | class_type | TOK_EVENT { init($$, ID_event); } @@ -1734,7 +1742,7 @@ packed_dimension_opt: packed_dimension: '[' const_expression TOK_COLON const_expression ']' - { init($$, ID_array); + { init($$, ID_verilog_packed_array); stack_type($$).add_subtype().make_nil(); exprt &range=static_cast(stack_type($$).add(ID_range)); range.add_to_operands(stack_expr($2)); @@ -1744,13 +1752,14 @@ packed_dimension: unpacked_dimension: '[' const_expression TOK_COLON const_expression ']' - { init($$, ID_array); + { init($$, ID_verilog_unpacked_array); stack_type($$).add_subtype().make_nil(); exprt &range=static_cast(stack_type($$).add(ID_range)); range.add_to_operands(stack_expr($2)); range.add_to_operands(stack_expr($4)); } | '[' expression ']' - { init($$, ID_array); + { // starts at index 0 + init($$, ID_verilog_unpacked_array); stack_type($$).add_subtype().make_nil(); stack_type($$).set(ID_size, std::move(stack_expr($2))); } diff --git a/src/verilog/verilog_elaborate.cpp b/src/verilog/verilog_elaborate.cpp index 6172a73bb..cf7561c6a 100644 --- a/src/verilog/verilog_elaborate.cpp +++ b/src/verilog/verilog_elaborate.cpp @@ -24,7 +24,9 @@ void verilog_typecheckt::collect_port_symbols(const verilog_declt &decl) const irep_idt &base_name = declarator.base_name(); const irep_idt &port_class = decl.get_class(); + auto type = convert_type(decl.type()); + irep_idt identifier = hierarchical_identifier(base_name); if(port_class.empty()) @@ -34,7 +36,18 @@ void verilog_typecheckt::collect_port_symbols(const verilog_declt &decl) else { // add the symbol - symbolt new_symbol(identifier, type, mode); + typet final_type; + if(declarator.type().is_nil()) + final_type = type; + else if(declarator.type().id() == ID_verilog_unpacked_array) + final_type = unpacked_array_type(declarator.type(), type); + else + { + throw errort().with_location(declarator.source_location()) + << "unexpected type on declarator"; + } + + symbolt new_symbol(identifier, final_type, mode); if(port_class == ID_input) { @@ -222,7 +235,7 @@ void verilog_typecheckt::collect_symbols(const verilog_declt &decl) if(declarator.type().is_nil()) symbol.type = type; - else if(declarator.type().id() == ID_array) + else if(declarator.type().id() == ID_verilog_unpacked_array) symbol.type = array_type(declarator.type(), type); else { @@ -315,7 +328,15 @@ void verilog_typecheckt::collect_symbols(const verilog_declt &decl) << "empty symbol name"; } - symbol.type = type; + if(declarator.type().is_nil()) + symbol.type = type; + else if(declarator.type().id() == ID_verilog_unpacked_array) + symbol.type = unpacked_array_type(declarator.type(), type); + else + { + throw errort().with_location(declarator.source_location()) + << "unexpected type on declarator"; + } symbol.name = hierarchical_identifier(symbol.base_name); @@ -401,7 +422,7 @@ void verilog_typecheckt::collect_symbols(const verilog_declt &decl) if(declarator.type().is_nil()) symbol.type = type; - else if(declarator.type().id() == ID_array) + else if(declarator.type().id() == ID_verilog_unpacked_array) symbol.type = array_type(declarator.type(), type); else { @@ -468,7 +489,7 @@ void verilog_typecheckt::collect_symbols(const verilog_declt &decl) if(declarator.type().is_nil()) symbol.type = type; - else if(declarator.type().id() == ID_array) + else if(declarator.type().id() == ID_verilog_unpacked_array) symbol.type = array_type(declarator.type(), type); else { diff --git a/src/verilog/verilog_typecheck.cpp b/src/verilog/verilog_typecheck.cpp index 4a779cc3d..a9a51a3e5 100644 --- a/src/verilog/verilog_typecheck.cpp +++ b/src/verilog/verilog_typecheck.cpp @@ -44,7 +44,7 @@ array_typet verilog_typecheckt::array_type( { // int whatnot[x:y]; // 'src' is yet to be converted, but 'element_type' is already converted. - PRECONDITION(src.id() == ID_array); + PRECONDITION(src.id() == ID_verilog_unpacked_array); // Unpacked arrays may have a range [x:y], // or a size [s], equivalent to [0:s-1] diff --git a/src/verilog/verilog_typecheck_type.cpp b/src/verilog/verilog_typecheck_type.cpp index 0485d99d5..f155e52a5 100644 --- a/src/verilog/verilog_typecheck_type.cpp +++ b/src/verilog/verilog_typecheck_type.cpp @@ -111,7 +111,7 @@ typet verilog_typecheck_exprt::convert_type(const typet &src) result.set(ID_C_identifier, enum_type.identifier()); return result.with_source_location(source_location); } - else if(src.id() == ID_array) + else if(src.id() == ID_verilog_packed_array) { const exprt &range=static_cast(src.find(ID_range)); @@ -147,7 +147,8 @@ typet verilog_typecheck_exprt::convert_type(const typet &src) } else { - // we have a genuine array, and do a recursive call + // We have a multi-dimensional packed array, + // and do a recursive call. const exprt size=from_integer(width, integer_typet()); typet s=convert_type(subtype); @@ -158,6 +159,11 @@ typet verilog_typecheck_exprt::convert_type(const typet &src) return std::move(result).with_source_location(source_location); } } + else if(src.id() == ID_verilog_unpacked_array) + { + // not expected here -- these stick to the declarators + PRECONDITION(false); + } else if(src.id() == ID_verilog_type_reference) { auto &type_reference = to_verilog_type_reference(src); From de6e7e7c43719853b9f7b29a9ed099d91059b239 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Fri, 15 Mar 2024 15:32:00 -0700 Subject: [PATCH 3/5] Verilog: make net_decl_assignment rule match SystemVerilog 1800-2017 This removes the net_name rule, and makes the assignment in the net_decl_assignment rule optional, to match SystemVerilog 1800-2017. --- src/verilog/parser.y | 34 +++++++++++----------------------- 1 file changed, 11 insertions(+), 23 deletions(-) diff --git a/src/verilog/parser.y b/src/verilog/parser.y index 2760a0375..9e46a22b8 100644 --- a/src/verilog/parser.y +++ b/src/verilog/parser.y @@ -1179,12 +1179,7 @@ genvar_declaration: ; net_declaration: - net_type drive_strength_opt vectored_scalared_opt data_type_or_implicit delay3_opt list_of_net_names ';' - { init($$, ID_decl); - addswap($$, ID_class, $1); - addswap($$, ID_type, $4); - swapop($$, $6); } - | net_type drive_strength_opt vectored_scalared_opt data_type_or_implicit delay3_opt list_of_net_decl_assignments ';' + net_type drive_strength_opt vectored_scalared_opt data_type_or_implicit delay3_opt list_of_net_decl_assignments ';' { init($$, ID_decl); addswap($$, ID_class, $1); addswap($$, ID_type, $4); @@ -1214,21 +1209,6 @@ vectored_scalared_opt: | TOK_SCALARED { init($$, "scalared"); } ; -list_of_net_names: - net_name - { init($$); mto($$, $1); } - | list_of_net_names ',' net_name - { $$=$1; mto($$, $3); } - ; - -net_name: net_identifier unpacked_dimension_brace - { - $$=$1; - stack_expr($$).id(ID_declarator); - addswap($$, ID_type, $2); - } - ; - list_of_net_decl_assignments: net_decl_assignment { init($$); mto($$, $1); } @@ -1708,8 +1688,16 @@ range: part_select; // System Verilog standard 1800-2017 // A.2.4 Declaration assignments -net_decl_assignment: net_identifier '=' expression - { $$ = $1; stack_expr($$).id(ID_declarator); addswap($$, ID_value, $3); } +net_decl_assignment: + net_identifier unpacked_dimension_brace + { $$ = $1; + stack_expr($$).id(ID_declarator); + addswap($$, ID_type, $2); } + | net_identifier unpacked_dimension_brace '=' expression + { $$ = $1; + stack_expr($$).id(ID_declarator); + addswap($$, ID_type, $2); + addswap($$, ID_value, $4); } ; variable_decl_assignment: From 975fb1ed455c94ac028282b7a9a52e8a35d07e35 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Fri, 15 Mar 2024 16:03:42 -0700 Subject: [PATCH 4/5] Verilog: move array_type method into verilog_typecheck_exprt This moves the verilog_typecheckt::array_type method to verilog_typecheck_exprt, together with the other type conversion methods. --- src/verilog/verilog_typecheck.cpp | 74 -------------------------- src/verilog/verilog_typecheck.h | 4 -- src/verilog/verilog_typecheck_expr.h | 1 + src/verilog/verilog_typecheck_type.cpp | 73 +++++++++++++++++++++++++ 4 files changed, 74 insertions(+), 78 deletions(-) diff --git a/src/verilog/verilog_typecheck.cpp b/src/verilog/verilog_typecheck.cpp index a9a51a3e5..c6352a498 100644 --- a/src/verilog/verilog_typecheck.cpp +++ b/src/verilog/verilog_typecheck.cpp @@ -28,80 +28,6 @@ Author: Daniel Kroening, kroening@kroening.com /*******************************************************************\ -Function: verilog_typecheckt::array_type - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -array_typet verilog_typecheckt::array_type( - const irept &src, - const typet &element_type) -{ - // int whatnot[x:y]; - // 'src' is yet to be converted, but 'element_type' is already converted. - PRECONDITION(src.id() == ID_verilog_unpacked_array); - - // Unpacked arrays may have a range [x:y], - // or a size [s], equivalent to [0:s-1] - const exprt &range_expr = static_cast(src.find(ID_range)); - const exprt &size_expr = static_cast(src.find(ID_size)); - - mp_integer size, offset; - bool little_endian; - - if(range_expr.is_not_nil()) - { - // these may be negative - mp_integer msb, lsb; - convert_range(range_expr, msb, lsb); - little_endian = (lsb <= msb); - size = (little_endian ? msb - lsb : lsb - msb) + 1; - offset = little_endian ? lsb : msb; - } - else if(size_expr.is_not_nil()) - { - little_endian = true; - size = convert_integer_constant_expression(size_expr); - offset = 0; - if(size < 0) - { - throw errort().with_location(size_expr.find_source_location()) - << "array size must be nonnegative"; - } - } - else - { - throw errort() << "array must have range or size"; - } - - const typet src_subtype = - static_cast(src).has_subtype() - ? static_cast(src).subtype() - : typet(ID_nil); - - typet array_subtype; - - // may need to go recursive - if(src_subtype.is_nil()) - array_subtype=element_type; - else - array_subtype=array_type(src_subtype, element_type); - - const exprt final_size_expr = from_integer(size, integer_typet()); - array_typet result(array_subtype, final_size_expr); - result.set(ID_offset, from_integer(offset, integer_typet())); - result.set(ID_C_little_endian, little_endian); - - return result; -} - -/*******************************************************************\ - Function: verilog_typecheckt::typecheck_port_connection Inputs: diff --git a/src/verilog/verilog_typecheck.h b/src/verilog/verilog_typecheck.h index a4cf42d75..d01b1c63e 100644 --- a/src/verilog/verilog_typecheck.h +++ b/src/verilog/verilog_typecheck.h @@ -125,10 +125,6 @@ class verilog_typecheckt: void interface_generate_block(const class verilog_generate_blockt &); void interface_statement(const class verilog_statementt &); - array_typet array_type( - const irept &src, - const typet &element_type); - // type checking typedef enum { A_CONTINUOUS, A_BLOCKING, A_NON_BLOCKING } vassignt; diff --git a/src/verilog/verilog_typecheck_expr.h b/src/verilog/verilog_typecheck_expr.h index 3fe66242c..8ce588850 100644 --- a/src/verilog/verilog_typecheck_expr.h +++ b/src/verilog/verilog_typecheck_expr.h @@ -64,6 +64,7 @@ class verilog_typecheck_exprt:public verilog_typecheck_baset typet convert_type(const typet &); typet convert_enum(const class verilog_enum_typet &); + array_typet array_type(const irept &src, const typet &element_type); void convert_range( const exprt &range, diff --git a/src/verilog/verilog_typecheck_type.cpp b/src/verilog/verilog_typecheck_type.cpp index f155e52a5..0e0f5b57d 100644 --- a/src/verilog/verilog_typecheck_type.cpp +++ b/src/verilog/verilog_typecheck_type.cpp @@ -16,6 +16,79 @@ Author: Daniel Kroening, kroening@kroening.com /*******************************************************************\ +Function: verilog_typecheck_exprt::array_type + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +array_typet +verilog_typecheck_exprt::array_type(const irept &src, const typet &element_type) +{ + // int whatnot[x:y]; + // 'src' is yet to be converted, but 'element_type' is already converted. + PRECONDITION(src.id() == ID_verilog_unpacked_array); + + // Unpacked arrays may have a range [x:y], + // or a size [s], equivalent to [0:s-1] + const exprt &range_expr = static_cast(src.find(ID_range)); + const exprt &size_expr = static_cast(src.find(ID_size)); + + mp_integer size, offset; + bool little_endian; + + if(range_expr.is_not_nil()) + { + // these may be negative + mp_integer msb, lsb; + convert_range(range_expr, msb, lsb); + little_endian = (lsb <= msb); + size = (little_endian ? msb - lsb : lsb - msb) + 1; + offset = little_endian ? lsb : msb; + } + else if(size_expr.is_not_nil()) + { + little_endian = true; + size = convert_integer_constant_expression(size_expr); + offset = 0; + if(size < 0) + { + throw errort().with_location(size_expr.find_source_location()) + << "array size must be nonnegative"; + } + } + else + { + throw errort() << "array must have range or size"; + } + + const typet src_subtype = + static_cast(src).has_subtype() + ? static_cast(src).subtype() + : typet(ID_nil); + + typet array_subtype; + + // may need to go recursive + if(src_subtype.is_nil()) + array_subtype = element_type; + else + array_subtype = array_type(src_subtype, element_type); + + const exprt final_size_expr = from_integer(size, integer_typet()); + array_typet result(array_subtype, final_size_expr); + result.set(ID_offset, from_integer(offset, integer_typet())); + result.set(ID_C_little_endian, little_endian); + + return result; +} + +/*******************************************************************\ + Function: verilog_typecheck_exprt::convert_type Inputs: From 0844c0b1a183840f9064f80d2d64a160740f711c Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Wed, 20 Mar 2024 16:06:52 -0700 Subject: [PATCH 5/5] Verilog: rename array_type method to unpacked_array_type --- src/verilog/verilog_elaborate.cpp | 6 +++--- src/verilog/verilog_typecheck_expr.h | 2 +- src/verilog/verilog_typecheck_type.cpp | 12 +++++++----- 3 files changed, 11 insertions(+), 9 deletions(-) diff --git a/src/verilog/verilog_elaborate.cpp b/src/verilog/verilog_elaborate.cpp index cf7561c6a..9cc0a7f4c 100644 --- a/src/verilog/verilog_elaborate.cpp +++ b/src/verilog/verilog_elaborate.cpp @@ -236,7 +236,7 @@ void verilog_typecheckt::collect_symbols(const verilog_declt &decl) if(declarator.type().is_nil()) symbol.type = type; else if(declarator.type().id() == ID_verilog_unpacked_array) - symbol.type = array_type(declarator.type(), type); + symbol.type = unpacked_array_type(declarator.type(), type); else { throw errort().with_location(declarator.source_location()) @@ -423,7 +423,7 @@ void verilog_typecheckt::collect_symbols(const verilog_declt &decl) if(declarator.type().is_nil()) symbol.type = type; else if(declarator.type().id() == ID_verilog_unpacked_array) - symbol.type = array_type(declarator.type(), type); + symbol.type = unpacked_array_type(declarator.type(), type); else { throw errort().with_location(symbol.location) @@ -490,7 +490,7 @@ void verilog_typecheckt::collect_symbols(const verilog_declt &decl) if(declarator.type().is_nil()) symbol.type = type; else if(declarator.type().id() == ID_verilog_unpacked_array) - symbol.type = array_type(declarator.type(), type); + symbol.type = unpacked_array_type(declarator.type(), type); else { throw errort().with_location(symbol.location) diff --git a/src/verilog/verilog_typecheck_expr.h b/src/verilog/verilog_typecheck_expr.h index 8ce588850..99ba701da 100644 --- a/src/verilog/verilog_typecheck_expr.h +++ b/src/verilog/verilog_typecheck_expr.h @@ -64,7 +64,7 @@ class verilog_typecheck_exprt:public verilog_typecheck_baset typet convert_type(const typet &); typet convert_enum(const class verilog_enum_typet &); - array_typet array_type(const irept &src, const typet &element_type); + array_typet unpacked_array_type(const typet &src, const typet &element_type); void convert_range( const exprt &range, diff --git a/src/verilog/verilog_typecheck_type.cpp b/src/verilog/verilog_typecheck_type.cpp index 0e0f5b57d..f595bbada 100644 --- a/src/verilog/verilog_typecheck_type.cpp +++ b/src/verilog/verilog_typecheck_type.cpp @@ -16,7 +16,7 @@ Author: Daniel Kroening, kroening@kroening.com /*******************************************************************\ -Function: verilog_typecheck_exprt::array_type +Function: verilog_typecheck_exprt::unpacked_array_type Inputs: @@ -26,8 +26,9 @@ Function: verilog_typecheck_exprt::array_type \*******************************************************************/ -array_typet -verilog_typecheck_exprt::array_type(const irept &src, const typet &element_type) +array_typet verilog_typecheck_exprt::unpacked_array_type( + const typet &src, + const typet &element_type) { // int whatnot[x:y]; // 'src' is yet to be converted, but 'element_type' is already converted. @@ -57,13 +58,14 @@ verilog_typecheck_exprt::array_type(const irept &src, const typet &element_type) offset = 0; if(size < 0) { + // The size must be positive. 1800-2017 7.4.2 throw errort().with_location(size_expr.find_source_location()) << "array size must be nonnegative"; } } else { - throw errort() << "array must have range or size"; + throw errort() << "unpacked array must have range or size"; } const typet src_subtype = @@ -77,7 +79,7 @@ verilog_typecheck_exprt::array_type(const irept &src, const typet &element_type) if(src_subtype.is_nil()) array_subtype = element_type; else - array_subtype = array_type(src_subtype, element_type); + array_subtype = unpacked_array_type(src_subtype, element_type); const exprt final_size_expr = from_integer(size, integer_typet()); array_typet result(array_subtype, final_size_expr);