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