diff --git a/regression/verilog/data-types/queue1.desc b/regression/verilog/data-types/queue1.desc index 92e35926..360fe4c7 100644 --- a/regression/verilog/data-types/queue1.desc +++ b/regression/verilog/data-types/queue1.desc @@ -1,8 +1,8 @@ -KNOWNBUG +CORE queue1.sv -^EXIT=0$ +^no properties$ +^EXIT=10$ ^SIGNAL=0$ -- -- -Parsing fails. diff --git a/regression/verilog/data-types/queue1.sv b/regression/verilog/data-types/queue1.sv index 5fb1508a..8d3f66ee 100644 --- a/regression/verilog/data-types/queue1.sv +++ b/regression/verilog/data-types/queue1.sv @@ -1,6 +1,6 @@ module main; byte queue_of_bytes[$]; - string queue_of_strings[$:10] = { "foobar" }; + string queue_of_strings[$:10]; endmodule diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h index 7efff7d9..c405df8d 100644 --- a/src/hw_cbmc_irep_ids.h +++ b/src/hw_cbmc_irep_ids.h @@ -94,6 +94,7 @@ IREP_ID_ONE(verilog_inside) IREP_ID_ONE(verilog_unique) IREP_ID_ONE(verilog_unique0) IREP_ID_ONE(verilog_priority) +IREP_ID_ONE(verilog_queue) IREP_ID_ONE(verilog_new) IREP_ID_ONE(verilog_non_indexed_part_select) IREP_ID_ONE(verilog_indexed_part_select_plus) diff --git a/src/verilog/expr2verilog.cpp b/src/verilog/expr2verilog.cpp index 23515ab8..50723f0e 100644 --- a/src/verilog/expr2verilog.cpp +++ b/src/verilog/expr2verilog.cpp @@ -2074,6 +2074,12 @@ std::string expr2verilogt::convert(const typet &type) { return "enum"; } + else if(type.id() == ID_verilog_queue) + { + std::string dest = "queue of "; + dest += convert(to_type_with_subtype(type).subtype()); + return dest; + } else if(type.id() == ID_struct) { return "struct"; diff --git a/src/verilog/parser.y b/src/verilog/parser.y index dd31f867..d8f6d5dc 100644 --- a/src/verilog/parser.y +++ b/src/verilog/parser.y @@ -2114,6 +2114,7 @@ variable_dimension: unsized_dimension | unpacked_dimension | associative_dimension + | queue_dimension ; variable_dimension_brace: @@ -2126,6 +2127,13 @@ variable_dimension_brace: } ; +queue_dimension: + '[' '$' ']' + { init($$, ID_verilog_queue); stack_type($$).add_subtype().make_nil(); } + | '[' '$' TOK_COLON constant_expression ']' + { init($$, ID_verilog_queue); stack_type($$).add_subtype().make_nil(); } + ; + unsized_dimension: '[' ']' { init($$, "unsized"); } ; diff --git a/src/verilog/verilog_elaborate_type.cpp b/src/verilog/verilog_elaborate_type.cpp index f297f7b6..0dd006c2 100644 --- a/src/verilog/verilog_elaborate_type.cpp +++ b/src/verilog/verilog_elaborate_type.cpp @@ -461,6 +461,13 @@ typet verilog_typecheck_exprt::elaborate_type(const typet &src) // package::typedef return elaborate_package_scope_typedef(to_verilog_package_scope_type(src)); } + else if(src.id() == ID_verilog_queue) + { + // The subtype is the element type. + auto tmp = to_type_with_subtype(src); + tmp.subtype() = elaborate_type(tmp.subtype()); + return std::move(tmp); + } else { throw errort().with_location(source_location) diff --git a/src/verilog/verilog_expr.cpp b/src/verilog/verilog_expr.cpp index 09660fe0..f0b4d8fd 100644 --- a/src/verilog/verilog_expr.cpp +++ b/src/verilog/verilog_expr.cpp @@ -35,7 +35,7 @@ typet verilog_declaratort::merged_type(const typet &declaration_type) const typet *p = &result; while(p->id() == ID_verilog_unpacked_array || - p->id() == ID_verilog_associative_array) + p->id() == ID_verilog_associative_array || p->id() == ID_verilog_queue) { p = &to_type_with_subtype(*p).subtype(); }