cprover
Loading...
Searching...
No Matches
c_typecheck_initializer.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: ANSI-C Conversion / Type Checking
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#include "c_typecheck_base.h"
13
14#include <util/arith_tools.h>
15#include <util/byte_operators.h>
16#include <util/c_types.h>
17#include <util/config.h>
18#include <util/cprover_prefix.h>
20#include <util/prefix.h>
21#include <util/std_types.h>
23
24#include "anonymous_member.h"
25
27 exprt &initializer,
28 const typet &type,
29 bool force_constant)
30{
31 exprt result=do_initializer_rec(initializer, type, force_constant);
32
33 if(type.id()==ID_array)
34 {
35 const typet &result_type = result.type();
36 DATA_INVARIANT(result_type.id()==ID_array &&
37 to_array_type(result_type).size().is_not_nil(),
38 "any array must have a size");
39
40 // we don't allow initialisation with symbols of array type
41 if(
42 result.id() != ID_array && result.id() != ID_array_of &&
43 result.id() != ID_compound_literal)
44 {
46 error() << "invalid array initializer " << to_string(result)
47 << eom;
48 throw 0;
49 }
50 }
51
52 initializer=result;
53}
54
57 const exprt &value,
58 const typet &type,
59 bool force_constant)
60{
61 const typet &full_type=follow(type);
62
63 if(
64 (full_type.id() == ID_struct || full_type.id() == ID_union) &&
65 to_struct_union_type(full_type).is_incomplete())
66 {
68 error() << "type '" << to_string(type)
69 << "' is still incomplete -- cannot initialize" << eom;
70 throw 0;
71 }
72
73 if(value.id()==ID_initializer_list)
74 return do_initializer_list(value, type, force_constant);
75
76 if(
77 value.id() == ID_array && value.get_bool(ID_C_string_constant) &&
78 full_type.id() == ID_array &&
79 (to_array_type(full_type).element_type().id() == ID_signedbv ||
80 to_array_type(full_type).element_type().id() == ID_unsignedbv) &&
81 to_bitvector_type(to_array_type(full_type).element_type()).get_width() ==
83 {
84 exprt tmp=value;
85
86 // adjust char type
88 to_array_type(full_type).element_type();
89
90 Forall_operands(it, tmp)
91 it->type() = to_array_type(full_type).element_type();
92
93 if(full_type.id()==ID_array &&
94 to_array_type(full_type).is_complete())
95 {
96 const auto &array_type = to_array_type(full_type);
97
98 // check size
99 const auto array_size = numeric_cast<mp_integer>(array_type.size());
100 if(!array_size.has_value())
101 {
103 error() << "array size needs to be constant, got "
104 << to_string(array_type.size()) << eom;
105 throw 0;
106 }
107
108 if(*array_size < 0)
109 {
111 error() << "array size must not be negative" << eom;
112 throw 0;
113 }
114
115 if(mp_integer(tmp.operands().size()) > *array_size)
116 {
117 // cut off long strings. gcc does a warning for this
118 tmp.operands().resize(numeric_cast_v<std::size_t>(*array_size));
119 tmp.type()=type;
120 }
121 else if(mp_integer(tmp.operands().size()) < *array_size)
122 {
123 // fill up
124 tmp.type()=type;
125 const auto zero = zero_initializer(
126 array_type.element_type(), value.source_location(), *this);
127 if(!zero.has_value())
128 {
130 error() << "cannot zero-initialize array with subtype '"
131 << to_string(array_type.element_type()) << "'" << eom;
132 throw 0;
133 }
134 tmp.operands().resize(numeric_cast_v<std::size_t>(*array_size), *zero);
135 }
136 }
137
138 return tmp;
139 }
140
141 if(
142 value.id() == ID_string_constant && full_type.id() == ID_array &&
143 (to_array_type(full_type).element_type().id() == ID_signedbv ||
144 to_array_type(full_type).element_type().id() == ID_unsignedbv) &&
145 to_bitvector_type(to_array_type(full_type).element_type()).get_width() ==
146 char_type().get_width())
147 {
148 // will go away, to be replaced by the above block
149
151 // adjust char type
152 tmp1.type().subtype() = to_array_type(full_type).element_type();
153
154 exprt tmp2=tmp1.to_array_expr();
155
156 if(full_type.id()==ID_array &&
157 to_array_type(full_type).is_complete())
158 {
159 // check size
160 const auto array_size =
161 numeric_cast<mp_integer>(to_array_type(full_type).size());
162 if(!array_size.has_value())
163 {
165 error() << "array size needs to be constant, got "
166 << to_string(to_array_type(full_type).size()) << eom;
167 throw 0;
168 }
169
170 if(*array_size < 0)
171 {
173 error() << "array size must not be negative" << eom;
174 throw 0;
175 }
176
177 if(mp_integer(tmp2.operands().size()) > *array_size)
178 {
179 // cut off long strings. gcc does a warning for this
180 tmp2.operands().resize(numeric_cast_v<std::size_t>(*array_size));
181 tmp2.type()=type;
182 }
183 else if(mp_integer(tmp2.operands().size()) < *array_size)
184 {
185 // fill up
186 tmp2.type()=type;
187 const auto zero = zero_initializer(
188 to_array_type(full_type).element_type(),
189 value.source_location(),
190 *this);
191 if(!zero.has_value())
192 {
194 error() << "cannot zero-initialize array with subtype '"
195 << to_string(to_array_type(full_type).element_type()) << "'"
196 << eom;
197 throw 0;
198 }
199 tmp2.operands().resize(numeric_cast_v<std::size_t>(*array_size), *zero);
200 }
201 }
202
203 return tmp2;
204 }
205
206 if(full_type.id()==ID_array &&
207 to_array_type(full_type).size().is_nil())
208 {
210 error() << "type '" << to_string(full_type)
211 << "' cannot be initialized with '" << to_string(value) << "'"
212 << eom;
213 throw 0;
214 }
215
216 if(value.id()==ID_designated_initializer)
217 {
219 error() << "type '" << to_string(full_type)
220 << "' cannot be initialized with designated initializer" << eom;
221 throw 0;
222 }
223
224 exprt result=value;
226 return result;
227}
228
230{
231 // this one doesn't need initialization
232 if(has_prefix(id2string(symbol.name), CPROVER_PREFIX "constant_infinity"))
233 return;
234
235 if(symbol.is_static_lifetime)
236 {
237 if(symbol.value.is_not_nil())
238 {
239 typecheck_expr(symbol.value);
240 do_initializer(symbol.value, symbol.type, true);
241
242 // need to adjust size?
243 if(
244 symbol.type.id() == ID_array &&
245 to_array_type(symbol.type).size().is_nil())
246 symbol.type=symbol.value.type();
247 }
248 }
249 else if(!symbol.is_type)
250 {
251 if(symbol.is_macro)
252 {
253 // these must have a constant value
254 assert(symbol.value.is_not_nil());
255 typecheck_expr(symbol.value);
256 source_locationt location=symbol.value.source_location();
257 do_initializer(symbol.value, symbol.type, true);
258 make_constant(symbol.value);
259 }
260 else if(symbol.value.is_not_nil())
261 {
262 typecheck_expr(symbol.value);
263 do_initializer(symbol.value, symbol.type, true);
264
265 // need to adjust size?
266 if(
267 symbol.type.id() == ID_array &&
268 to_array_type(symbol.type).size().is_nil())
269 symbol.type=symbol.value.type();
270 }
271 }
272}
273
275 const typet &type,
276 designatort &designator)
277{
278 designatort::entryt entry(type);
279
280 const typet &full_type=follow(type);
281
282 if(full_type.id()==ID_struct)
283 {
284 const struct_typet &struct_type=to_struct_type(full_type);
285
286 entry.size=struct_type.components().size();
287 entry.subtype.make_nil();
288 // only a top-level struct may end with a variable-length array
289 entry.vla_permitted=designator.empty();
290
291 for(const auto &c : struct_type.components())
292 {
293 if(c.type().id() != ID_code && !c.get_is_padding())
294 {
295 entry.subtype = c.type();
296 break;
297 }
298
299 ++entry.index;
300 }
301 }
302 else if(full_type.id()==ID_union)
303 {
304 const union_typet &union_type=to_union_type(full_type);
305
306 if(union_type.components().empty())
307 {
308 entry.size=0;
309 entry.subtype.make_nil();
310 }
311 else
312 {
313 // The default is to initialize using the first member of the
314 // union.
315 entry.size=1;
316 entry.subtype=union_type.components().front().type();
317 }
318 }
319 else if(full_type.id()==ID_array)
320 {
321 const array_typet &array_type=to_array_type(full_type);
322
323 if(array_type.size().is_nil())
324 {
325 entry.size=0;
326 entry.subtype = array_type.element_type();
327 }
328 else
329 {
330 const auto array_size = numeric_cast<mp_integer>(array_type.size());
331 if(!array_size.has_value())
332 {
333 error().source_location = array_type.size().source_location();
334 error() << "array has non-constant size '"
335 << to_string(array_type.size()) << "'" << eom;
336 throw 0;
337 }
338
339 entry.size = numeric_cast_v<std::size_t>(*array_size);
340 entry.subtype = array_type.element_type();
341 }
342 }
343 else if(full_type.id()==ID_vector)
344 {
345 const vector_typet &vector_type=to_vector_type(full_type);
346
347 const auto vector_size = numeric_cast<mp_integer>(vector_type.size());
348
349 if(!vector_size.has_value())
350 {
351 error().source_location = vector_type.size().source_location();
352 error() << "vector has non-constant size '"
353 << to_string(vector_type.size()) << "'" << eom;
354 throw 0;
355 }
356
357 entry.size = numeric_cast_v<std::size_t>(*vector_size);
358 entry.subtype = vector_type.element_type();
359 }
360 else
362
363 designator.push_entry(entry);
364}
365
366exprt::operandst::const_iterator c_typecheck_baset::do_designated_initializer(
367 exprt &result,
368 designatort &designator,
369 const exprt &initializer_list,
370 exprt::operandst::const_iterator init_it,
371 bool force_constant)
372{
373 // copy the value, we may need to adjust it
374 exprt value=*init_it;
375
376 assert(!designator.empty());
377
378 if(value.id()==ID_designated_initializer)
379 {
380 assert(value.operands().size()==1);
381
382 designator=
384 designator.front().type,
385 static_cast<const exprt &>(value.find(ID_designator)));
386
387 assert(!designator.empty());
388
389 // discard the return value
391 result, designator, value, value.operands().begin(), force_constant);
392 return ++init_it;
393 }
394
395 exprt *dest=&result;
396
397 // first phase: follow given designator
398
399 for(size_t i=0; i<designator.size(); i++)
400 {
401 size_t index=designator[i].index;
402 const typet &type=designator[i].type;
403 const typet &full_type=follow(type);
404
405 if(full_type.id()==ID_array ||
406 full_type.id()==ID_vector)
407 {
408 // zero_initializer may have built an array_of expression for a large
409 // array; as we have a designated initializer we need to have an array of
410 // individual objects
411 if(dest->id() == ID_array_of)
412 {
413 const array_typet array_type = to_array_type(dest->type());
414 const auto array_size = numeric_cast<mp_integer>(array_type.size());
415 if(!array_size.has_value())
416 {
418 error() << "cannot zero-initialize array with element type '"
419 << to_string(to_type_with_subtype(full_type).subtype()) << "'"
420 << eom;
421 throw 0;
422 }
423 const exprt zero = to_array_of_expr(*dest).what();
424 *dest = array_exprt{{}, array_type};
425 dest->operands().resize(numeric_cast_v<std::size_t>(*array_size), zero);
426 }
427
428 if(index>=dest->operands().size())
429 {
430 if(full_type.id()==ID_array &&
431 (to_array_type(full_type).size().is_zero() ||
432 to_array_type(full_type).size().is_nil()))
433 {
434 // we are willing to grow an incomplete or zero-sized array
435 const auto zero = zero_initializer(
436 to_array_type(full_type).element_type(),
437 value.source_location(),
438 *this);
439 if(!zero.has_value())
440 {
442 error() << "cannot zero-initialize array with element type '"
443 << to_string(to_type_with_subtype(full_type).subtype())
444 << "'" << eom;
445 throw 0;
446 }
447 dest->operands().resize(
448 numeric_cast_v<std::size_t>(index) + 1, *zero);
449
450 // todo: adjust type!
451 }
452 else
453 {
455 error() << "array index designator " << index
456 << " out of bounds (" << dest->operands().size()
457 << ")" << eom;
458 throw 0;
459 }
460 }
461
462 dest = &(dest->operands()[numeric_cast_v<std::size_t>(index)]);
463 }
464 else if(full_type.id()==ID_struct)
465 {
466 const struct_typet::componentst &components=
467 to_struct_type(full_type).components();
468
469 if(index>=dest->operands().size())
470 {
472 error() << "structure member designator " << index
473 << " out of bounds (" << dest->operands().size()
474 << ")" << eom;
475 throw 0;
476 }
477
478 DATA_INVARIANT(index<components.size(),
479 "member designator is bounded by components size");
480 DATA_INVARIANT(components[index].type().id()!=ID_code &&
481 !components[index].get_is_padding(),
482 "member designator points at data member");
483
484 dest=&(dest->operands()[index]);
485 }
486 else if(full_type.id()==ID_union)
487 {
488 const union_typet &union_type=to_union_type(full_type);
489
490 const union_typet::componentst &components=
491 union_type.components();
492
493 if(components.empty())
494 {
496 error() << "union member designator found for empty union" << eom;
497 throw 0;
498 }
499 else if(init_it != initializer_list.operands().begin())
500 {
502 {
504 error() << "too many initializers" << eom;
505 throw 0;
506 }
507 else
508 {
510 warning() << "excess elements in union initializer" << eom;
511
512 return ++init_it;
513 }
514 }
515 else if(index >= components.size())
516 {
518 error() << "union member designator " << index << " out of bounds ("
519 << components.size() << ")" << eom;
520 throw 0;
521 }
522
523 const union_typet::componentt &component = components[index];
524
525 if(
526 dest->id() == ID_union &&
527 to_union_expr(*dest).get_component_name() == component.get_name())
528 {
529 // Already right union component. We can initialize multiple submembers,
530 // so do not overwrite this.
531 dest = &(to_union_expr(*dest).op());
532 }
533 else if(dest->id() == ID_union)
534 {
535 // The designated initializer does not initialize the maximum member,
536 // which the (default) zero initializer prepared. Replace this by a
537 // component-specific initializer; other bytes have an unspecified value
538 // (C Standard 6.2.6.1(7)). In practice, objects of static lifetime are
539 // fully zero initialized, so we just byte-update on top of the existing
540 // zero initializer.
541 const auto zero =
542 zero_initializer(component.type(), value.source_location(), *this);
543 if(!zero.has_value())
544 {
546 error() << "cannot zero-initialize union component of type '"
547 << to_string(component.type()) << "'" << eom;
548 throw 0;
549 }
550
552 {
553 byte_update_exprt byte_update =
554 make_byte_update(*dest, from_integer(0, c_index_type()), *zero);
555 byte_update.add_source_location() = value.source_location();
556 *dest = std::move(byte_update);
557 dest = &(to_byte_update_expr(*dest).op2());
558 }
559 else
560 {
561 union_exprt union_expr(component.get_name(), *zero, type);
562 union_expr.add_source_location() = value.source_location();
563 *dest = std::move(union_expr);
564 dest = &(to_union_expr(*dest).op());
565 }
566 }
567 else if(
568 dest->id() == ID_byte_update_big_endian ||
569 dest->id() == ID_byte_update_little_endian)
570 {
571 // handle the byte update introduced by an earlier initializer (if
572 // current_symbol.is_static_lifetime)
573 byte_update_exprt &byte_update = to_byte_update_expr(*dest);
574 dest = &byte_update.op2();
575 }
576 }
577 else
579 }
580
581 // second phase: assign value
582 // for this, we may need to go down, adding to the designator
583
584 while(true)
585 {
586 // see what type we have to initialize
587
588 const typet &type=designator.back().subtype;
589 const typet &full_type=follow(type);
590
591 // do we initialize a scalar?
592 if(full_type.id()!=ID_struct &&
593 full_type.id()!=ID_union &&
594 full_type.id()!=ID_array &&
595 full_type.id()!=ID_vector)
596 {
597 // The initializer for a scalar shall be a single expression,
598 // * optionally enclosed in braces. *
599
600 if(value.id()==ID_initializer_list &&
601 value.operands().size()==1)
602 {
603 *dest =
604 do_initializer_rec(to_unary_expr(value).op(), type, force_constant);
605 }
606 else
607 *dest=do_initializer_rec(value, type, force_constant);
608
609 assert(full_type==follow(dest->type()));
610
611 return ++init_it; // done
612 }
613
614 // union? The component in the zero initializer might
615 // not be the first one.
616 if(full_type.id()==ID_union)
617 {
618 const union_typet &union_type=to_union_type(full_type);
619
620 const union_typet::componentst &components=
621 union_type.components();
622
623 if(!components.empty())
624 {
626 union_type.components().front();
627
628 const auto zero =
629 zero_initializer(component.type(), value.source_location(), *this);
630 if(!zero.has_value())
631 {
633 error() << "cannot zero-initialize union component of type '"
634 << to_string(component.type()) << "'" << eom;
635 throw 0;
636 }
637 union_exprt union_expr(component.get_name(), *zero, type);
638 union_expr.add_source_location()=value.source_location();
639 *dest=union_expr;
640 }
641 }
642
643 // see what initializer we are given
644 if(value.id()==ID_initializer_list)
645 {
646 *dest=do_initializer_rec(value, type, force_constant);
647 return ++init_it; // done
648 }
649 else if(value.id()==ID_string_constant)
650 {
651 // We stop for initializers that are string-constants,
652 // which are like arrays. We only do so if we are to
653 // initialize an array of scalars.
654 if(
655 full_type.id() == ID_array &&
656 (to_array_type(full_type).element_type().id() == ID_signedbv ||
657 to_array_type(full_type).element_type().id() == ID_unsignedbv))
658 {
659 *dest=do_initializer_rec(value, type, force_constant);
660 return ++init_it; // done
661 }
662 }
663 else if(follow(value.type())==full_type)
664 {
665 // a struct/union/vector can be initialized directly with
666 // an expression of the right type. This doesn't
667 // work with arrays, unfortunately.
668 if(full_type.id()==ID_struct ||
669 full_type.id()==ID_union ||
670 full_type.id()==ID_vector)
671 {
672 *dest=value;
673 return ++init_it; // done
674 }
675 }
676
677 assert(full_type.id()==ID_struct ||
678 full_type.id()==ID_union ||
679 full_type.id()==ID_array ||
680 full_type.id()==ID_vector);
681
682 // we are initializing a compound type, and enter it!
683 // this may change the type, full_type might not be valid any more
684 const typet dest_type=full_type;
685 const bool vla_permitted=designator.back().vla_permitted;
686 designator_enter(type, designator);
687
688 // GCC permits (though issuing a warning with -Wall) composite
689 // types built from flat initializer lists
690 if(dest->operands().empty())
691 {
693 warning() << "initialisation of " << dest_type.id()
694 << " requires initializer list, found " << value.id()
695 << " instead" << eom;
696
697 // in case of a variable-length array consume all remaining
698 // initializer elements
699 if(vla_permitted &&
700 dest_type.id()==ID_array &&
701 (to_array_type(dest_type).size().is_zero() ||
702 to_array_type(dest_type).size().is_nil()))
703 {
704 value.id(ID_initializer_list);
705 value.operands().clear();
706 for( ; init_it!=initializer_list.operands().end(); ++init_it)
707 value.copy_to_operands(*init_it);
708 *dest=do_initializer_rec(value, dest_type, force_constant);
709
710 return init_it;
711 }
712 else
713 {
715 error() << "cannot initialize type '" << to_string(dest_type)
716 << "' using value '" << to_string(value) << "'" << eom;
717 throw 0;
718 }
719 }
720
721 dest = &(to_multi_ary_expr(*dest).op0());
722
723 // we run into another loop iteration
724 }
725
726 return ++init_it;
727}
728
730{
731 assert(!designator.empty());
732
733 while(true)
734 {
735 designatort::entryt &entry=designator[designator.size()-1];
736 const typet &full_type=follow(entry.type);
737
738 entry.index++;
739
740 if(full_type.id()==ID_array &&
741 to_array_type(full_type).size().is_nil())
742 return; // we will keep going forever
743
744 if(full_type.id()==ID_struct &&
745 entry.index<entry.size)
746 {
747 // need to adjust subtype
748 const struct_typet &struct_type=
749 to_struct_type(full_type);
750 const struct_typet::componentst &components=
751 struct_type.components();
752 assert(components.size()==entry.size);
753
754 // we skip over any padding or code
755 // we also skip over anonymous members
756 while(entry.index < entry.size &&
757 (components[entry.index].get_is_padding() ||
758 (components[entry.index].get_anonymous() &&
759 components[entry.index].type().id() != ID_struct_tag &&
760 components[entry.index].type().id() != ID_union_tag) ||
761 components[entry.index].type().id() == ID_code))
762 {
763 entry.index++;
764 }
765
766 if(entry.index<entry.size)
767 entry.subtype=components[entry.index].type();
768 }
769
770 if(entry.index<entry.size)
771 return; // done
772
773 if(designator.size()==1)
774 return; // done
775
776 // pop entry
777 designator.pop_entry();
778
779 assert(!designator.empty());
780 }
781}
782
784 const typet &src_type,
785 const exprt &src)
786{
787 assert(!src.operands().empty());
788
789 typet type=src_type;
790 designatort designator;
791
792 forall_operands(it, src)
793 {
794 const exprt &d_op=*it;
795 designatort::entryt entry(type);
796 const typet &full_type=follow(entry.type);
797
798 if(full_type.id()==ID_array)
799 {
800 if(d_op.id()!=ID_index)
801 {
803 error() << "expected array index designator" << eom;
804 throw 0;
805 }
806
807 exprt tmp_index = to_unary_expr(d_op).op();
808 make_constant_index(tmp_index);
809
810 mp_integer index, size;
811
812 if(to_integer(to_constant_expr(tmp_index), index))
813 {
815 error() << "expected constant array index designator" << eom;
816 throw 0;
817 }
818
819 if(to_array_type(full_type).size().is_nil())
820 size=0;
821 else if(
822 const auto size_opt =
823 numeric_cast<mp_integer>(to_array_type(full_type).size()))
824 size = *size_opt;
825 else
826 {
828 error() << "expected constant array size" << eom;
829 throw 0;
830 }
831
832 entry.index = numeric_cast_v<std::size_t>(index);
833 entry.size = numeric_cast_v<std::size_t>(size);
834 entry.subtype = to_array_type(full_type).element_type();
835 }
836 else if(full_type.id()==ID_struct ||
837 full_type.id()==ID_union)
838 {
839 const struct_union_typet &struct_union_type=
840 to_struct_union_type(full_type);
841
842 if(d_op.id()!=ID_member)
843 {
845 error() << "expected member designator" << eom;
846 throw 0;
847 }
848
849 const irep_idt &component_name=d_op.get(ID_component_name);
850
851 if(struct_union_type.has_component(component_name))
852 {
853 // a direct member
854 entry.index=struct_union_type.component_number(component_name);
855 entry.size=struct_union_type.components().size();
856 entry.subtype=struct_union_type.components()[entry.index].type();
857 }
858 else
859 {
860 // We will search for anonymous members,
861 // in a loop. This isn't supported by gcc, but icc does allow it.
862
863 bool found=false, repeat;
864 typet tmp_type=entry.type;
865
866 do
867 {
868 repeat=false;
869 std::size_t number = 0;
870 const struct_union_typet::componentst &components=
872
873 for(const auto &c : components)
874 {
875 if(c.get_name() == component_name)
876 {
877 // done!
878 entry.index=number;
879 entry.size=components.size();
880 entry.subtype = c.type();
881 entry.type=tmp_type;
882 }
883 else if(
884 c.get_anonymous() &&
885 (c.type().id() == ID_struct_tag ||
886 c.type().id() == ID_union_tag) &&
887 has_component_rec(c.type(), component_name, *this))
888 {
889 entry.index=number;
890 entry.size=components.size();
891 entry.subtype = c.type();
892 entry.type=tmp_type;
893 tmp_type=entry.subtype;
894 designator.push_entry(entry);
895 found=repeat=true;
896 break;
897 }
898
899 ++number;
900 }
901 }
902 while(repeat);
903
904 if(!found)
905 {
907 error() << "failed to find struct component '" << component_name
908 << "' in initialization of '" << to_string(struct_union_type)
909 << "'" << eom;
910 throw 0;
911 }
912 }
913 }
914 else
915 {
917 error() << "designated initializers cannot initialize '"
918 << to_string(full_type) << "'" << eom;
919 throw 0;
920 }
921
922 type=entry.subtype;
923 designator.push_entry(entry);
924 }
925
926 assert(!designator.empty());
927
928 return designator;
929}
930
932 const exprt &value,
933 const typet &type,
934 bool force_constant)
935{
936 assert(value.id()==ID_initializer_list);
937
938 const typet &full_type=follow(type);
939
940 // 6.7.9, 14: An array of character type may be initialized by a character
941 // string literal or UTF-8 string literal, optionally enclosed in braces.
942 if(
943 full_type.id() == ID_array && value.operands().size() >= 1 &&
944 to_multi_ary_expr(value).op0().id() == ID_string_constant &&
945 (to_array_type(full_type).element_type().id() == ID_signedbv ||
946 to_array_type(full_type).element_type().id() == ID_unsignedbv) &&
947 to_bitvector_type(to_array_type(full_type).element_type()).get_width() ==
948 char_type().get_width())
949 {
950 if(value.operands().size() > 1)
951 {
953 warning() << "ignoring excess initializers" << eom;
954 }
955
956 return do_initializer_rec(
957 to_multi_ary_expr(value).op0(), type, force_constant);
958 }
959
961 if(full_type.id()==ID_struct ||
962 full_type.id()==ID_union ||
963 full_type.id()==ID_vector)
964 {
965 // start with zero everywhere
966 const auto zero = zero_initializer(type, value.source_location(), *this);
967 if(!zero.has_value())
968 {
970 error() << "cannot zero-initialize '" << to_string(full_type) << "'"
971 << eom;
972 throw 0;
973 }
974 result = *zero;
975 }
976 else if(full_type.id()==ID_array)
977 {
978 if(to_array_type(full_type).size().is_nil())
979 {
980 // start with empty array
981 result=exprt(ID_array, full_type);
982 result.add_source_location()=value.source_location();
983 }
984 else
985 {
986 // start with zero everywhere
987 const auto zero = zero_initializer(type, value.source_location(), *this);
988 if(!zero.has_value())
989 {
991 error() << "cannot zero-initialize '" << to_string(full_type) << "'"
992 << eom;
993 throw 0;
994 }
995 result = *zero;
996 }
997 }
998 else
999 {
1000 // The initializer for a scalar shall be a single expression,
1001 // * optionally enclosed in braces. *
1002
1003 if(value.operands().size()==1)
1004 return do_initializer_rec(
1005 to_unary_expr(value).op(), type, force_constant);
1006
1008 error() << "cannot initialize '" << to_string(full_type)
1009 << "' with an initializer list" << eom;
1010 throw 0;
1011 }
1012
1013 designatort current_designator;
1014
1015 designator_enter(type, current_designator);
1016
1017 const exprt::operandst &operands=value.operands();
1018 for(exprt::operandst::const_iterator it=operands.begin();
1019 it!=operands.end(); ) // no ++it
1020 {
1022 result, current_designator, value, it, force_constant);
1023
1024 // increase designator -- might go up
1025 increment_designator(current_designator);
1026 }
1027
1028 // make sure we didn't mess up index computation
1029 if(full_type.id()==ID_struct)
1030 {
1031 assert(result.operands().size()==
1032 to_struct_type(full_type).components().size());
1033 }
1034
1035 if(full_type.id()==ID_array &&
1036 to_array_type(full_type).size().is_nil())
1037 {
1038 // make complete by setting array size
1039 size_t size=result.operands().size();
1040 result.type().id(ID_array);
1041 result.type().set(ID_size, from_integer(size, c_index_type()));
1042 }
1043
1044 return result;
1045}
bool has_component_rec(const typet &type, const irep_idt &component_name, const namespacet &ns)
C Language Type Checking.
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
bool to_integer(const constant_exprt &expr, mp_integer &int_value)
Convert a constant expression expr to an arbitrary-precision integer.
Definition: arith_tools.cpp:19
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Expression classes for byte-level operators.
const byte_update_exprt & to_byte_update_expr(const exprt &expr)
ANSI-C Language Type Checking.
bitvector_typet char_type()
Definition: c_types.cpp:124
bitvector_typet c_index_type()
Definition: c_types.cpp:16
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition: c_types.h:162
Array constructor from list of elements.
Definition: std_expr.h:1476
exprt & what()
Definition: std_expr.h:1428
Arrays with given size.
Definition: std_types.h:763
const exprt & size() const
Definition: std_types.h:790
const typet & element_type() const
The type of the elements of the array.
Definition: std_types.h:777
std::size_t get_width() const
Definition: std_types.h:864
Expression corresponding to op() where the bytes starting at position offset (given in number of byte...
virtual exprt do_initializer_list(const exprt &value, const typet &type, bool force_constant)
virtual void implicit_typecast(exprt &expr, const typet &type)
virtual exprt do_initializer_rec(const exprt &value, const typet &type, bool force_constant)
initialize something of type ‘type’ with given value ‘value’
virtual void typecheck_expr(exprt &expr)
virtual void do_initializer(exprt &initializer, const typet &type, bool force_constant)
virtual void make_constant(exprt &expr)
virtual std::string to_string(const exprt &expr)
void increment_designator(designatort &designator)
virtual exprt::operandst::const_iterator do_designated_initializer(exprt &result, designatort &designator, const exprt &initializer_list, exprt::operandst::const_iterator init_it, bool force_constant)
virtual void make_constant_index(exprt &expr)
designatort make_designator(const typet &type, const exprt &src)
void designator_enter(const typet &type, designatort &designator)
struct configt::ansi_ct ansi_c
const entryt & front() const
Definition: designator.h:41
size_t size() const
Definition: designator.h:37
void push_entry(const entryt &entry)
Definition: designator.h:45
const entryt & back() const
Definition: designator.h:40
bool empty() const
Definition: designator.h:36
void pop_entry()
Definition: designator.h:50
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
Definition: expr.cpp:165
std::vector< exprt > operandst
Definition: expr.h:56
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
Definition: expr.h:129
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:92
const source_locationt & source_location() const
Definition: expr.h:230
source_locationt & add_source_location()
Definition: expr.h:235
bool get_bool(const irep_idt &name) const
Definition: irep.cpp:58
const irept & find(const irep_idt &name) const
Definition: irep.cpp:106
const irep_idt & get(const irep_idt &name) const
Definition: irep.cpp:45
bool is_not_nil() const
Definition: irep.h:380
void make_nil()
Definition: irep.h:454
const irep_idt & id() const
Definition: irep.h:396
bool is_nil() const
Definition: irep.h:376
source_locationt source_location
Definition: message.h:247
mstreamt & error() const
Definition: message.h:399
mstreamt & warning() const
Definition: message.h:404
mstreamt & result() const
Definition: message.h:409
static eomt eom
Definition: message.h:297
exprt & op0()
Definition: std_expr.h:844
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:49
array_exprt to_array_expr() const
convert string into array constant
Structure type, corresponds to C style structs.
Definition: std_types.h:231
Base type for structs and unions.
Definition: std_types.h:62
const componentst & components() const
Definition: std_types.h:147
bool has_component(const irep_idt &component_name) const
Definition: std_types.h:157
std::size_t component_number(const irep_idt &component_name) const
Return the sequence number of the component with given name.
Definition: std_types.cpp:40
std::vector< componentt > componentst
Definition: std_types.h:140
Symbol table entry.
Definition: symbol.h:28
bool is_macro
Definition: symbol.h:61
bool is_static_lifetime
Definition: symbol.h:65
bool is_type
Definition: symbol.h:61
typet type
Type of symbol.
Definition: symbol.h:31
irep_idt name
The unique identifier.
Definition: symbol.h:40
exprt value
Initial value of symbol.
Definition: symbol.h:34
exprt & op2()
Definition: expr.h:105
The type of an expression, extends irept.
Definition: type.h:29
const typet & subtype() const
Definition: type.h:48
const exprt & op() const
Definition: std_expr.h:293
Union constructor from single element.
Definition: std_expr.h:1611
irep_idt get_component_name() const
Definition: std_expr.h:1619
The union type.
Definition: c_types.h:125
The vector type.
Definition: std_types.h:996
const constant_exprt & size() const
Definition: std_types.cpp:253
const typet & element_type() const
The type of the elements of the vector.
Definition: std_types.h:1006
configt config
Definition: config.cpp:25
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
#define CPROVER_PREFIX
#define forall_operands(it, expr)
Definition: expr.h:18
#define Forall_operands(it, expr)
Definition: expr.h:25
optionalt< exprt > zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns)
Create the equivalent of zero for type type.
Expression Initialization.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
BigInt mp_integer
Definition: smt_terms.h:12
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:510
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:48
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast an exprt to an array_of_exprt.
Definition: std_expr.h:1456
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:328
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
Definition: std_expr.h:899
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
Definition: std_expr.h:1657
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2840
Pre-defined types.
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition: std_types.h:1040
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:308
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:832
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition: std_types.h:214
const string_constantt & to_string_constant(const exprt &expr)
flavourt mode
Definition: config.h:222
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition: type.h:177
byte_update_exprt make_byte_update(const exprt &_op, const exprt &_offset, const exprt &_value)
Construct a byte_update_exprt with endianness and byte width matching the current configuration.