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 
518  dest->id() == ID_union, "union should be zero initialized");
519 
520  if(dest->get(ID_component_name) == component.get_name())
521  {
522  // Already right union component. We can initialize multiple submembers,
523  // so do not overwrite this.
524  dest = &(to_union_expr(*dest).op());
525  }
526  else
527  {
528  // The first component is not the maximum member, which the (default)
529  // zero initializer prepared. Replace this by a component-specific
530  // initializer; other bytes have an unspecified value (C Standard
531  // 6.2.6.1(7)). In practice, objects of static lifetime are fully zero
532  // initialized.
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  }
560  else
561  UNREACHABLE;
562  }
563 
564  // second phase: assign value
565  // for this, we may need to go down, adding to the designator
566 
567  while(true)
568  {
569  // see what type we have to initialize
570 
571  const typet &type=designator.back().subtype;
572  const typet &full_type=follow(type);
573 
574  // do we initialize a scalar?
575  if(full_type.id()!=ID_struct &&
576  full_type.id()!=ID_union &&
577  full_type.id()!=ID_array &&
578  full_type.id()!=ID_vector)
579  {
580  // The initializer for a scalar shall be a single expression,
581  // * optionally enclosed in braces. *
582 
583  if(value.id()==ID_initializer_list &&
584  value.operands().size()==1)
585  {
586  *dest =
587  do_initializer_rec(to_unary_expr(value).op(), type, force_constant);
588  }
589  else
590  *dest=do_initializer_rec(value, type, force_constant);
591 
592  assert(full_type==follow(dest->type()));
593 
594  return ++init_it; // done
595  }
596 
597  // union? The component in the zero initializer might
598  // not be the first one.
599  if(full_type.id()==ID_union)
600  {
601  const union_typet &union_type=to_union_type(full_type);
602 
603  const union_typet::componentst &components=
604  union_type.components();
605 
606  if(!components.empty())
607  {
609  union_type.components().front();
610 
611  const auto zero =
612  zero_initializer(component.type(), value.source_location(), *this);
613  if(!zero.has_value())
614  {
616  error() << "cannot zero-initialize union component of type '"
617  << to_string(component.type()) << "'" << eom;
618  throw 0;
619  }
620  union_exprt union_expr(component.get_name(), *zero, type);
621  union_expr.add_source_location()=value.source_location();
622  *dest=union_expr;
623  }
624  }
625 
626  // see what initializer we are given
627  if(value.id()==ID_initializer_list)
628  {
629  *dest=do_initializer_rec(value, type, force_constant);
630  return ++init_it; // done
631  }
632  else if(value.id()==ID_string_constant)
633  {
634  // We stop for initializers that are string-constants,
635  // which are like arrays. We only do so if we are to
636  // initialize an array of scalars.
637  if(
638  full_type.id() == ID_array &&
639  (full_type.subtype().id() == ID_signedbv ||
640  full_type.subtype().id() == ID_unsignedbv))
641  {
642  *dest=do_initializer_rec(value, type, force_constant);
643  return ++init_it; // done
644  }
645  }
646  else if(follow(value.type())==full_type)
647  {
648  // a struct/union/vector can be initialized directly with
649  // an expression of the right type. This doesn't
650  // work with arrays, unfortunately.
651  if(full_type.id()==ID_struct ||
652  full_type.id()==ID_union ||
653  full_type.id()==ID_vector)
654  {
655  *dest=value;
656  return ++init_it; // done
657  }
658  }
659 
660  assert(full_type.id()==ID_struct ||
661  full_type.id()==ID_union ||
662  full_type.id()==ID_array ||
663  full_type.id()==ID_vector);
664 
665  // we are initializing a compound type, and enter it!
666  // this may change the type, full_type might not be valid any more
667  const typet dest_type=full_type;
668  const bool vla_permitted=designator.back().vla_permitted;
669  designator_enter(type, designator);
670 
671  // GCC permits (though issuing a warning with -Wall) composite
672  // types built from flat initializer lists
673  if(dest->operands().empty())
674  {
676  warning() << "initialisation of " << dest_type.id()
677  << " requires initializer list, found " << value.id()
678  << " instead" << eom;
679 
680  // in case of a variable-length array consume all remaining
681  // initializer elements
682  if(vla_permitted &&
683  dest_type.id()==ID_array &&
684  (to_array_type(dest_type).size().is_zero() ||
685  to_array_type(dest_type).size().is_nil()))
686  {
687  value.id(ID_initializer_list);
688  value.operands().clear();
689  for( ; init_it!=initializer_list.operands().end(); ++init_it)
690  value.copy_to_operands(*init_it);
691  *dest=do_initializer_rec(value, dest_type, force_constant);
692 
693  return init_it;
694  }
695  else
696  {
698  error() << "cannot initialize type '" << to_string(dest_type)
699  << "' using value '" << to_string(value) << "'" << eom;
700  throw 0;
701  }
702  }
703 
704  dest = &(to_multi_ary_expr(*dest).op0());
705 
706  // we run into another loop iteration
707  }
708 
709  return ++init_it;
710 }
711 
713 {
714  assert(!designator.empty());
715 
716  while(true)
717  {
718  designatort::entryt &entry=designator[designator.size()-1];
719  const typet &full_type=follow(entry.type);
720 
721  entry.index++;
722 
723  if(full_type.id()==ID_array &&
724  to_array_type(full_type).size().is_nil())
725  return; // we will keep going forever
726 
727  if(full_type.id()==ID_struct &&
728  entry.index<entry.size)
729  {
730  // need to adjust subtype
731  const struct_typet &struct_type=
732  to_struct_type(full_type);
733  const struct_typet::componentst &components=
734  struct_type.components();
735  assert(components.size()==entry.size);
736 
737  // we skip over any padding or code
738  // we also skip over anonymous members
739  while(entry.index < entry.size &&
740  (components[entry.index].get_is_padding() ||
741  (components[entry.index].get_anonymous() &&
742  components[entry.index].type().id() != ID_struct_tag &&
743  components[entry.index].type().id() != ID_union_tag) ||
744  components[entry.index].type().id() == ID_code))
745  {
746  entry.index++;
747  }
748 
749  if(entry.index<entry.size)
750  entry.subtype=components[entry.index].type();
751  }
752 
753  if(entry.index<entry.size)
754  return; // done
755 
756  if(designator.size()==1)
757  return; // done
758 
759  // pop entry
760  designator.pop_entry();
761 
762  assert(!designator.empty());
763  }
764 }
765 
767  const typet &src_type,
768  const exprt &src)
769 {
770  assert(!src.operands().empty());
771 
772  typet type=src_type;
773  designatort designator;
774 
775  forall_operands(it, src)
776  {
777  const exprt &d_op=*it;
778  designatort::entryt entry(type);
779  const typet &full_type=follow(entry.type);
780 
781  if(full_type.id()==ID_array)
782  {
783  if(d_op.id()!=ID_index)
784  {
786  error() << "expected array index designator" << eom;
787  throw 0;
788  }
789 
790  exprt tmp_index = to_unary_expr(d_op).op();
791  make_constant_index(tmp_index);
792 
793  mp_integer index, size;
794 
795  if(to_integer(to_constant_expr(tmp_index), index))
796  {
798  error() << "expected constant array index designator" << eom;
799  throw 0;
800  }
801 
802  if(to_array_type(full_type).size().is_nil())
803  size=0;
804  else if(
805  const auto size_opt =
806  numeric_cast<mp_integer>(to_array_type(full_type).size()))
807  size = *size_opt;
808  else
809  {
811  error() << "expected constant array size" << eom;
812  throw 0;
813  }
814 
815  entry.index = numeric_cast_v<std::size_t>(index);
816  entry.size = numeric_cast_v<std::size_t>(size);
817  entry.subtype=full_type.subtype();
818  }
819  else if(full_type.id()==ID_struct ||
820  full_type.id()==ID_union)
821  {
822  const struct_union_typet &struct_union_type=
823  to_struct_union_type(full_type);
824 
825  if(d_op.id()!=ID_member)
826  {
828  error() << "expected member designator" << eom;
829  throw 0;
830  }
831 
832  const irep_idt &component_name=d_op.get(ID_component_name);
833 
834  if(struct_union_type.has_component(component_name))
835  {
836  // a direct member
837  entry.index=struct_union_type.component_number(component_name);
838  entry.size=struct_union_type.components().size();
839  entry.subtype=struct_union_type.components()[entry.index].type();
840  }
841  else
842  {
843  // We will search for anonymous members,
844  // in a loop. This isn't supported by gcc, but icc does allow it.
845 
846  bool found=false, repeat;
847  typet tmp_type=entry.type;
848 
849  do
850  {
851  repeat=false;
852  std::size_t number = 0;
853  const struct_union_typet::componentst &components=
855 
856  for(const auto &c : components)
857  {
858  if(c.get_name() == component_name)
859  {
860  // done!
861  entry.index=number;
862  entry.size=components.size();
863  entry.subtype = c.type();
864  entry.type=tmp_type;
865  }
866  else if(
867  c.get_anonymous() &&
868  (c.type().id() == ID_struct_tag ||
869  c.type().id() == ID_union_tag) &&
870  has_component_rec(c.type(), component_name, *this))
871  {
872  entry.index=number;
873  entry.size=components.size();
874  entry.subtype = c.type();
875  entry.type=tmp_type;
876  tmp_type=entry.subtype;
877  designator.push_entry(entry);
878  found=repeat=true;
879  break;
880  }
881 
882  ++number;
883  }
884  }
885  while(repeat);
886 
887  if(!found)
888  {
890  error() << "failed to find struct component '" << component_name
891  << "' in initialization of '" << to_string(struct_union_type)
892  << "'" << eom;
893  throw 0;
894  }
895  }
896  }
897  else
898  {
900  error() << "designated initializers cannot initialize '"
901  << to_string(full_type) << "'" << eom;
902  throw 0;
903  }
904 
905  type=entry.subtype;
906  designator.push_entry(entry);
907  }
908 
909  assert(!designator.empty());
910 
911  return designator;
912 }
913 
915  const exprt &value,
916  const typet &type,
917  bool force_constant)
918 {
919  assert(value.id()==ID_initializer_list);
920 
921  const typet &full_type=follow(type);
922 
923  // 6.7.9, 14: An array of character type may be initialized by a character
924  // string literal or UTF-8 string literal, optionally enclosed in braces.
925  if(
926  full_type.id() == ID_array && value.operands().size() >= 1 &&
927  to_multi_ary_expr(value).op0().id() == ID_string_constant &&
928  (full_type.subtype().id() == ID_signedbv ||
929  full_type.subtype().id() == ID_unsignedbv) &&
930  to_bitvector_type(full_type.subtype()).get_width() ==
931  char_type().get_width())
932  {
933  if(value.operands().size() > 1)
934  {
936  warning() << "ignoring excess initializers" << eom;
937  }
938 
939  return do_initializer_rec(
940  to_multi_ary_expr(value).op0(), type, force_constant);
941  }
942 
943  exprt result;
944  if(full_type.id()==ID_struct ||
945  full_type.id()==ID_union ||
946  full_type.id()==ID_vector)
947  {
948  // start with zero everywhere
949  const auto zero = zero_initializer(type, value.source_location(), *this);
950  if(!zero.has_value())
951  {
953  error() << "cannot zero-initialize '" << to_string(full_type) << "'"
954  << eom;
955  throw 0;
956  }
957  result = *zero;
958  }
959  else if(full_type.id()==ID_array)
960  {
961  if(to_array_type(full_type).size().is_nil())
962  {
963  // start with empty array
964  result=exprt(ID_array, full_type);
965  result.add_source_location()=value.source_location();
966  }
967  else
968  {
969  // start with zero everywhere
970  const auto zero = zero_initializer(type, value.source_location(), *this);
971  if(!zero.has_value())
972  {
974  error() << "cannot zero-initialize '" << to_string(full_type) << "'"
975  << eom;
976  throw 0;
977  }
978  result = *zero;
979  }
980  }
981  else
982  {
983  // The initializer for a scalar shall be a single expression,
984  // * optionally enclosed in braces. *
985 
986  if(value.operands().size()==1)
987  return do_initializer_rec(
988  to_unary_expr(value).op(), type, force_constant);
989 
991  error() << "cannot initialize '" << to_string(full_type)
992  << "' with an initializer list" << eom;
993  throw 0;
994  }
995 
996  designatort current_designator;
997 
998  designator_enter(type, current_designator);
999 
1000  const exprt::operandst &operands=value.operands();
1001  for(exprt::operandst::const_iterator it=operands.begin();
1002  it!=operands.end(); ) // no ++it
1003  {
1005  result, current_designator, value, it, force_constant);
1006 
1007  // increase designator -- might go up
1008  increment_designator(current_designator);
1009  }
1010 
1011  // make sure we didn't mess up index computation
1012  if(full_type.id()==ID_struct)
1013  {
1014  assert(result.operands().size()==
1015  to_struct_type(full_type).components().size());
1016  }
1017 
1018  if(full_type.id()==ID_array &&
1019  to_array_type(full_type).size().is_nil())
1020  {
1021  // make complete by setting array size
1022  size_t size=result.operands().size();
1023  result.type().id(ID_array);
1024  result.type().set(ID_size, from_integer(size, index_type()));
1025  }
1026 
1027  return result;
1028 }
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:133
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:142
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
to_unary_expr
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:329
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:303
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:209
array_of_exprt::what
exprt & what()
Definition: std_expr.h:1334
ternary_exprt::op2
exprt & op2()
Definition: expr.h:109
irept::make_nil
void make_nil()
Definition: irep.h:464
typet
The type of an expression, extends irept.
Definition: type.h:28
c_typecheck_base.h
ANSI-C Language Type Checking.
c_typecheck_baset::do_initializer
virtual void do_initializer(symbolt &symbol)
Definition: c_typecheck_initializer.cpp:225
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:57
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:103
prefix.h
union_exprt
Union constructor from single element.
Definition: std_expr.h:1517
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:1362
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:135
to_union_expr
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
Definition: std_expr.h:1563
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:1764
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:19
messaget::eom
static eomt eom
Definition: message.h:297
configt::ansi_c
struct configt::ansi_ct ansi_c
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:50
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:3769
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:914
designatort::pop_entry
void pop_entry()
Definition: designator.h:50
array_typet::size
const exprt & size() const
Definition: std_types.h:976
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:179
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:152
c_typecheck_baset::make_constant_index
virtual void make_constant_index(exprt &expr)
Definition: c_typecheck_expr.cpp:3790
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: std_types.h:393
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:294
cprover_prefix.h
vector_typet::size
const constant_exprt & size() const
Definition: std_types.cpp:282
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:43
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:1048
struct_union_typet::componentt
Definition: std_types.h:64
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:226
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:968
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:51
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:766
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:99
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:1018
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:1789
anonymous_member.h
C Language Type Checking.
c_typecheck_baset::increment_designator
void increment_designator(designatort &designator)
Definition: c_typecheck_initializer.cpp:712
exprt::operands
operandst & operands()
Definition: expr.h:96
to_union_type
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition: std_types.h:430
designatort::entryt::subtype
typet subtype
Definition: designator.h:28
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:239
messaget::warning
mstreamt & warning() const
Definition: message.h:404
multi_ary_exprt::op0
exprt & op0()
Definition: std_expr.h:761
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:816
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:234
array_exprt
Array constructor from list of elements.
Definition: std_expr.h:1382
c_types.h
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
to_bitvector_type
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Definition: std_types.h:1096
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:2701