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  (full_type.subtype().id() == ID_signedbv ||
80  full_type.subtype().id() == ID_unsignedbv) &&
81  to_bitvector_type(full_type.subtype()).get_width() ==
83  {
84  exprt tmp=value;
85 
86  // adjust char type
87  tmp.type().subtype()=full_type.subtype();
88 
89  Forall_operands(it, tmp)
90  it->type()=full_type.subtype();
91 
92  if(full_type.id()==ID_array &&
93  to_array_type(full_type).is_complete())
94  {
95  // check size
96  const auto array_size =
97  numeric_cast<mp_integer>(to_array_type(full_type).size());
98  if(!array_size.has_value())
99  {
101  error() << "array size needs to be constant, got "
102  << to_string(to_array_type(full_type).size()) << eom;
103  throw 0;
104  }
105 
106  if(*array_size < 0)
107  {
109  error() << "array size must not be negative" << eom;
110  throw 0;
111  }
112 
113  if(mp_integer(tmp.operands().size()) > *array_size)
114  {
115  // cut off long strings. gcc does a warning for this
116  tmp.operands().resize(numeric_cast_v<std::size_t>(*array_size));
117  tmp.type()=type;
118  }
119  else if(mp_integer(tmp.operands().size()) < *array_size)
120  {
121  // fill up
122  tmp.type()=type;
123  const auto zero =
124  zero_initializer(full_type.subtype(), value.source_location(), *this);
125  if(!zero.has_value())
126  {
128  error() << "cannot zero-initialize array with subtype '"
129  << to_string(full_type.subtype()) << "'" << eom;
130  throw 0;
131  }
132  tmp.operands().resize(numeric_cast_v<std::size_t>(*array_size), *zero);
133  }
134  }
135 
136  return tmp;
137  }
138 
139  if(
140  value.id() == ID_string_constant && full_type.id() == ID_array &&
141  (full_type.subtype().id() == ID_signedbv ||
142  full_type.subtype().id() == ID_unsignedbv) &&
143  to_bitvector_type(full_type.subtype()).get_width() ==
144  char_type().get_width())
145  {
146  // will go away, to be replaced by the above block
147 
149  // adjust char type
150  tmp1.type().subtype()=full_type.subtype();
151 
152  exprt tmp2=tmp1.to_array_expr();
153 
154  if(full_type.id()==ID_array &&
155  to_array_type(full_type).is_complete())
156  {
157  // check size
158  const auto array_size =
159  numeric_cast<mp_integer>(to_array_type(full_type).size());
160  if(!array_size.has_value())
161  {
163  error() << "array size needs to be constant, got "
164  << to_string(to_array_type(full_type).size()) << eom;
165  throw 0;
166  }
167 
168  if(*array_size < 0)
169  {
171  error() << "array size must not be negative" << eom;
172  throw 0;
173  }
174 
175  if(mp_integer(tmp2.operands().size()) > *array_size)
176  {
177  // cut off long strings. gcc does a warning for this
178  tmp2.operands().resize(numeric_cast_v<std::size_t>(*array_size));
179  tmp2.type()=type;
180  }
181  else if(mp_integer(tmp2.operands().size()) < *array_size)
182  {
183  // fill up
184  tmp2.type()=type;
185  const auto zero =
186  zero_initializer(full_type.subtype(), value.source_location(), *this);
187  if(!zero.has_value())
188  {
190  error() << "cannot zero-initialize array with subtype '"
191  << to_string(full_type.subtype()) << "'" << eom;
192  throw 0;
193  }
194  tmp2.operands().resize(numeric_cast_v<std::size_t>(*array_size), *zero);
195  }
196  }
197 
198  return tmp2;
199  }
200 
201  if(full_type.id()==ID_array &&
202  to_array_type(full_type).size().is_nil())
203  {
205  error() << "type '" << to_string(full_type)
206  << "' cannot be initialized with '" << to_string(value) << "'"
207  << eom;
208  throw 0;
209  }
210 
211  if(value.id()==ID_designated_initializer)
212  {
214  error() << "type '" << to_string(full_type)
215  << "' cannot be initialized with designated initializer" << eom;
216  throw 0;
217  }
218 
219  exprt result=value;
220  implicit_typecast(result, type);
221  return result;
222 }
223 
225 {
226  // this one doesn't need initialization
227  if(has_prefix(id2string(symbol.name), CPROVER_PREFIX "constant_infinity"))
228  return;
229 
230  if(symbol.is_static_lifetime)
231  {
232  if(symbol.value.is_not_nil())
233  {
234  typecheck_expr(symbol.value);
235  do_initializer(symbol.value, symbol.type, true);
236 
237  // need to adjust size?
238  if(
239  symbol.type.id() == ID_array &&
240  to_array_type(symbol.type).size().is_nil())
241  symbol.type=symbol.value.type();
242  }
243  }
244  else if(!symbol.is_type)
245  {
246  if(symbol.is_macro)
247  {
248  // these must have a constant value
249  assert(symbol.value.is_not_nil());
250  typecheck_expr(symbol.value);
251  source_locationt location=symbol.value.source_location();
252  do_initializer(symbol.value, symbol.type, true);
253  make_constant(symbol.value);
254  }
255  else if(symbol.value.is_not_nil())
256  {
257  typecheck_expr(symbol.value);
258  do_initializer(symbol.value, symbol.type, true);
259 
260  // need to adjust size?
261  if(
262  symbol.type.id() == ID_array &&
263  to_array_type(symbol.type).size().is_nil())
264  symbol.type=symbol.value.type();
265  }
266  }
267 }
268 
270  const typet &type,
271  designatort &designator)
272 {
273  designatort::entryt entry(type);
274 
275  const typet &full_type=follow(type);
276 
277  if(full_type.id()==ID_struct)
278  {
279  const struct_typet &struct_type=to_struct_type(full_type);
280 
281  entry.size=struct_type.components().size();
282  entry.subtype.make_nil();
283  // only a top-level struct may end with a variable-length array
284  entry.vla_permitted=designator.empty();
285 
286  for(const auto &c : struct_type.components())
287  {
288  if(c.type().id() != ID_code && !c.get_is_padding())
289  {
290  entry.subtype = c.type();
291  break;
292  }
293 
294  ++entry.index;
295  }
296  }
297  else if(full_type.id()==ID_union)
298  {
299  const union_typet &union_type=to_union_type(full_type);
300 
301  if(union_type.components().empty())
302  {
303  entry.size=0;
304  entry.subtype.make_nil();
305  }
306  else
307  {
308  // The default is to initialize using the first member of the
309  // union.
310  entry.size=1;
311  entry.subtype=union_type.components().front().type();
312  }
313  }
314  else if(full_type.id()==ID_array)
315  {
316  const array_typet &array_type=to_array_type(full_type);
317 
318  if(array_type.size().is_nil())
319  {
320  entry.size=0;
321  entry.subtype=array_type.subtype();
322  }
323  else
324  {
325  const auto array_size = numeric_cast<mp_integer>(array_type.size());
326  if(!array_size.has_value())
327  {
328  error().source_location = array_type.size().source_location();
329  error() << "array has non-constant size '"
330  << to_string(array_type.size()) << "'" << eom;
331  throw 0;
332  }
333 
334  entry.size = numeric_cast_v<std::size_t>(*array_size);
335  entry.subtype=array_type.subtype();
336  }
337  }
338  else if(full_type.id()==ID_vector)
339  {
340  const vector_typet &vector_type=to_vector_type(full_type);
341 
342  const auto vector_size = numeric_cast<mp_integer>(vector_type.size());
343 
344  if(!vector_size.has_value())
345  {
346  error().source_location = vector_type.size().source_location();
347  error() << "vector has non-constant size '"
348  << to_string(vector_type.size()) << "'" << eom;
349  throw 0;
350  }
351 
352  entry.size = numeric_cast_v<std::size_t>(*vector_size);
353  entry.subtype=vector_type.subtype();
354  }
355  else
356  UNREACHABLE;
357 
358  designator.push_entry(entry);
359 }
360 
361 exprt::operandst::const_iterator c_typecheck_baset::do_designated_initializer(
362  exprt &result,
363  designatort &designator,
364  const exprt &initializer_list,
365  exprt::operandst::const_iterator init_it,
366  bool force_constant)
367 {
368  // copy the value, we may need to adjust it
369  exprt value=*init_it;
370 
371  assert(!designator.empty());
372 
373  if(value.id()==ID_designated_initializer)
374  {
375  assert(value.operands().size()==1);
376 
377  designator=
379  designator.front().type,
380  static_cast<const exprt &>(value.find(ID_designator)));
381 
382  assert(!designator.empty());
383 
384  // discard the return value
386  result, designator, value, value.operands().begin(), force_constant);
387  return ++init_it;
388  }
389 
390  exprt *dest=&result;
391 
392  // first phase: follow given designator
393 
394  for(size_t i=0; i<designator.size(); i++)
395  {
396  size_t index=designator[i].index;
397  const typet &type=designator[i].type;
398  const typet &full_type=follow(type);
399 
400  if(full_type.id()==ID_array ||
401  full_type.id()==ID_vector)
402  {
403  // zero_initializer may have built an array_of expression for a large
404  // array; as we have a designated initializer we need to have an array of
405  // individual objects
406  if(dest->id() == ID_array_of)
407  {
408  const array_typet array_type = to_array_type(dest->type());
409  const auto array_size = numeric_cast<mp_integer>(array_type.size());
410  if(!array_size.has_value())
411  {
413  error() << "cannot zero-initialize array with subtype '"
414  << to_string(full_type.subtype()) << "'" << eom;
415  throw 0;
416  }
417  const exprt zero = to_array_of_expr(*dest).what();
418  *dest = array_exprt{{}, array_type};
419  dest->operands().resize(numeric_cast_v<std::size_t>(*array_size), zero);
420  }
421 
422  if(index>=dest->operands().size())
423  {
424  if(full_type.id()==ID_array &&
425  (to_array_type(full_type).size().is_zero() ||
426  to_array_type(full_type).size().is_nil()))
427  {
428  // we are willing to grow an incomplete or zero-sized array
429  const auto zero = zero_initializer(
430  full_type.subtype(), value.source_location(), *this);
431  if(!zero.has_value())
432  {
434  error() << "cannot zero-initialize array with subtype '"
435  << to_string(full_type.subtype()) << "'" << eom;
436  throw 0;
437  }
438  dest->operands().resize(
439  numeric_cast_v<std::size_t>(index) + 1, *zero);
440 
441  // todo: adjust type!
442  }
443  else
444  {
446  error() << "array index designator " << index
447  << " out of bounds (" << dest->operands().size()
448  << ")" << eom;
449  throw 0;
450  }
451  }
452 
453  dest = &(dest->operands()[numeric_cast_v<std::size_t>(index)]);
454  }
455  else if(full_type.id()==ID_struct)
456  {
457  const struct_typet::componentst &components=
458  to_struct_type(full_type).components();
459 
460  if(index>=dest->operands().size())
461  {
463  error() << "structure member designator " << index
464  << " out of bounds (" << dest->operands().size()
465  << ")" << eom;
466  throw 0;
467  }
468 
469  DATA_INVARIANT(index<components.size(),
470  "member designator is bounded by components size");
471  DATA_INVARIANT(components[index].type().id()!=ID_code &&
472  !components[index].get_is_padding(),
473  "member designator points at data member");
474 
475  dest=&(dest->operands()[index]);
476  }
477  else if(full_type.id()==ID_union)
478  {
479  const union_typet &union_type=to_union_type(full_type);
480 
481  const union_typet::componentst &components=
482  union_type.components();
483 
484  if(components.empty())
485  {
487  error() << "union member designator found for empty union" << eom;
488  throw 0;
489  }
490  else if(init_it != initializer_list.operands().begin())
491  {
493  {
495  error() << "too many initializers" << eom;
496  throw 0;
497  }
498  else
499  {
501  warning() << "excess elements in union initializer" << eom;
502 
503  return ++init_it;
504  }
505  }
506  else if(index >= components.size())
507  {
509  error() << "union member designator " << index << " out of bounds ("
510  << components.size() << ")" << eom;
511  throw 0;
512  }
513 
514  const union_typet::componentt &component = components[index];
515 
516  if(
517  dest->id() == ID_union &&
518  to_union_expr(*dest).get_component_name() == component.get_name())
519  {
520  // Already right union component. We can initialize multiple submembers,
521  // so do not overwrite this.
522  dest = &(to_union_expr(*dest).op());
523  }
524  else if(dest->id() == ID_union)
525  {
526  // The designated initializer does not initialize the maximum member,
527  // which the (default) zero initializer prepared. Replace this by a
528  // component-specific initializer; other bytes have an unspecified value
529  // (C Standard 6.2.6.1(7)). In practice, objects of static lifetime are
530  // fully zero initialized, so we just byte-update on top of the existing
531  // zero initializer.
532  const auto zero =
533  zero_initializer(component.type(), value.source_location(), *this);
534  if(!zero.has_value())
535  {
537  error() << "cannot zero-initialize union component of type '"
538  << to_string(component.type()) << "'" << eom;
539  throw 0;
540  }
541 
543  {
544  byte_update_exprt byte_update =
545  make_byte_update(*dest, from_integer(0, index_type()), *zero);
546  byte_update.add_source_location() = value.source_location();
547  *dest = std::move(byte_update);
548  dest = &(to_byte_update_expr(*dest).op2());
549  }
550  else
551  {
552  union_exprt union_expr(component.get_name(), *zero, type);
553  union_expr.add_source_location() = value.source_location();
554  *dest = std::move(union_expr);
555  dest = &(to_union_expr(*dest).op());
556  }
557  }
558  else if(
559  dest->id() == ID_byte_update_big_endian ||
560  dest->id() == ID_byte_update_little_endian)
561  {
562  // handle the byte update introduced by an earlier initializer (if
563  // current_symbol.is_static_lifetime)
564  byte_update_exprt &byte_update = to_byte_update_expr(*dest);
565  dest = &byte_update.op2();
566  }
567  }
568  else
569  UNREACHABLE;
570  }
571 
572  // second phase: assign value
573  // for this, we may need to go down, adding to the designator
574 
575  while(true)
576  {
577  // see what type we have to initialize
578 
579  const typet &type=designator.back().subtype;
580  const typet &full_type=follow(type);
581 
582  // do we initialize a scalar?
583  if(full_type.id()!=ID_struct &&
584  full_type.id()!=ID_union &&
585  full_type.id()!=ID_array &&
586  full_type.id()!=ID_vector)
587  {
588  // The initializer for a scalar shall be a single expression,
589  // * optionally enclosed in braces. *
590 
591  if(value.id()==ID_initializer_list &&
592  value.operands().size()==1)
593  {
594  *dest =
595  do_initializer_rec(to_unary_expr(value).op(), type, force_constant);
596  }
597  else
598  *dest=do_initializer_rec(value, type, force_constant);
599 
600  assert(full_type==follow(dest->type()));
601 
602  return ++init_it; // done
603  }
604 
605  // union? The component in the zero initializer might
606  // not be the first one.
607  if(full_type.id()==ID_union)
608  {
609  const union_typet &union_type=to_union_type(full_type);
610 
611  const union_typet::componentst &components=
612  union_type.components();
613 
614  if(!components.empty())
615  {
617  union_type.components().front();
618 
619  const auto zero =
620  zero_initializer(component.type(), value.source_location(), *this);
621  if(!zero.has_value())
622  {
624  error() << "cannot zero-initialize union component of type '"
625  << to_string(component.type()) << "'" << eom;
626  throw 0;
627  }
628  union_exprt union_expr(component.get_name(), *zero, type);
629  union_expr.add_source_location()=value.source_location();
630  *dest=union_expr;
631  }
632  }
633 
634  // see what initializer we are given
635  if(value.id()==ID_initializer_list)
636  {
637  *dest=do_initializer_rec(value, type, force_constant);
638  return ++init_it; // done
639  }
640  else if(value.id()==ID_string_constant)
641  {
642  // We stop for initializers that are string-constants,
643  // which are like arrays. We only do so if we are to
644  // initialize an array of scalars.
645  if(
646  full_type.id() == ID_array &&
647  (full_type.subtype().id() == ID_signedbv ||
648  full_type.subtype().id() == ID_unsignedbv))
649  {
650  *dest=do_initializer_rec(value, type, force_constant);
651  return ++init_it; // done
652  }
653  }
654  else if(follow(value.type())==full_type)
655  {
656  // a struct/union/vector can be initialized directly with
657  // an expression of the right type. This doesn't
658  // work with arrays, unfortunately.
659  if(full_type.id()==ID_struct ||
660  full_type.id()==ID_union ||
661  full_type.id()==ID_vector)
662  {
663  *dest=value;
664  return ++init_it; // done
665  }
666  }
667 
668  assert(full_type.id()==ID_struct ||
669  full_type.id()==ID_union ||
670  full_type.id()==ID_array ||
671  full_type.id()==ID_vector);
672 
673  // we are initializing a compound type, and enter it!
674  // this may change the type, full_type might not be valid any more
675  const typet dest_type=full_type;
676  const bool vla_permitted=designator.back().vla_permitted;
677  designator_enter(type, designator);
678 
679  // GCC permits (though issuing a warning with -Wall) composite
680  // types built from flat initializer lists
681  if(dest->operands().empty())
682  {
684  warning() << "initialisation of " << dest_type.id()
685  << " requires initializer list, found " << value.id()
686  << " instead" << eom;
687 
688  // in case of a variable-length array consume all remaining
689  // initializer elements
690  if(vla_permitted &&
691  dest_type.id()==ID_array &&
692  (to_array_type(dest_type).size().is_zero() ||
693  to_array_type(dest_type).size().is_nil()))
694  {
695  value.id(ID_initializer_list);
696  value.operands().clear();
697  for( ; init_it!=initializer_list.operands().end(); ++init_it)
698  value.copy_to_operands(*init_it);
699  *dest=do_initializer_rec(value, dest_type, force_constant);
700 
701  return init_it;
702  }
703  else
704  {
706  error() << "cannot initialize type '" << to_string(dest_type)
707  << "' using value '" << to_string(value) << "'" << eom;
708  throw 0;
709  }
710  }
711 
712  dest = &(to_multi_ary_expr(*dest).op0());
713 
714  // we run into another loop iteration
715  }
716 
717  return ++init_it;
718 }
719 
721 {
722  assert(!designator.empty());
723 
724  while(true)
725  {
726  designatort::entryt &entry=designator[designator.size()-1];
727  const typet &full_type=follow(entry.type);
728 
729  entry.index++;
730 
731  if(full_type.id()==ID_array &&
732  to_array_type(full_type).size().is_nil())
733  return; // we will keep going forever
734 
735  if(full_type.id()==ID_struct &&
736  entry.index<entry.size)
737  {
738  // need to adjust subtype
739  const struct_typet &struct_type=
740  to_struct_type(full_type);
741  const struct_typet::componentst &components=
742  struct_type.components();
743  assert(components.size()==entry.size);
744 
745  // we skip over any padding or code
746  // we also skip over anonymous members
747  while(entry.index < entry.size &&
748  (components[entry.index].get_is_padding() ||
749  (components[entry.index].get_anonymous() &&
750  components[entry.index].type().id() != ID_struct_tag &&
751  components[entry.index].type().id() != ID_union_tag) ||
752  components[entry.index].type().id() == ID_code))
753  {
754  entry.index++;
755  }
756 
757  if(entry.index<entry.size)
758  entry.subtype=components[entry.index].type();
759  }
760 
761  if(entry.index<entry.size)
762  return; // done
763 
764  if(designator.size()==1)
765  return; // done
766 
767  // pop entry
768  designator.pop_entry();
769 
770  assert(!designator.empty());
771  }
772 }
773 
775  const typet &src_type,
776  const exprt &src)
777 {
778  assert(!src.operands().empty());
779 
780  typet type=src_type;
781  designatort designator;
782 
783  forall_operands(it, src)
784  {
785  const exprt &d_op=*it;
786  designatort::entryt entry(type);
787  const typet &full_type=follow(entry.type);
788 
789  if(full_type.id()==ID_array)
790  {
791  if(d_op.id()!=ID_index)
792  {
794  error() << "expected array index designator" << eom;
795  throw 0;
796  }
797 
798  exprt tmp_index = to_unary_expr(d_op).op();
799  make_constant_index(tmp_index);
800 
801  mp_integer index, size;
802 
803  if(to_integer(to_constant_expr(tmp_index), index))
804  {
806  error() << "expected constant array index designator" << eom;
807  throw 0;
808  }
809 
810  if(to_array_type(full_type).size().is_nil())
811  size=0;
812  else if(
813  const auto size_opt =
814  numeric_cast<mp_integer>(to_array_type(full_type).size()))
815  size = *size_opt;
816  else
817  {
819  error() << "expected constant array size" << eom;
820  throw 0;
821  }
822 
823  entry.index = numeric_cast_v<std::size_t>(index);
824  entry.size = numeric_cast_v<std::size_t>(size);
825  entry.subtype=full_type.subtype();
826  }
827  else if(full_type.id()==ID_struct ||
828  full_type.id()==ID_union)
829  {
830  const struct_union_typet &struct_union_type=
831  to_struct_union_type(full_type);
832 
833  if(d_op.id()!=ID_member)
834  {
836  error() << "expected member designator" << eom;
837  throw 0;
838  }
839 
840  const irep_idt &component_name=d_op.get(ID_component_name);
841 
842  if(struct_union_type.has_component(component_name))
843  {
844  // a direct member
845  entry.index=struct_union_type.component_number(component_name);
846  entry.size=struct_union_type.components().size();
847  entry.subtype=struct_union_type.components()[entry.index].type();
848  }
849  else
850  {
851  // We will search for anonymous members,
852  // in a loop. This isn't supported by gcc, but icc does allow it.
853 
854  bool found=false, repeat;
855  typet tmp_type=entry.type;
856 
857  do
858  {
859  repeat=false;
860  std::size_t number = 0;
861  const struct_union_typet::componentst &components=
863 
864  for(const auto &c : components)
865  {
866  if(c.get_name() == component_name)
867  {
868  // done!
869  entry.index=number;
870  entry.size=components.size();
871  entry.subtype = c.type();
872  entry.type=tmp_type;
873  }
874  else if(
875  c.get_anonymous() &&
876  (c.type().id() == ID_struct_tag ||
877  c.type().id() == ID_union_tag) &&
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  {
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  {
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  assert(!designator.empty());
918 
919  return designator;
920 }
921 
923  const exprt &value,
924  const typet &type,
925  bool force_constant)
926 {
927  assert(value.id()==ID_initializer_list);
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  (full_type.subtype().id() == ID_signedbv ||
937  full_type.subtype().id() == ID_unsignedbv) &&
938  to_bitvector_type(full_type.subtype()).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 
951  exprt result;
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=exprt(ID_array, 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 
1004  designatort current_designator;
1005 
1006  designator_enter(type, current_designator);
1007 
1008  const exprt::operandst &operands=value.operands();
1009  for(exprt::operandst::const_iterator it=operands.begin();
1010  it!=operands.end(); ) // no ++it
1011  {
1013  result, current_designator, value, it, force_constant);
1014 
1015  // increase designator -- might go up
1016  increment_designator(current_designator);
1017  }
1018 
1019  // make sure we didn't mess up index computation
1020  if(full_type.id()==ID_struct)
1021  {
1022  assert(result.operands().size()==
1023  to_struct_type(full_type).components().size());
1024  }
1025 
1026  if(full_type.id()==ID_array &&
1027  to_array_type(full_type).size().is_nil())
1028  {
1029  // make complete by setting array size
1030  size_t size=result.operands().size();
1031  result.type().id(ID_array);
1032  result.type().set(ID_size, from_integer(size, index_type()));
1033  }
1034 
1035  return result;
1036 }
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 index_type()
Definition: c_types.cpp:16
bitvector_typet char_type()
Definition: c_types.cpp:114
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition: c_types.h:149
Array constructor from list of elements.
Definition: std_expr.h:1467
exprt & what()
Definition: std_expr.h:1419
Arrays with given size.
Definition: std_types.h:763
const exprt & size() const
Definition: std_types.h:771
std::size_t get_width() const
Definition: std_types.h:843
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_namet &name) const
Definition: irep.cpp:58
const irept & find(const irep_namet &name) const
Definition: irep.cpp:106
bool is_not_nil() const
Definition: irep.h:391
const irep_idt & id() const
Definition: irep.h:407
void make_nil()
Definition: irep.h:465
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:45
bool is_nil() const
Definition: irep.h:387
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:32
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:28
const typet & subtype() const
Definition: type.h:47
const exprt & op() const
Definition: std_expr.h:293
Union constructor from single element.
Definition: std_expr.h:1602
irep_idt get_component_name() const
Definition: std_expr.h:1610
The union type.
Definition: c_types.h:112
The vector type.
Definition: std_types.h:975
const constant_exprt & size() const
Definition: std_types.cpp:239
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:49
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:2786
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
Definition: std_expr.h:1648
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:1447
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:1000
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:813
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:195
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.