CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
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 <util/arith_tools.h>
13#include <util/byte_operators.h>
14#include <util/c_types.h>
15#include <util/config.h>
16#include <util/cprover_prefix.h>
18#include <util/std_types.h>
21
22#include "anonymous_member.h"
23#include "c_typecheck_base.h"
24#include "type2name.h"
25
27 exprt &initializer,
28 const typet &type,
29 bool force_constant)
30{
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 &&
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 if(
62 (type.id() == ID_struct_tag &&
63 follow_tag(to_struct_tag_type(type)).is_incomplete()) ||
64 (type.id() == ID_union_tag &&
65 follow_tag(to_union_tag_type(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 type.id() == ID_array &&
79 (to_array_type(type).element_type().id() == ID_signedbv ||
80 to_array_type(type).element_type().id() == ID_unsignedbv) &&
81 to_bitvector_type(to_array_type(type).element_type()).get_width() ==
82 to_bitvector_type(to_array_type(value.type()).element_type()).get_width())
83 {
84 exprt tmp=value;
85
86 // adjust char type
87 to_array_type(tmp.type()).element_type() =
88 to_array_type(type).element_type();
89
91 it->type() = to_array_type(type).element_type();
92
93 if(type.id() == ID_array && to_array_type(type).is_complete())
94 {
95 const auto &array_type = to_array_type(type);
96
97 // check size
99 if(!array_size.has_value())
100 {
102 error() << "array size needs to be constant, got "
103 << to_string(array_type.size()) << eom;
104 throw 0;
105 }
106
107 if(*array_size < 0)
108 {
110 error() << "array size must not be negative" << eom;
111 throw 0;
112 }
113
114 if(mp_integer(tmp.operands().size()) > *array_size)
115 {
116 // cut off long strings. gcc does a warning for this
117 tmp.operands().resize(numeric_cast_v<std::size_t>(*array_size));
118 tmp.type()=type;
119 }
120 else if(mp_integer(tmp.operands().size()) < *array_size)
121 {
122 // fill up
123 tmp.type()=type;
124 const auto zero = zero_initializer(
125 array_type.element_type(), value.source_location(), *this);
126 if(!zero.has_value())
127 {
129 error() << "cannot zero-initialize array with subtype '"
130 << to_string(array_type.element_type()) << "'" << eom;
131 throw 0;
132 }
133 tmp.operands().resize(numeric_cast_v<std::size_t>(*array_size), *zero);
134 }
135 }
136
137 return tmp;
138 }
139
140 if(
141 value.id() == ID_string_constant && type.id() == ID_array &&
142 (to_array_type(type).element_type().id() == ID_signedbv ||
143 to_array_type(type).element_type().id() == ID_unsignedbv) &&
144 to_bitvector_type(to_array_type(type).element_type()).get_width() ==
145 char_type().get_width())
146 {
147 // will go away, to be replaced by the above block
148
150 // adjust char type
151 to_array_type(tmp1.type()).element_type() =
152 to_array_type(type).element_type();
153
154 exprt tmp2=tmp1.to_array_expr();
155
156 if(type.id() == ID_array && to_array_type(type).is_complete())
157 {
158 // check size
159 const auto array_size =
161 if(!array_size.has_value())
162 {
164 error() << "array size needs to be constant, got "
165 << to_string(to_array_type(type).size()) << eom;
166 throw 0;
167 }
168
169 if(*array_size < 0)
170 {
172 error() << "array size must not be negative" << eom;
173 throw 0;
174 }
175
176 if(mp_integer(tmp2.operands().size()) > *array_size)
177 {
178 // cut off long strings. gcc does a warning for this
179 tmp2.operands().resize(numeric_cast_v<std::size_t>(*array_size));
180 tmp2.type()=type;
181 }
182 else if(mp_integer(tmp2.operands().size()) < *array_size)
183 {
184 // fill up
185 tmp2.type()=type;
186 const auto zero = zero_initializer(
187 to_array_type(type).element_type(), value.source_location(), *this);
188 if(!zero.has_value())
189 {
191 error() << "cannot zero-initialize array with subtype '"
192 << to_string(to_array_type(type).element_type()) << "'"
193 << eom;
194 throw 0;
195 }
196 tmp2.operands().resize(numeric_cast_v<std::size_t>(*array_size), *zero);
197 }
198 }
199
200 return tmp2;
201 }
202
203 if(type.id() == ID_array && to_array_type(type).size().is_nil())
204 {
206 error() << "type '" << to_string(type) << "' cannot be initialized with '"
207 << to_string(value) << "'" << eom;
208 throw 0;
209 }
210
211 if(value.id()==ID_designated_initializer)
212 {
214 error() << "type '" << to_string(type)
215 << "' cannot be initialized with designated initializer" << eom;
216 throw 0;
217 }
218
219 exprt result=value;
221 return result;
222}
223
225{
226 // this one doesn't need initialization
227 if(symbol.name.starts_with(CPROVER_PREFIX "constant_infinity"))
228 return;
229
230 if(symbol.is_type)
231 return;
232
233 if(symbol.value.is_not_nil())
234 {
235 typecheck_expr(symbol.value);
236 do_initializer(symbol.value, symbol.type, true);
237
238 // A flexible array may have been initialized, which entails a type change.
239 // Note that the type equality test is important: we want to preserve
240 // annotations like typedefs or const-ness when the type is otherwise the
241 // same.
242 if(!symbol.is_macro && symbol.type != symbol.value.type())
243 symbol.type = symbol.value.type();
244 }
245
246 if(symbol.is_macro)
247 make_constant(symbol.value);
248}
249
251 const typet &type,
252 designatort &designator)
253{
254 designatort::entryt entry(type);
255
257 {
259
260 entry.size=struct_type.components().size();
261 entry.subtype.make_nil();
262 // only a top-level struct may end with a variable-length array
263 entry.vla_permitted=designator.empty();
264
265 for(const auto &c : struct_type.components())
266 {
268 c.type().id() != ID_code, "struct member must not be of code type");
269
270 if(
271 !c.get_is_padding() &&
272 (c.type().id() != ID_c_bit_field || !c.get_anonymous()))
273 {
274 entry.subtype = c.type();
275 break;
276 }
277
278 ++entry.index;
279 }
280 }
282 {
284
285 if(union_type.components().empty())
286 {
287 entry.size=0;
288 entry.subtype.make_nil();
289 }
290 else
291 {
292 // The default is to initialize using the first member of the
293 // union.
294 entry.size=1;
295 entry.subtype=union_type.components().front().type();
296 }
297 }
298 else if(type.id() == ID_array)
299 {
300 const array_typet &array_type = to_array_type(type);
301
302 if(array_type.size().is_nil())
303 {
304 entry.size=0;
305 entry.subtype = array_type.element_type();
306 }
307 else
308 {
310 if(!array_size.has_value())
311 {
312 error().source_location = array_type.size().source_location();
313 error() << "array has non-constant size '"
314 << to_string(array_type.size()) << "'" << eom;
315 throw 0;
316 }
317
319 entry.subtype = array_type.element_type();
320 }
321 }
322 else if(type.id() == ID_vector)
323 {
325
326 const auto vector_size = numeric_cast<mp_integer>(vector_type.size());
327
328 if(!vector_size.has_value())
329 {
330 error().source_location = vector_type.size().source_location();
331 error() << "vector has non-constant size '"
332 << to_string(vector_type.size()) << "'" << eom;
333 throw 0;
334 }
335
336 entry.size = numeric_cast_v<std::size_t>(*vector_size);
337 entry.subtype = vector_type.element_type();
338 }
339 else
341
342 designator.push_entry(entry);
343}
344
345exprt::operandst::const_iterator c_typecheck_baset::do_designated_initializer(
346 exprt &result,
347 designatort &designator,
348 const exprt &initializer_list,
349 exprt::operandst::const_iterator init_it,
350 bool force_constant)
351{
352 // copy the value, we may need to adjust it
353 exprt value=*init_it;
354
355 PRECONDITION(!designator.empty());
356
357 if(value.id()==ID_designated_initializer)
358 {
359 PRECONDITION(value.operands().size() == 1);
360
361 designator=
363 designator.front().type,
364 static_cast<const exprt &>(value.find(ID_designator)));
365
366 CHECK_RETURN(!designator.empty());
367
368 // discard the return value
370 result, designator, value, value.operands().begin(), force_constant);
371 return ++init_it;
372 }
373
374 exprt *dest=&result;
375
376 // first phase: follow given designator
377
378 for(size_t i=0; i<designator.size(); i++)
379 {
380 size_t index=designator[i].index;
381 const typet &type=designator[i].type;
382
383 if(type.id() == ID_array || type.id() == ID_vector)
384 {
385 // zero_initializer may have built an array_of expression for a large
386 // array; as we have a designated initializer we need to have an array of
387 // individual objects
388 if(dest->id() == ID_array_of)
389 {
390 const array_typet array_type = to_array_type(dest->type());
392 if(!array_size.has_value())
393 {
395 error() << "cannot zero-initialize array with element type '"
396 << to_string(to_type_with_subtype(type).subtype()) << "'"
397 << eom;
398 throw 0;
399 }
400 const exprt zero = to_array_of_expr(*dest).what();
401 *dest = array_exprt{{}, array_type};
402 dest->operands().resize(numeric_cast_v<std::size_t>(*array_size), zero);
403 }
404
405 if(index>=dest->operands().size())
406 {
407 if(
408 type.id() == ID_array && (to_array_type(type).size().is_zero() ||
409 to_array_type(type).size().is_nil()))
410 {
411 const typet &element_type = to_array_type(type).element_type();
412
413 // we are willing to grow an incomplete or zero-sized array --
414 // do_initializer_list will fix up the resulting type
415 const auto zero =
416 zero_initializer(element_type, value.source_location(), *this);
417 if(!zero.has_value())
418 {
420 error() << "cannot zero-initialize array with element type '"
421 << to_string(element_type) << "'" << eom;
422 throw 0;
423 }
424 dest->operands().resize(
425 numeric_cast_v<std::size_t>(index) + 1, *zero);
426 }
427 else
428 {
430 error() << "array index designator " << index
431 << " out of bounds (" << dest->operands().size()
432 << ")" << eom;
433 throw 0;
434 }
435 }
436
437 dest = &(dest->operands()[numeric_cast_v<std::size_t>(index)]);
438 }
439 else if(
441 {
442 const struct_typet::componentst &components =
443 follow_tag(*struct_tag_type).components();
444
445 if(index>=dest->operands().size())
446 {
448 error() << "structure member designator " << index
449 << " out of bounds (" << dest->operands().size()
450 << ")" << eom;
451 throw 0;
452 }
453
454 DATA_INVARIANT(index<components.size(),
455 "member designator is bounded by components size");
457 components[index].type().id() != ID_code,
458 "struct member must not be of code type");
460 !components[index].get_is_padding(),
461 "member designator points at non-padding member");
462
463 dest=&(dest->operands()[index]);
464 }
466 {
468
469 const union_typet::componentst &components=
470 union_type.components();
471
472 if(components.empty())
473 {
475 error() << "union member designator found for empty union" << eom;
476 throw 0;
477 }
478 else if(init_it != initializer_list.operands().begin())
479 {
481 {
483 error() << "too many initializers" << eom;
484 throw 0;
485 }
486 else
487 {
489 warning() << "excess elements in union initializer" << eom;
490
491 return ++init_it;
492 }
493 }
494 else if(index >= components.size())
495 {
497 error() << "union member designator " << index << " out of bounds ("
498 << components.size() << ")" << eom;
499 throw 0;
500 }
501
502 const union_typet::componentt &component = components[index];
503
504 if(
505 dest->id() == ID_union &&
506 to_union_expr(*dest).get_component_name() == component.get_name())
507 {
508 // Already right union component. We can initialize multiple submembers,
509 // so do not overwrite this.
510 dest = &(to_union_expr(*dest).op());
511 }
512 else if(dest->id() == ID_union)
513 {
514 // The designated initializer does not initialize the maximum member,
515 // which the (default) zero initializer prepared. Replace this by a
516 // component-specific initializer; other bytes have an unspecified value
517 // (C Standard 6.2.6.1(7)). In practice, objects of static lifetime are
518 // fully zero initialized, so we just byte-update on top of the existing
519 // zero initializer.
520 const auto zero =
521 zero_initializer(component.type(), value.source_location(), *this);
522 if(!zero.has_value())
523 {
525 error() << "cannot zero-initialize union component of type '"
526 << to_string(component.type()) << "'" << eom;
527 throw 0;
528 }
529
531 {
533 make_byte_update(*dest, from_integer(0, c_index_type()), *zero);
534 byte_update.add_source_location() = value.source_location();
535 *dest = std::move(byte_update);
536 dest = &(to_byte_update_expr(*dest).op2());
537 }
538 else
539 {
540 union_exprt union_expr(component.get_name(), *zero, type);
541 union_expr.add_source_location() = value.source_location();
542 *dest = std::move(union_expr);
543 dest = &(to_union_expr(*dest).op());
544 }
545 }
546 else if(
547 dest->id() == ID_byte_update_big_endian ||
549 {
550 // handle the byte update introduced by an earlier initializer (if
551 // current_symbol.is_static_lifetime)
553 dest = &byte_update.op2();
554 }
555 }
556 else
558 }
559
560 // second phase: assign value
561 // for this, we may need to go down, adding to the designator
562
563 while(true)
564 {
565 // see what type we have to initialize
566
567 const typet &type=designator.back().subtype;
568
569 // do we initialize a scalar?
570 if(
571 type.id() != ID_struct_tag && type.id() != ID_union_tag &&
572 type.id() != ID_array && type.id() != ID_vector)
573 {
574 // The initializer for a scalar shall be a single expression,
575 // * optionally enclosed in braces. *
576
577 if(value.id()==ID_initializer_list &&
578 value.operands().size()==1)
579 {
580 *dest =
582 }
583 else
584 *dest=do_initializer_rec(value, type, force_constant);
585
586 DATA_INVARIANT(type == dest->type(), "matching types");
587
588 return ++init_it; // done
589 }
590
591 // union? The component in the zero initializer might
592 // not be the first one.
594 {
596
597 const union_typet::componentst &components=
598 union_type.components();
599
600 if(!components.empty())
601 {
603 union_type.components().front();
604
605 const auto zero =
606 zero_initializer(component.type(), value.source_location(), *this);
607 if(!zero.has_value())
608 {
610 error() << "cannot zero-initialize union component of type '"
611 << to_string(component.type()) << "'" << eom;
612 throw 0;
613 }
614 union_exprt union_expr(component.get_name(), *zero, type);
615 union_expr.add_source_location()=value.source_location();
616 *dest=union_expr;
617 }
618 }
619
620 // see what initializer we are given
621 if(value.id()==ID_initializer_list)
622 {
623 *dest=do_initializer_rec(value, type, force_constant);
624 return ++init_it; // done
625 }
626 else if(value.id()==ID_string_constant)
627 {
628 // We stop for initializers that are string-constants,
629 // which are like arrays. We only do so if we are to
630 // initialize an array of scalars.
631 if(
632 type.id() == ID_array &&
633 (to_array_type(type).element_type().id() == ID_signedbv ||
634 to_array_type(type).element_type().id() == ID_unsignedbv))
635 {
636 *dest=do_initializer_rec(value, type, force_constant);
637 return ++init_it; // done
638 }
639 }
640 else if(value.type() == type)
641 {
642 // a struct/union/vector can be initialized directly with
643 // an expression of the right type. This doesn't
644 // work with arrays, unfortunately.
645 if(
646 type.id() == ID_struct_tag || type.id() == ID_union_tag ||
647 type.id() == ID_vector)
648 {
649 *dest=value;
650 return ++init_it; // done
651 }
652 }
653
655 type.id() == ID_struct_tag || type.id() == ID_union_tag ||
656 type.id() == ID_array || type.id() == ID_vector,
657 "full type must be composite");
658
659 // we are initializing a compound type, and enter it!
660 // this may change the type, type might not be valid any more
661 const typet dest_type = type;
662 const bool vla_permitted=designator.back().vla_permitted;
663 designator_enter(type, designator);
664
665 // GCC permits (though issuing a warning with -Wall) composite
666 // types built from flat initializer lists
667 if(dest->operands().empty())
668 {
670 warning() << "initialisation of " << dest_type.id()
671 << " requires initializer list, found " << value.id()
672 << " instead" << eom;
673
674 // in case of a variable-length array consume all remaining
675 // initializer elements
676 if(vla_permitted &&
677 dest_type.id()==ID_array &&
678 (to_array_type(dest_type).size().is_zero() ||
679 to_array_type(dest_type).size().is_nil()))
680 {
681 value.id(ID_initializer_list);
682 value.operands().clear();
683 for( ; init_it!=initializer_list.operands().end(); ++init_it)
686
687 return init_it;
688 }
689 else
690 {
692 error() << "cannot initialize type '" << to_string(dest_type)
693 << "' using value '" << to_string(value) << "'" << eom;
694 throw 0;
695 }
696 }
697
698 dest = &(to_multi_ary_expr(*dest).op0());
699
700 // we run into another loop iteration
701 }
702
703 return ++init_it;
704}
705
707{
708 PRECONDITION(!designator.empty());
709
710 while(true)
711 {
712 designatort::entryt &entry=designator[designator.size()-1];
713
714 entry.index++;
715
716 if(entry.type.id() == ID_array && to_array_type(entry.type).size().is_nil())
717 return; // we will keep going forever
718
719 if(entry.type.id() == ID_struct_tag && entry.index < entry.size)
720 {
721 // need to adjust subtype
724 const struct_typet::componentst &components=
725 struct_type.components();
727 components.size() == entry.size, "matching component numbers");
728
729 // we skip over any padding
730 // we also skip over anonymous members that are bit fields
731 while(entry.index < entry.size &&
732 (components[entry.index].get_is_padding() ||
733 (components[entry.index].get_anonymous() &&
734 components[entry.index].type().id() == ID_c_bit_field)))
735 {
736 entry.index++;
737 }
738
739 if(entry.index<entry.size)
740 entry.subtype=components[entry.index].type();
741 }
742
743 if(entry.index<entry.size)
744 return; // done
745
746 if(designator.size()==1)
747 return; // done
748
749 // pop entry
750 designator.pop_entry();
751
752 INVARIANT(!designator.empty(), "designator had more than one entry");
753 }
754}
755
757 const typet &src_type,
758 const exprt &src)
759{
760 PRECONDITION(!src.operands().empty());
761
762 typet type=src_type;
763 designatort designator;
764
765 for(const auto &d_op : src.operands())
766 {
767 designatort::entryt entry(type);
768
769 if(entry.type.id() == ID_array)
770 {
771 if(d_op.id()!=ID_index)
772 {
773 error().source_location = d_op.source_location();
774 error() << "expected array index designator" << eom;
775 throw 0;
776 }
777
780
781 mp_integer index, size;
782
784 {
785 error().source_location = to_unary_expr(d_op).op().source_location();
786 error() << "expected constant array index designator" << eom;
787 throw 0;
788 }
789
790 if(to_array_type(entry.type).size().is_nil())
791 size=0;
792 else if(
793 const auto size_opt =
795 size = *size_opt;
796 else
797 {
798 error().source_location = to_unary_expr(d_op).op().source_location();
799 error() << "expected constant array size" << eom;
800 throw 0;
801 }
802
803 entry.index = numeric_cast_v<std::size_t>(index);
804 entry.size = numeric_cast_v<std::size_t>(size);
805 entry.subtype = to_array_type(entry.type).element_type();
806 }
807 else if(
810 {
813
814 if(d_op.id()!=ID_member)
815 {
816 error().source_location = d_op.source_location();
817 error() << "expected member designator" << eom;
818 throw 0;
819 }
820
821 const irep_idt &component_name=d_op.get(ID_component_name);
822
823 if(struct_union_type.has_component(component_name))
824 {
825 // a direct member
826 entry.index=struct_union_type.component_number(component_name);
827 entry.size=struct_union_type.components().size();
828 entry.subtype=struct_union_type.components()[entry.index].type();
829 }
830 else
831 {
832 // We will search for anonymous members, in a loop. This isn't supported
833 // by GCC (unless the anonymous member is within an unnamed union or
834 // struct), but Visual Studio does allow it.
835
836 bool found=false, repeat;
837 typet tmp_type=entry.type;
838
839 do
840 {
841 repeat=false;
842 std::size_t number = 0;
843 const struct_union_typet::componentst &components =
845
846 for(const auto &c : components)
847 {
848 if(c.get_name() == component_name)
849 {
850 // done!
851 entry.index=number;
852 entry.size=components.size();
853 entry.subtype = c.type();
854 entry.type=tmp_type;
855 }
856 else if(
857 c.get_anonymous() &&
858 (c.type().id() == ID_struct_tag ||
859 c.type().id() == ID_union_tag) &&
860 (config.ansi_c.mode ==
863 .find(ID_tag)
864 .is_nil()) &&
865 has_component_rec(c.type(), component_name, *this))
866 {
867 entry.index=number;
868 entry.size=components.size();
869 entry.subtype = c.type();
870 entry.type=tmp_type;
871 tmp_type=entry.subtype;
872 designator.push_entry(entry);
873 found=repeat=true;
874 break;
875 }
876
877 ++number;
878 }
879 }
880 while(repeat);
881
882 if(!found)
883 {
884 error().source_location = d_op.source_location();
885 error() << "failed to find struct component '" << component_name
886 << "' in initialization of '" << to_string(struct_union_type)
887 << "'" << eom;
888 throw 0;
889 }
890 }
891 }
892 else
893 {
894 error().source_location = d_op.source_location();
895 error() << "designated initializers cannot initialize '"
896 << to_string(entry.type) << "'" << eom;
897 throw 0;
898 }
899
900 type=entry.subtype;
901 designator.push_entry(entry);
902 }
903
904 INVARIANT(!designator.empty(), "expected an entry to be added");
905
906 return designator;
907}
908
910 const exprt &value,
911 const typet &type,
912 bool force_constant)
913{
915
916 // 6.7.9, 14: An array of character type may be initialized by a character
917 // string literal or UTF-8 string literal, optionally enclosed in braces.
918 if(
919 type.id() == ID_array && value.operands().size() >= 1 &&
920 to_multi_ary_expr(value).op0().id() == ID_string_constant &&
921 (to_array_type(type).element_type().id() == ID_signedbv ||
922 to_array_type(type).element_type().id() == ID_unsignedbv) &&
923 to_bitvector_type(to_array_type(type).element_type()).get_width() ==
924 char_type().get_width())
925 {
926 if(value.operands().size() > 1)
927 {
929 warning() << "ignoring excess initializers" << eom;
930 }
931
932 return do_initializer_rec(
933 to_multi_ary_expr(value).op0(), type, force_constant);
934 }
935
937 if(
938 type.id() == ID_struct_tag || type.id() == ID_union_tag ||
939 type.id() == ID_vector)
940 {
941 // start with zero everywhere
942 const auto zero = zero_initializer(type, value.source_location(), *this);
943 if(!zero.has_value())
944 {
946 error() << "cannot zero-initialize '" << to_string(type) << "'" << eom;
947 throw 0;
948 }
949 result = *zero;
950 }
951 else if(type.id() == ID_array)
952 {
953 if(to_array_type(type).size().is_nil())
954 {
955 // start with empty array
956 result = array_exprt({}, to_array_type(type));
957 result.add_source_location()=value.source_location();
958 }
959 else
960 {
961 // start with zero everywhere
962 const auto zero = zero_initializer(type, value.source_location(), *this);
963 if(!zero.has_value())
964 {
966 error() << "cannot zero-initialize '" << to_string(type) << "'" << eom;
967 throw 0;
968 }
969 result = *zero;
970 }
971 }
972 else if(type.id() == ID_complex)
973 {
974 // These may be initialized with an expression, an initializer list
975 // of size two, or an initializer list of size one.
976 if(value.operands().size() == 1)
977 {
978 return do_initializer_rec(
979 to_unary_expr(value).op(), type, force_constant);
980 }
981 else if(value.operands().size() == 2)
982 {
983 auto &complex_type = to_complex_type(type);
984 auto &subtype = complex_type.subtype();
985 auto real = do_initializer_rec(
986 to_binary_expr(value).op0(), subtype, force_constant);
987 auto imag = do_initializer_rec(
988 to_binary_expr(value).op1(), subtype, force_constant);
989 return complex_exprt(real, imag, complex_type)
991 }
992 else
993 {
994 throw errort().with_location(value.source_location())
995 << "too many initializers for '" << to_string(type) << "'";
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(type)
1009 << "' with an initializer list" << eom;
1010 throw 0;
1011 }
1012
1014
1016
1017 const exprt::operandst &operands=value.operands();
1018 for(exprt::operandst::const_iterator it=operands.begin();
1019 it!=operands.end(); ) // no ++it
1020 {
1023
1024 // increase designator -- might go up
1026 }
1027
1029 {
1031 const struct_typet::componentst &components = full_struct_type.components();
1032 // make sure we didn't mess up index computation
1033 CHECK_RETURN(result.operands().size() == components.size());
1034
1035 if(
1036 !components.empty() &&
1037 components.back().type().get_bool(ID_C_flexible_array_member))
1038 {
1040 to_array_type(components.back().type()).size());
1041 array_exprt &init_array = to_array_expr(result.operands().back());
1042 if(
1043 !array_size.has_value() ||
1044 (*array_size <= 1 && init_array.operands().size() != *array_size))
1045 {
1048 to_array_type(actual_struct_type.components().back().type());
1050 init_array.operands().size(), actual_array_type.index_type());
1053
1054 // mimic bits of typecheck_compound_type to produce a new struct tag
1055 actual_struct_type.remove(ID_tag);
1056 std::string typestr = type2name(actual_struct_type, *this);
1057 irep_idt tag_identifier = "tag-#anon#" + typestr;
1059 compound_symbol.base_name = "#anon#" + typestr;
1060 compound_symbol.location = value.source_location();
1061
1062 // We might already have the same anonymous struct, which is fine as it
1063 // will be exactly the same type.
1065
1067 }
1068 }
1069 }
1070
1071 if(type.id() == ID_array && to_array_type(type).size().is_nil())
1072 {
1073 // make complete by setting array size
1075 array_type.size() =
1076 from_integer(result.operands().size(), array_type.index_type());
1077 }
1078
1079 return result;
1080}
bool has_component_rec(const typet &type, const irep_idt &component_name, const namespacet &ns)
C Language Type Checking.
configt config
Definition config.cpp:25
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
bool to_integer(const constant_exprt &expr, mp_integer &int_value)
Convert a constant expression expr to an arbitrary-precision integer.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
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.
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:106
bitvector_typet c_index_type()
Definition c_types.cpp:16
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition c_types.h:224
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Array constructor from list of elements.
Definition std_expr.h:1621
Arrays with given size.
Definition std_types.h:807
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)
symbol_table_baset & symbol_table
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)
const irep_idt const irep_idt mode
virtual void make_constant_index(exprt &expr)
designatort make_designator(const typet &type, const exprt &src)
void designator_enter(const typet &type, designatort &designator)
Complex constructor from a pair of numbers.
Definition std_expr.h:1916
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:38
bool starts_with(const char *s) const
equivalent of as_string().starts_with(s)
Definition dstring.h:95
Base class for all expressions.
Definition expr.h:56
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
Definition expr.cpp:147
std::vector< exprt > operandst
Definition expr.h:58
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
Definition expr.h:163
typet & type()
Return the type of the expression.
Definition expr.h:84
operandst & operands()
Definition expr.h:94
const source_locationt & source_location() const
Definition expr.h:231
exprt & with_source_location(source_locationt location) &
Add the source location from location, if it is non-nil.
Definition expr.h:101
bool get_bool(const irep_idt &name) const
Definition irep.cpp:57
const irept & find(const irep_idt &name) const
Definition irep.cpp:93
bool is_not_nil() const
Definition irep.h:372
void make_nil()
Definition irep.h:446
const irep_idt & id() const
Definition irep.h:388
source_locationt source_location
Definition message.h:239
mstreamt & error() const
Definition message.h:391
mstreamt & warning() const
Definition message.h:396
mstreamt & result() const
Definition message.h:401
static eomt eom
Definition message.h:289
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition namespace.cpp:49
A struct tag type, i.e., struct_typet with an identifier.
Definition std_types.h:493
Structure type, corresponds to C style structs.
Definition std_types.h:231
Base type for structs and unions.
Definition std_types.h:62
std::vector< componentt > componentst
Definition std_types.h:140
virtual std::pair< symbolt &, bool > insert(symbolt symbol)=0
Move or copy a new symbol to the symbol table.
Symbol table entry.
Definition symbol.h:28
bool is_macro
Definition symbol.h:62
bool is_static_lifetime
Definition symbol.h:70
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
Symbol table entry describing a data typeThis is a symbol generated as part of type checking.
Definition symbol.h:139
errort with_location(source_locationt _location) &&
Definition typecheck.h:47
The type of an expression, extends irept.
Definition type.h:29
Union constructor from single element.
Definition std_expr.h:1770
The union type.
Definition c_types.h:147
The vector type.
Definition std_types.h:1064
#define CPROVER_PREFIX
#define Forall_operands(it, expr)
Definition expr.h:27
std::optional< exprt > zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns)
Create the equivalent of zero for type type.
Expression Initialization.
BigInt mp_integer
Definition smt_terms.h:17
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:525
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:534
#define PRECONDITION(CONDITION)
Definition invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition std_expr.cpp:97
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast an exprt to an array_of_exprt.
Definition std_expr.h:1603
const array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_exprt.
Definition std_expr.h:1665
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition std_expr.h:715
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition std_expr.h:426
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
Definition std_expr.h:987
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
Definition std_expr.h:1816
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition std_expr.h:3172
Pre-defined types.
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition std_types.h:1116
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition std_types.h:518
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
Definition std_types.h:1158
const struct_or_union_tag_typet & to_struct_or_union_tag_type(const typet &type)
Cast a typet to a struct_or_union_tag_typet.
Definition std_types.h:478
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:888
const string_constantt & to_string_constant(const exprt &expr)
Author: Diffblue Ltd.
static std::string type2name(const typet &type, const namespacet &ns, symbol_numbert &symbol_number)
Definition type2name.cpp:82
Type Naming for C.
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition type.h:208