cprover
c_typecheck_initializer.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: ANSI-C Conversion / Type Checking
4 
5 Author: 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>
19 #include <util/expr_initializer.h>
20 #include <util/prefix.h>
21 #include <util/std_types.h>
22 #include <util/string_constant.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;
225  implicit_typecast(result, type);
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
361  UNREACHABLE;
362 
363  designator.push_entry(entry);
364 }
365 
366 exprt::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
578  UNREACHABLE;
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 
960  exprt result;
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 typet & element_type() const
The type of the elements of the array.
Definition: std_types.h:777
const exprt & size() const
Definition: std_types.h:790
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
source_locationt & add_source_location()
Definition: expr.h:235
const source_locationt & source_location() const
Definition: expr.h:230
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:92
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
const irep_idt & id() const
Definition: irep.h:396
void make_nil()
Definition: irep.h:454
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
bool has_component(const irep_idt &component_name) const
Definition: std_types.h:157
const componentst & components() const
Definition: std_types.h:147
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 constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2840
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
Definition: std_expr.h:1657
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 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
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.