diff --git a/regression/verilog/data-types/associative_array1.desc b/regression/verilog/data-types/associative_array1.desc index a36a5996..931f2900 100644 --- a/regression/verilog/data-types/associative_array1.desc +++ b/regression/verilog/data-types/associative_array1.desc @@ -1,8 +1,8 @@ -KNOWNBUG +CORE associative_array1.sv -^EXIT=0$ +^no properties$ +^EXIT=10$ ^SIGNAL=0$ -- -- -Parsing fails. diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h index 6de2e27f..97910226 100644 --- a/src/hw_cbmc_irep_ids.h +++ b/src/hw_cbmc_irep_ids.h @@ -78,6 +78,7 @@ IREP_ID_ONE(inst) IREP_ID_ONE(Verilog) IREP_ID_ONE(verilog_array_range) IREP_ID_ONE(verilog_assignment_pattern) +IREP_ID_ONE(verilog_associative_array) IREP_ID_ONE(verilog_declarations) IREP_ID_ONE(verilog_lifetime) IREP_ID_ONE(verilog_logical_equality) diff --git a/src/verilog/parser.y b/src/verilog/parser.y index 476dd85f..0c451cec 100644 --- a/src/verilog/parser.y +++ b/src/verilog/parser.y @@ -2055,6 +2055,24 @@ packed_dimension: | unsized_dimension ; +associative_dimension: + '[' data_type ']' + { init($$, ID_verilog_associative_array); + // for the element type + stack_type($$).add_subtype().make_nil(); + } + | '[' '*' ']' + { init($$, ID_verilog_associative_array); + // for the element type + stack_type($$).add_subtype().make_nil(); + } + | "[*" ']' + { init($$, ID_verilog_associative_array); + // for the element type + stack_type($$).add_subtype().make_nil(); + } + ; + unpacked_dimension: '[' const_expression TOK_COLON const_expression ']' { init($$, ID_verilog_unpacked_array); @@ -2073,6 +2091,7 @@ unpacked_dimension: variable_dimension: unsized_dimension | unpacked_dimension + | associative_dimension ; variable_dimension_brace: diff --git a/src/verilog/verilog_elaborate_type.cpp b/src/verilog/verilog_elaborate_type.cpp index 6c48c8f0..bb5273b3 100644 --- a/src/verilog/verilog_elaborate_type.cpp +++ b/src/verilog/verilog_elaborate_type.cpp @@ -210,6 +210,13 @@ typet verilog_typecheck_exprt::elaborate_type(const typet &src) return rec; } } + else if(src.id() == ID_verilog_associative_array) + { + // The subtype is the element type. + auto tmp = to_type_with_subtype(src); + tmp.subtype() = elaborate_type(tmp.subtype()); + return std::move(tmp); + } else if(src.id() == ID_verilog_byte) { // two-valued type, signed diff --git a/src/verilog/verilog_expr.cpp b/src/verilog/verilog_expr.cpp index faf88735..4358ca60 100644 --- a/src/verilog/verilog_expr.cpp +++ b/src/verilog/verilog_expr.cpp @@ -33,10 +33,16 @@ typet verilog_declaratort::merged_type(const typet &declaration_type) const typet result = type(); typet *p = &result; - while(p->id() == ID_verilog_unpacked_array) + while(p->id() == ID_verilog_unpacked_array || + p->id() == ID_verilog_associative_array) + { p = &to_type_with_subtype(*p).subtype(); + } + + DATA_INVARIANT( + p->is_nil(), + "merged_type only works on unpacked arrays and associative arrays"); - DATA_INVARIANT(p->is_nil(), "merged_type only works on unpacked arrays"); *p = declaration_type; return result;