@@ -81,6 +81,72 @@ array_typet verilog_typecheck_exprt::convert_unpacked_array_type(
8181
8282/* ******************************************************************\
8383
84+ Function: verilog_typecheck_exprt::convert_packed_array_type
85+
86+ Inputs:
87+
88+ Outputs:
89+
90+ Purpose:
91+
92+ \*******************************************************************/
93+
94+ typet verilog_typecheck_exprt::convert_packed_array_type (
95+ const type_with_subtypet &src)
96+ {
97+ PRECONDITION (src.id () == ID_verilog_packed_array);
98+
99+ const exprt &range = static_cast <const exprt &>(src.find (ID_range));
100+ const auto &source_location = src.source_location ();
101+
102+ mp_integer msb, lsb;
103+ convert_range (range, msb, lsb);
104+
105+ bool big_endian = (lsb > msb);
106+
107+ mp_integer width = (big_endian ? lsb - msb : msb - lsb) + 1 ;
108+ mp_integer offset = big_endian ? msb : lsb;
109+
110+ // let's look at the subtype
111+ const auto subtype =
112+ static_cast <const typet &>(src).has_subtype ()
113+ ? static_cast <const type_with_subtypet &>(src).subtype ()
114+ : typet (ID_nil);
115+
116+ if (
117+ subtype.is_nil () || subtype.id () == ID_signed ||
118+ subtype.id () == ID_unsigned || subtype.id () == ID_verilog_bit ||
119+ subtype.id () == ID_verilog_logic)
120+ {
121+ // we have a bit-vector type, not an array
122+
123+ bitvector_typet dest (
124+ subtype.id () == ID_signed ? ID_signedbv : ID_unsignedbv);
125+
126+ dest.add_source_location () = source_location;
127+ dest.set_width (width.to_ulong ());
128+ dest.set (ID_C_big_endian, big_endian);
129+ dest.set (ID_C_offset, integer2string (offset));
130+
131+ return std::move (dest).with_source_location (source_location);
132+ }
133+ else
134+ {
135+ // We have a multi-dimensional packed array,
136+ // and do a recursive call.
137+ const exprt size = from_integer (width, integer_typet ());
138+ typet s = convert_type (subtype);
139+
140+ array_typet result (s, size);
141+ result.add_source_location () = source_location;
142+ result.set (ID_offset, from_integer (offset, integer_typet ()));
143+
144+ return std::move (result).with_source_location (source_location);
145+ }
146+ }
147+
148+ /* ******************************************************************\
149+
84150Function: verilog_typecheck_exprt::convert_type
85151
86152 Inputs:
@@ -178,51 +244,7 @@ typet verilog_typecheck_exprt::convert_type(const typet &src)
178244 }
179245 else if (src.id () == ID_verilog_packed_array)
180246 {
181- const exprt &range=static_cast <const exprt &>(src.find (ID_range));
182-
183- mp_integer msb, lsb;
184- convert_range (range, msb, lsb);
185-
186- bool big_endian = (lsb > msb);
187-
188- mp_integer width = (big_endian ? lsb - msb : msb - lsb) + 1 ;
189- mp_integer offset = big_endian ? msb : lsb;
190-
191- // let's look at the subtype
192- const auto subtype =
193- static_cast <const typet &>(src).has_subtype ()
194- ? static_cast <const type_with_subtypet &>(src).subtype ()
195- : typet (ID_nil);
196-
197- if (
198- subtype.is_nil () || subtype.id () == ID_signed ||
199- subtype.id () == ID_unsigned || subtype.id () == ID_verilog_bit ||
200- subtype.id () == ID_verilog_logic)
201- {
202- // we have a bit-vector type, not an array
203-
204- bitvector_typet dest (subtype.id ()==ID_signed?ID_signedbv:ID_unsignedbv);
205-
206- dest.add_source_location () = source_location;
207- dest.set_width (width.to_ulong ());
208- dest.set (ID_C_big_endian, big_endian);
209- dest.set (ID_C_offset, integer2string (offset));
210-
211- return std::move (dest).with_source_location (source_location);
212- }
213- else
214- {
215- // We have a multi-dimensional packed array,
216- // and do a recursive call.
217- const exprt size=from_integer (width, integer_typet ());
218- typet s=convert_type (subtype);
219-
220- array_typet result (s, size);
221- result.add_source_location () = source_location;
222- result.set (ID_offset, from_integer (offset, integer_typet ()));
223-
224- return std::move (result).with_source_location (source_location);
225- }
247+ return convert_packed_array_type (to_type_with_subtype (src));
226248 }
227249 else if (src.id () == ID_verilog_unpacked_array)
228250 {
0 commit comments