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 <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/prefix.h>
19#include <util/std_types.h>
22
23#include "anonymous_member.h"
24#include "c_typecheck_base.h"
25#include "type2name.h"
26
28 exprt &initializer,
29 const typet &type,
30 bool force_constant)
31{
33
34 if(type.id()==ID_array)
35 {
36 const typet &result_type = result.type();
37 DATA_INVARIANT(result_type.id()==ID_array &&
38 to_array_type(result_type).size().is_not_nil(),
39 "any array must have a size");
40
41 // we don't allow initialisation with symbols of array type
42 if(
43 result.id() != ID_array && result.id() != ID_array_of &&
45 {
47 error() << "invalid array initializer " << to_string(result)
48 << eom;
49 throw 0;
50 }
51 }
52
53 initializer=result;
54}
55
58 const exprt &value,
59 const typet &type,
60 bool force_constant)
61{
62 const typet &full_type=follow(type);
63
64 if(
65 (full_type.id() == ID_struct || full_type.id() == ID_union) &&
66 to_struct_union_type(full_type).is_incomplete())
67 {
69 error() << "type '" << to_string(type)
70 << "' is still incomplete -- cannot initialize" << eom;
71 throw 0;
72 }
73
74 if(value.id()==ID_initializer_list)
75 return do_initializer_list(value, type, force_constant);
76
77 if(
78 value.id() == ID_array && value.get_bool(ID_C_string_constant) &&
79 full_type.id() == ID_array &&
80 (to_array_type(full_type).element_type().id() == ID_signedbv ||
81 to_array_type(full_type).element_type().id() == ID_unsignedbv) &&
82 to_bitvector_type(to_array_type(full_type).element_type()).get_width() ==
83 to_bitvector_type(to_array_type(value.type()).element_type()).get_width())
84 {
85 exprt tmp=value;
86
87 // adjust char type
88 to_array_type(tmp.type()).element_type() =
89 to_array_type(full_type).element_type();
90
92 it->type() = to_array_type(full_type).element_type();
93
94 if(full_type.id()==ID_array &&
95 to_array_type(full_type).is_complete())
96 {
97 const auto &array_type = to_array_type(full_type);
98
99 // check size
101 if(!array_size.has_value())
102 {
104 error() << "array size needs to be constant, got "
105 << to_string(array_type.size()) << eom;
106 throw 0;
107 }
108
109 if(*array_size < 0)
110 {
112 error() << "array size must not be negative" << eom;
113 throw 0;
114 }
115
116 if(mp_integer(tmp.operands().size()) > *array_size)
117 {
118 // cut off long strings. gcc does a warning for this
119 tmp.operands().resize(numeric_cast_v<std::size_t>(*array_size));
120 tmp.type()=type;
121 }
122 else if(mp_integer(tmp.operands().size()) < *array_size)
123 {
124 // fill up
125 tmp.type()=type;
126 const auto zero = zero_initializer(
127 array_type.element_type(), value.source_location(), *this);
128 if(!zero.has_value())
129 {
131 error() << "cannot zero-initialize array with subtype '"
132 << to_string(array_type.element_type()) << "'" << eom;
133 throw 0;
134 }
135 tmp.operands().resize(numeric_cast_v<std::size_t>(*array_size), *zero);
136 }
137 }
138
139 return tmp;
140 }
141
142 if(
143 value.id() == ID_string_constant && full_type.id() == ID_array &&
144 (to_array_type(full_type).element_type().id() == ID_signedbv ||
145 to_array_type(full_type).element_type().id() == ID_unsignedbv) &&
146 to_bitvector_type(to_array_type(full_type).element_type()).get_width() ==
147 char_type().get_width())
148 {
149 // will go away, to be replaced by the above block
150
152 // adjust char type
153 to_array_type(tmp1.type()).element_type() =
154 to_array_type(full_type).element_type();
155
156 exprt tmp2=tmp1.to_array_expr();
157
158 if(full_type.id()==ID_array &&
159 to_array_type(full_type).is_complete())
160 {
161 // check size
162 const auto array_size =
163 numeric_cast<mp_integer>(to_array_type(full_type).size());
164 if(!array_size.has_value())
165 {
167 error() << "array size needs to be constant, got "
168 << to_string(to_array_type(full_type).size()) << eom;
169 throw 0;
170 }
171
172 if(*array_size < 0)
173 {
175 error() << "array size must not be negative" << eom;
176 throw 0;
177 }
178
179 if(mp_integer(tmp2.operands().size()) > *array_size)
180 {
181 // cut off long strings. gcc does a warning for this
182 tmp2.operands().resize(numeric_cast_v<std::size_t>(*array_size));
183 tmp2.type()=type;
184 }
185 else if(mp_integer(tmp2.operands().size()) < *array_size)
186 {
187 // fill up
188 tmp2.type()=type;
189 const auto zero = zero_initializer(
190 to_array_type(full_type).element_type(),
191 value.source_location(),
192 *this);
193 if(!zero.has_value())
194 {
196 error() << "cannot zero-initialize array with subtype '"
197 << to_string(to_array_type(full_type).element_type()) << "'"
198 << eom;
199 throw 0;
200 }
201 tmp2.operands().resize(numeric_cast_v<std::size_t>(*array_size), *zero);
202 }
203 }
204
205 return tmp2;
206 }
207
208 if(full_type.id()==ID_array &&
209 to_array_type(full_type).size().is_nil())
210 {
212 error() << "type '" << to_string(full_type)
213 << "' cannot be initialized with '" << to_string(value) << "'"
214 << eom;
215 throw 0;
216 }
217
218 if(value.id()==ID_designated_initializer)
219 {
221 error() << "type '" << to_string(full_type)
222 << "' cannot be initialized with designated initializer" << eom;
223 throw 0;
224 }
225
226 exprt result=value;
228 return result;
229}
230
232{
233 // this one doesn't need initialization
234 if(has_prefix(id2string(symbol.name), CPROVER_PREFIX "constant_infinity"))
235 return;
236
237 if(symbol.is_type)
238 return;
239
240 if(symbol.value.is_not_nil())
241 {
242 typecheck_expr(symbol.value);
243 do_initializer(symbol.value, symbol.type, true);
244
245 // A flexible array may have been initialized, which entails a type change.
246 // Note that the type equality test is important: we want to preserve
247 // annotations like typedefs or const-ness when the type is otherwise the
248 // same.
249 if(!symbol.is_macro && symbol.type != symbol.value.type())
250 symbol.type = symbol.value.type();
251 }
252
253 if(symbol.is_macro)
254 make_constant(symbol.value);
255}
256
258 const typet &type,
259 designatort &designator)
260{
261 designatort::entryt entry(type);
262
263 const typet &full_type=follow(type);
264
265 if(full_type.id()==ID_struct)
266 {
267 const struct_typet &struct_type=to_struct_type(full_type);
268
269 entry.size=struct_type.components().size();
270 entry.subtype.make_nil();
271 // only a top-level struct may end with a variable-length array
272 entry.vla_permitted=designator.empty();
273
274 for(const auto &c : struct_type.components())
275 {
277 c.type().id() != ID_code, "struct member must not be of code type");
278
279 if(
280 !c.get_is_padding() &&
281 (c.type().id() != ID_c_bit_field || !c.get_anonymous()))
282 {
283 entry.subtype = c.type();
284 break;
285 }
286
287 ++entry.index;
288 }
289 }
290 else if(full_type.id()==ID_union)
291 {
292 const union_typet &union_type=to_union_type(full_type);
293
294 if(union_type.components().empty())
295 {
296 entry.size=0;
297 entry.subtype.make_nil();
298 }
299 else
300 {
301 // The default is to initialize using the first member of the
302 // union.
303 entry.size=1;
304 entry.subtype=union_type.components().front().type();
305 }
306 }
307 else if(full_type.id()==ID_array)
308 {
309 const array_typet &array_type=to_array_type(full_type);
310
311 if(array_type.size().is_nil())
312 {
313 entry.size=0;
314 entry.subtype = array_type.element_type();
315 }
316 else
317 {
319 if(!array_size.has_value())
320 {
321 error().source_location = array_type.size().source_location();
322 error() << "array has non-constant size '"
323 << to_string(array_type.size()) << "'" << eom;
324 throw 0;
325 }
326
328 entry.subtype = array_type.element_type();
329 }
330 }
331 else if(full_type.id()==ID_vector)
332 {
333 const vector_typet &vector_type=to_vector_type(full_type);
334
335 const auto vector_size = numeric_cast<mp_integer>(vector_type.size());
336
337 if(!vector_size.has_value())
338 {
339 error().source_location = vector_type.size().source_location();
340 error() << "vector has non-constant size '"
341 << to_string(vector_type.size()) << "'" << eom;
342 throw 0;
343 }
344
345 entry.size = numeric_cast_v<std::size_t>(*vector_size);
346 entry.subtype = vector_type.element_type();
347 }
348 else
350
351 designator.push_entry(entry);
352}
353
354exprt::operandst::const_iterator c_typecheck_baset::do_designated_initializer(
355 exprt &result,
356 designatort &designator,
357 const exprt &initializer_list,
358 exprt::operandst::const_iterator init_it,
359 bool force_constant)
360{
361 // copy the value, we may need to adjust it
362 exprt value=*init_it;
363
364 PRECONDITION(!designator.empty());
365
366 if(value.id()==ID_designated_initializer)
367 {
368 PRECONDITION(value.operands().size() == 1);
369
370 designator=
372 designator.front().type,
373 static_cast<const exprt &>(value.find(ID_designator)));
374
375 CHECK_RETURN(!designator.empty());
376
377 // discard the return value
379 result, designator, value, value.operands().begin(), force_constant);
380 return ++init_it;
381 }
382
383 exprt *dest=&result;
384
385 // first phase: follow given designator
386
387 for(size_t i=0; i<designator.size(); i++)
388 {
389 size_t index=designator[i].index;
390 const typet &type=designator[i].type;
391 const typet &full_type=follow(type);
392
393 if(full_type.id()==ID_array ||
394 full_type.id()==ID_vector)
395 {
396 // zero_initializer may have built an array_of expression for a large
397 // array; as we have a designated initializer we need to have an array of
398 // individual objects
399 if(dest->id() == ID_array_of)
400 {
401 const array_typet array_type = to_array_type(dest->type());
403 if(!array_size.has_value())
404 {
406 error() << "cannot zero-initialize array with element type '"
407 << to_string(to_type_with_subtype(full_type).subtype()) << "'"
408 << eom;
409 throw 0;
410 }
411 const exprt zero = to_array_of_expr(*dest).what();
412 *dest = array_exprt{{}, array_type};
413 dest->operands().resize(numeric_cast_v<std::size_t>(*array_size), zero);
414 }
415
416 if(index>=dest->operands().size())
417 {
418 if(full_type.id()==ID_array &&
419 (to_array_type(full_type).size().is_zero() ||
420 to_array_type(full_type).size().is_nil()))
421 {
422 const typet &element_type = to_array_type(full_type).element_type();
423
424 // we are willing to grow an incomplete or zero-sized array --
425 // do_initializer_list will fix up the resulting type
426 const auto zero =
427 zero_initializer(element_type, value.source_location(), *this);
428 if(!zero.has_value())
429 {
431 error() << "cannot zero-initialize array with element type '"
432 << to_string(element_type) << "'" << eom;
433 throw 0;
434 }
435 dest->operands().resize(
436 numeric_cast_v<std::size_t>(index) + 1, *zero);
437 }
438 else
439 {
441 error() << "array index designator " << index
442 << " out of bounds (" << dest->operands().size()
443 << ")" << eom;
444 throw 0;
445 }
446 }
447
448 dest = &(dest->operands()[numeric_cast_v<std::size_t>(index)]);
449 }
450 else if(full_type.id()==ID_struct)
451 {
452 const struct_typet::componentst &components=
453 to_struct_type(full_type).components();
454
455 if(index>=dest->operands().size())
456 {
458 error() << "structure member designator " << index
459 << " out of bounds (" << dest->operands().size()
460 << ")" << eom;
461 throw 0;
462 }
463
464 DATA_INVARIANT(index<components.size(),
465 "member designator is bounded by components size");
467 components[index].type().id() != ID_code,
468 "struct member must not be of code type");
470 !components[index].get_is_padding(),
471 "member designator points at non-padding member");
472
473 dest=&(dest->operands()[index]);
474 }
475 else if(full_type.id()==ID_union)
476 {
477 const union_typet &union_type=to_union_type(full_type);
478
479 const union_typet::componentst &components=
480 union_type.components();
481
482 if(components.empty())
483 {
485 error() << "union member designator found for empty union" << eom;
486 throw 0;
487 }
488 else if(init_it != initializer_list.operands().begin())
489 {
491 {
493 error() << "too many initializers" << eom;
494 throw 0;
495 }
496 else
497 {
499 warning() << "excess elements in union initializer" << eom;
500
501 return ++init_it;
502 }
503 }
504 else if(index >= components.size())
505 {
507 error() << "union member designator " << index << " out of bounds ("
508 << components.size() << ")" << eom;
509 throw 0;
510 }
511
512 const union_typet::componentt &component = components[index];
513
514 if(
515 dest->id() == ID_union &&
516 to_union_expr(*dest).get_component_name() == component.get_name())
517 {
518 // Already right union component. We can initialize multiple submembers,
519 // so do not overwrite this.
520 dest = &(to_union_expr(*dest).op());
521 }
522 else if(dest->id() == ID_union)
523 {
524 // The designated initializer does not initialize the maximum member,
525 // which the (default) zero initializer prepared. Replace this by a
526 // component-specific initializer; other bytes have an unspecified value
527 // (C Standard 6.2.6.1(7)). In practice, objects of static lifetime are
528 // fully zero initialized, so we just byte-update on top of the existing
529 // zero initializer.
530 const auto zero =
531 zero_initializer(component.type(), value.source_location(), *this);
532 if(!zero.has_value())
533 {
535 error() << "cannot zero-initialize union component of type '"
536 << to_string(component.type()) << "'" << eom;
537 throw 0;
538 }
539
541 {
543 make_byte_update(*dest, from_integer(0, c_index_type()), *zero);
544 byte_update.add_source_location() = value.source_location();
545 *dest = std::move(byte_update);
546 dest = &(to_byte_update_expr(*dest).op2());
547 }
548 else
549 {
550 union_exprt union_expr(component.get_name(), *zero, type);
551 union_expr.add_source_location() = value.source_location();
552 *dest = std::move(union_expr);
553 dest = &(to_union_expr(*dest).op());
554 }
555 }
556 else if(
557 dest->id() == ID_byte_update_big_endian ||
559 {
560 // handle the byte update introduced by an earlier initializer (if
561 // current_symbol.is_static_lifetime)
563 dest = &byte_update.op2();
564 }
565 }
566 else
568 }
569
570 // second phase: assign value
571 // for this, we may need to go down, adding to the designator
572
573 while(true)
574 {
575 // see what type we have to initialize
576
577 const typet &type=designator.back().subtype;
578 const typet &full_type=follow(type);
579
580 // do we initialize a scalar?
581 if(full_type.id()!=ID_struct &&
582 full_type.id()!=ID_union &&
583 full_type.id()!=ID_array &&
584 full_type.id()!=ID_vector)
585 {
586 // The initializer for a scalar shall be a single expression,
587 // * optionally enclosed in braces. *
588
589 if(value.id()==ID_initializer_list &&
590 value.operands().size()==1)
591 {
592 *dest =
594 }
595 else
596 *dest=do_initializer_rec(value, type, force_constant);
597
598 DATA_INVARIANT(full_type == follow(dest->type()), "matching types");
599
600 return ++init_it; // done
601 }
602
603 // union? The component in the zero initializer might
604 // not be the first one.
605 if(full_type.id()==ID_union)
606 {
607 const union_typet &union_type=to_union_type(full_type);
608
609 const union_typet::componentst &components=
610 union_type.components();
611
612 if(!components.empty())
613 {
615 union_type.components().front();
616
617 const auto zero =
618 zero_initializer(component.type(), value.source_location(), *this);
619 if(!zero.has_value())
620 {
622 error() << "cannot zero-initialize union component of type '"
623 << to_string(component.type()) << "'" << eom;
624 throw 0;
625 }
626 union_exprt union_expr(component.get_name(), *zero, type);
627 union_expr.add_source_location()=value.source_location();
628 *dest=union_expr;
629 }
630 }
631
632 // see what initializer we are given
633 if(value.id()==ID_initializer_list)
634 {
635 *dest=do_initializer_rec(value, type, force_constant);
636 return ++init_it; // done
637 }
638 else if(value.id()==ID_string_constant)
639 {
640 // We stop for initializers that are string-constants,
641 // which are like arrays. We only do so if we are to
642 // initialize an array of scalars.
643 if(
644 full_type.id() == ID_array &&
645 (to_array_type(full_type).element_type().id() == ID_signedbv ||
646 to_array_type(full_type).element_type().id() == ID_unsignedbv))
647 {
648 *dest=do_initializer_rec(value, type, force_constant);
649 return ++init_it; // done
650 }
651 }
652 else if(follow(value.type())==full_type)
653 {
654 // a struct/union/vector can be initialized directly with
655 // an expression of the right type. This doesn't
656 // work with arrays, unfortunately.
657 if(full_type.id()==ID_struct ||
658 full_type.id()==ID_union ||
659 full_type.id()==ID_vector)
660 {
661 *dest=value;
662 return ++init_it; // done
663 }
664 }
665
667 full_type.id() == ID_struct || full_type.id() == ID_union ||
668 full_type.id() == ID_array || full_type.id() == ID_vector,
669 "full type must be composite");
670
671 // we are initializing a compound type, and enter it!
672 // this may change the type, full_type might not be valid any more
673 const typet dest_type=full_type;
674 const bool vla_permitted=designator.back().vla_permitted;
675 designator_enter(type, designator);
676
677 // GCC permits (though issuing a warning with -Wall) composite
678 // types built from flat initializer lists
679 if(dest->operands().empty())
680 {
682 warning() << "initialisation of " << dest_type.id()
683 << " requires initializer list, found " << value.id()
684 << " instead" << eom;
685
686 // in case of a variable-length array consume all remaining
687 // initializer elements
688 if(vla_permitted &&
689 dest_type.id()==ID_array &&
690 (to_array_type(dest_type).size().is_zero() ||
691 to_array_type(dest_type).size().is_nil()))
692 {
693 value.id(ID_initializer_list);
694 value.operands().clear();
695 for( ; init_it!=initializer_list.operands().end(); ++init_it)
698
699 return init_it;
700 }
701 else
702 {
704 error() << "cannot initialize type '" << to_string(dest_type)
705 << "' using value '" << to_string(value) << "'" << eom;
706 throw 0;
707 }
708 }
709
710 dest = &(to_multi_ary_expr(*dest).op0());
711
712 // we run into another loop iteration
713 }
714
715 return ++init_it;
716}
717
719{
720 PRECONDITION(!designator.empty());
721
722 while(true)
723 {
724 designatort::entryt &entry=designator[designator.size()-1];
725 const typet &full_type=follow(entry.type);
726
727 entry.index++;
728
729 if(full_type.id()==ID_array &&
730 to_array_type(full_type).size().is_nil())
731 return; // we will keep going forever
732
733 if(full_type.id()==ID_struct &&
734 entry.index<entry.size)
735 {
736 // need to adjust subtype
738 to_struct_type(full_type);
739 const struct_typet::componentst &components=
740 struct_type.components();
742 components.size() == entry.size, "matching component numbers");
743
744 // we skip over any padding
745 // we also skip over anonymous members that are bit fields
746 while(entry.index < entry.size &&
747 (components[entry.index].get_is_padding() ||
748 (components[entry.index].get_anonymous() &&
749 components[entry.index].type().id() == ID_c_bit_field)))
750 {
751 entry.index++;
752 }
753
754 if(entry.index<entry.size)
755 entry.subtype=components[entry.index].type();
756 }
757
758 if(entry.index<entry.size)
759 return; // done
760
761 if(designator.size()==1)
762 return; // done
763
764 // pop entry
765 designator.pop_entry();
766
767 INVARIANT(!designator.empty(), "designator had more than one entry");
768 }
769}
770
772 const typet &src_type,
773 const exprt &src)
774{
775 PRECONDITION(!src.operands().empty());
776
777 typet type=src_type;
778 designatort designator;
779
780 for(const auto &d_op : src.operands())
781 {
782 designatort::entryt entry(type);
783 const typet &full_type=follow(entry.type);
784
785 if(full_type.id()==ID_array)
786 {
787 if(d_op.id()!=ID_index)
788 {
789 error().source_location = d_op.source_location();
790 error() << "expected array index designator" << eom;
791 throw 0;
792 }
793
796
797 mp_integer index, size;
798
800 {
801 error().source_location = to_unary_expr(d_op).op().source_location();
802 error() << "expected constant array index designator" << eom;
803 throw 0;
804 }
805
806 if(to_array_type(full_type).size().is_nil())
807 size=0;
808 else if(
809 const auto size_opt =
810 numeric_cast<mp_integer>(to_array_type(full_type).size()))
811 size = *size_opt;
812 else
813 {
814 error().source_location = to_unary_expr(d_op).op().source_location();
815 error() << "expected constant array size" << eom;
816 throw 0;
817 }
818
819 entry.index = numeric_cast_v<std::size_t>(index);
820 entry.size = numeric_cast_v<std::size_t>(size);
821 entry.subtype = to_array_type(full_type).element_type();
822 }
823 else if(full_type.id()==ID_struct ||
824 full_type.id()==ID_union)
825 {
827 to_struct_union_type(full_type);
828
829 if(d_op.id()!=ID_member)
830 {
831 error().source_location = d_op.source_location();
832 error() << "expected member designator" << eom;
833 throw 0;
834 }
835
836 const irep_idt &component_name=d_op.get(ID_component_name);
837
838 if(struct_union_type.has_component(component_name))
839 {
840 // a direct member
841 entry.index=struct_union_type.component_number(component_name);
842 entry.size=struct_union_type.components().size();
843 entry.subtype=struct_union_type.components()[entry.index].type();
844 }
845 else
846 {
847 // We will search for anonymous members, in a loop. This isn't supported
848 // by GCC (unless the anonymous member is within an unnamed union or
849 // struct), but Visual Studio does allow it.
850
851 bool found=false, repeat;
852 typet tmp_type=entry.type;
853
854 do
855 {
856 repeat=false;
857 std::size_t number = 0;
858 const struct_union_typet::componentst &components=
859 to_struct_union_type(follow(tmp_type)).components();
860
861 for(const auto &c : components)
862 {
863 if(c.get_name() == component_name)
864 {
865 // done!
866 entry.index=number;
867 entry.size=components.size();
868 entry.subtype = c.type();
869 entry.type=tmp_type;
870 }
871 else if(
872 c.get_anonymous() &&
873 (c.type().id() == ID_struct_tag ||
874 c.type().id() == ID_union_tag) &&
875 (config.ansi_c.mode ==
877 follow(c.type()).find(ID_tag).is_nil()) &&
878 has_component_rec(c.type(), component_name, *this))
879 {
880 entry.index=number;
881 entry.size=components.size();
882 entry.subtype = c.type();
883 entry.type=tmp_type;
884 tmp_type=entry.subtype;
885 designator.push_entry(entry);
886 found=repeat=true;
887 break;
888 }
889
890 ++number;
891 }
892 }
893 while(repeat);
894
895 if(!found)
896 {
897 error().source_location = d_op.source_location();
898 error() << "failed to find struct component '" << component_name
899 << "' in initialization of '" << to_string(struct_union_type)
900 << "'" << eom;
901 throw 0;
902 }
903 }
904 }
905 else
906 {
907 error().source_location = d_op.source_location();
908 error() << "designated initializers cannot initialize '"
909 << to_string(full_type) << "'" << eom;
910 throw 0;
911 }
912
913 type=entry.subtype;
914 designator.push_entry(entry);
915 }
916
917 INVARIANT(!designator.empty(), "expected an entry to be added");
918
919 return designator;
920}
921
923 const exprt &value,
924 const typet &type,
925 bool force_constant)
926{
928
929 const typet &full_type=follow(type);
930
931 // 6.7.9, 14: An array of character type may be initialized by a character
932 // string literal or UTF-8 string literal, optionally enclosed in braces.
933 if(
934 full_type.id() == ID_array && value.operands().size() >= 1 &&
935 to_multi_ary_expr(value).op0().id() == ID_string_constant &&
936 (to_array_type(full_type).element_type().id() == ID_signedbv ||
937 to_array_type(full_type).element_type().id() == ID_unsignedbv) &&
938 to_bitvector_type(to_array_type(full_type).element_type()).get_width() ==
939 char_type().get_width())
940 {
941 if(value.operands().size() > 1)
942 {
944 warning() << "ignoring excess initializers" << eom;
945 }
946
947 return do_initializer_rec(
948 to_multi_ary_expr(value).op0(), type, force_constant);
949 }
950
952 if(full_type.id()==ID_struct ||
953 full_type.id()==ID_union ||
954 full_type.id()==ID_vector)
955 {
956 // start with zero everywhere
957 const auto zero = zero_initializer(type, value.source_location(), *this);
958 if(!zero.has_value())
959 {
961 error() << "cannot zero-initialize '" << to_string(full_type) << "'"
962 << eom;
963 throw 0;
964 }
965 result = *zero;
966 }
967 else if(full_type.id()==ID_array)
968 {
969 if(to_array_type(full_type).size().is_nil())
970 {
971 // start with empty array
972 result = array_exprt({}, to_array_type(full_type));
973 result.add_source_location()=value.source_location();
974 }
975 else
976 {
977 // start with zero everywhere
978 const auto zero = zero_initializer(type, value.source_location(), *this);
979 if(!zero.has_value())
980 {
982 error() << "cannot zero-initialize '" << to_string(full_type) << "'"
983 << eom;
984 throw 0;
985 }
986 result = *zero;
987 }
988 }
989 else
990 {
991 // The initializer for a scalar shall be a single expression,
992 // * optionally enclosed in braces. *
993
994 if(value.operands().size()==1)
995 return do_initializer_rec(
996 to_unary_expr(value).op(), type, force_constant);
997
999 error() << "cannot initialize '" << to_string(full_type)
1000 << "' with an initializer list" << eom;
1001 throw 0;
1002 }
1003
1005
1007
1008 const exprt::operandst &operands=value.operands();
1009 for(exprt::operandst::const_iterator it=operands.begin();
1010 it!=operands.end(); ) // no ++it
1011 {
1014
1015 // increase designator -- might go up
1017 }
1018
1019 if(full_type.id()==ID_struct)
1020 {
1021 const struct_typet &full_struct_type = to_struct_type(full_type);
1022 const struct_typet::componentst &components = full_struct_type.components();
1023 // make sure we didn't mess up index computation
1024 CHECK_RETURN(result.operands().size() == components.size());
1025
1026 if(
1027 !components.empty() &&
1028 components.back().type().get_bool(ID_C_flexible_array_member))
1029 {
1031 to_array_type(components.back().type()).size());
1032 array_exprt &init_array = to_array_expr(result.operands().back());
1033 if(
1034 !array_size.has_value() ||
1035 (*array_size <= 1 && init_array.operands().size() != *array_size))
1036 {
1039 to_array_type(actual_struct_type.components().back().type());
1041 init_array.operands().size(), actual_array_type.index_type());
1044
1045 // mimic bits of typecheck_compound_type to produce a new struct tag
1046 actual_struct_type.remove(ID_tag);
1047 std::string typestr = type2name(actual_struct_type, *this);
1048 irep_idt tag_identifier = "tag-#anon#" + typestr;
1050 compound_symbol.base_name = "#anon#" + typestr;
1051 compound_symbol.location = value.source_location();
1052
1053 // We might already have the same anonymous struct, which is fine as it
1054 // will be exactly the same type.
1056
1058 }
1059 }
1060 }
1061
1062 if(full_type.id()==ID_array &&
1063 to_array_type(full_type).size().is_nil())
1064 {
1065 // make complete by setting array size
1067 array_type.size() =
1068 from_integer(result.operands().size(), array_type.index_type());
1069 }
1070
1071 return result;
1072}
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:111
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:184
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
Array constructor from list of elements.
Definition std_expr.h:1563
Arrays with given size.
Definition std_types.h:763
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)
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:39
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:155
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:223
bool get_bool(const irep_idt &name) const
Definition irep.cpp:57
const irept & find(const irep_idt &name) const
Definition irep.cpp:101
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
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
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition namespace.cpp:49
A struct tag type, i.e., struct_typet with an identifier.
Definition std_types.h:449
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
The type of an expression, extends irept.
Definition type.h:29
Union constructor from single element.
Definition std_expr.h:1708
The union type.
Definition c_types.h:147
The vector type.
Definition std_types.h:1008
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:27
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:18
#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:77
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast an exprt to an array_of_exprt.
Definition std_expr.h:1543
const array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_exprt.
Definition std_expr.h:1603
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition std_expr.h:361
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
Definition std_expr.h:932
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
Definition std_expr.h:1754
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition std_expr.h:2992
Pre-defined types.
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition std_types.h:1060
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:844
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)
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:175