diff --git a/lib/cbmc b/lib/cbmc index fc4f7ca7..f2489e3e 160000 --- a/lib/cbmc +++ b/lib/cbmc @@ -1 +1 @@ -Subproject commit fc4f7ca71ddcbd290cea0d9ac58b6cc6f6b79cb0 +Subproject commit f2489e3edf77f95c5d43c4baf733607a073f8ccd 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 7a052d39..0ea3190f 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 f5ada047..7a51ce89 100644 --- a/src/verilog/verilog_elaborate_type.cpp +++ b/src/verilog/verilog_elaborate_type.cpp @@ -447,6 +447,13 @@ typet verilog_typecheck_exprt::elaborate_type(const typet &src) // package::typedef return elaborate_package_scope_typedef(to_type_with_subtypes(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 4358ca60..ea89f48c 100644 --- a/src/verilog/verilog_expr.cpp +++ b/src/verilog/verilog_expr.cpp @@ -34,7 +34,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(); }