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/c_types.h>
16 #include <util/cprover_prefix.h>
17 #include <util/expr_initializer.h>
18 #include <util/prefix.h>
19 #include <util/simplify_expr.h>
20 #include <util/std_types.h>
21 #include <util/string_constant.h>
22 
23 #include "anonymous_member.h"
24 
26  exprt &initializer,
27  const typet &type,
28  bool force_constant)
29 {
30  exprt result=do_initializer_rec(initializer, type, force_constant);
31 
32  if(type.id()==ID_array)
33  {
34  const typet &result_type = result.type();
35  DATA_INVARIANT(result_type.id()==ID_array &&
36  to_array_type(result_type).size().is_not_nil(),
37  "any array must have a size");
38 
39  // we don't allow initialisation with symbols of array type
40  if(result.id() != ID_array && result.id() != ID_array_of)
41  {
43  error() << "invalid array initializer " << to_string(result)
44  << eom;
45  throw 0;
46  }
47  }
48 
49  initializer=result;
50 }
51 
54  const exprt &value,
55  const typet &type,
56  bool force_constant)
57 {
58  const typet &full_type=follow(type);
59 
60  if(
61  (full_type.id() == ID_struct || full_type.id() == ID_union) &&
62  to_struct_union_type(full_type).is_incomplete())
63  {
65  error() << "type '" << to_string(type)
66  << "' is still incomplete -- cannot initialize" << eom;
67  throw 0;
68  }
69 
70  if(value.id()==ID_initializer_list)
71  return do_initializer_list(value, type, force_constant);
72 
73  if(
74  value.id() == ID_array && value.get_bool(ID_C_string_constant) &&
75  full_type.id() == ID_array &&
76  (full_type.subtype().id() == ID_signedbv ||
77  full_type.subtype().id() == ID_unsignedbv) &&
78  to_bitvector_type(full_type.subtype()).get_width() ==
80  {
81  exprt tmp=value;
82 
83  // adjust char type
84  tmp.type().subtype()=full_type.subtype();
85 
86  Forall_operands(it, tmp)
87  it->type()=full_type.subtype();
88 
89  if(full_type.id()==ID_array &&
90  to_array_type(full_type).is_complete())
91  {
92  // check size
93  const auto array_size =
94  numeric_cast<mp_integer>(to_array_type(full_type).size());
95  if(!array_size.has_value())
96  {
98  error() << "array size needs to be constant, got "
99  << to_string(to_array_type(full_type).size()) << eom;
100  throw 0;
101  }
102 
103  if(*array_size < 0)
104  {
106  error() << "array size must not be negative" << eom;
107  throw 0;
108  }
109 
110  if(mp_integer(tmp.operands().size()) > *array_size)
111  {
112  // cut off long strings. gcc does a warning for this
113  tmp.operands().resize(numeric_cast_v<std::size_t>(*array_size));
114  tmp.type()=type;
115  }
116  else if(mp_integer(tmp.operands().size()) < *array_size)
117  {
118  // fill up
119  tmp.type()=type;
120  const auto zero =
121  zero_initializer(full_type.subtype(), value.source_location(), *this);
122  if(!zero.has_value())
123  {
125  error() << "cannot zero-initialize array with subtype '"
126  << to_string(full_type.subtype()) << "'" << eom;
127  throw 0;
128  }
129  tmp.operands().resize(numeric_cast_v<std::size_t>(*array_size), *zero);
130  }
131  }
132 
133  return tmp;
134  }
135 
136  if(
137  value.id() == ID_string_constant && full_type.id() == ID_array &&
138  (full_type.subtype().id() == ID_signedbv ||
139  full_type.subtype().id() == ID_unsignedbv) &&
140  to_bitvector_type(full_type.subtype()).get_width() ==
141  char_type().get_width())
142  {
143  // will go away, to be replaced by the above block
144 
146  // adjust char type
147  tmp1.type().subtype()=full_type.subtype();
148 
149  exprt tmp2=tmp1.to_array_expr();
150 
151  if(full_type.id()==ID_array &&
152  to_array_type(full_type).is_complete())
153  {
154  // check size
155  const auto array_size =
156  numeric_cast<mp_integer>(to_array_type(full_type).size());
157  if(!array_size.has_value())
158  {
160  error() << "array size needs to be constant, got "
161  << to_string(to_array_type(full_type).size()) << eom;
162  throw 0;
163  }
164 
165  if(*array_size < 0)
166  {
168  error() << "array size must not be negative" << eom;
169  throw 0;
170  }
171 
172  if(mp_integer(tmp2.operands().size()) > *array_size)
173  {
174  // cut off long strings. gcc does a warning for this
175  tmp2.operands().resize(numeric_cast_v<std::size_t>(*array_size));
176  tmp2.type()=type;
177  }
178  else if(mp_integer(tmp2.operands().size()) < *array_size)
179  {
180  // fill up
181  tmp2.type()=type;
182  const auto zero =
183  zero_initializer(full_type.subtype(), value.source_location(), *this);
184  if(!zero.has_value())
185  {
187  error() << "cannot zero-initialize array with subtype '"
188  << to_string(full_type.subtype()) << "'" << eom;
189  throw 0;
190  }
191  tmp2.operands().resize(numeric_cast_v<std::size_t>(*array_size), *zero);
192  }
193  }
194 
195  return tmp2;
196  }
197 
198  if(full_type.id()==ID_array &&
199  to_array_type(full_type).size().is_nil())
200  {
202  error() << "type '" << to_string(full_type)
203  << "' cannot be initialized with '" << to_string(value) << "'"
204  << eom;
205  throw 0;
206  }
207 
208  if(value.id()==ID_designated_initializer)
209  {
211  error() << "type '" << to_string(full_type)
212  << "' cannot be initialized with designated initializer" << eom;
213  throw 0;
214  }
215 
216  exprt result=value;
217  implicit_typecast(result, type);
218  return result;
219 }
220 
222 {
223  // this one doesn't need initialization
224  if(has_prefix(id2string(symbol.name), CPROVER_PREFIX "constant_infinity"))
225  return;
226 
227  if(symbol.is_static_lifetime)
228  {
229  if(symbol.value.is_not_nil())
230  {
231  typecheck_expr(symbol.value);
232  do_initializer(symbol.value, symbol.type, true);
233 
234  // need to adjust size?
235  if(
236  symbol.type.id() == ID_array &&
237  to_array_type(symbol.type).size().is_nil())
238  symbol.type=symbol.value.type();
239  }
240  }
241  else if(!symbol.is_type)
242  {
243  if(symbol.is_macro)
244  {
245  // these must have a constant value
246  assert(symbol.value.is_not_nil());
247  typecheck_expr(symbol.value);
248  source_locationt location=symbol.value.source_location();
249  do_initializer(symbol.value, symbol.type, true);
250  make_constant(symbol.value);
251  }
252  else if(symbol.value.is_not_nil())
253  {
254  typecheck_expr(symbol.value);
255  do_initializer(symbol.value, symbol.type, true);
256 
257  // need to adjust size?
258  if(
259  symbol.type.id() == ID_array &&
260  to_array_type(symbol.type).size().is_nil())
261  symbol.type=symbol.value.type();
262  }
263  }
264 }
265 
267  const typet &type,
268  designatort &designator)
269 {
270  designatort::entryt entry(type);
271 
272  const typet &full_type=follow(type);
273 
274  if(full_type.id()==ID_struct)
275  {
276  const struct_typet &struct_type=to_struct_type(full_type);
277 
278  entry.size=struct_type.components().size();
279  entry.subtype.make_nil();
280  // only a top-level struct may end with a variable-length array
281  entry.vla_permitted=designator.empty();
282 
283  for(const auto &c : struct_type.components())
284  {
285  if(c.type().id() != ID_code && !c.get_is_padding())
286  {
287  entry.subtype = c.type();
288  break;
289  }
290 
291  ++entry.index;
292  }
293  }
294  else if(full_type.id()==ID_union)
295  {
296  const union_typet &union_type=to_union_type(full_type);
297 
298  if(union_type.components().empty())
299  {
300  entry.size=0;
301  entry.subtype.make_nil();
302  }
303  else
304  {
305  // The default is to initialize using the first member of the
306  // union.
307  entry.size=1;
308  entry.subtype=union_type.components().front().type();
309  }
310  }
311  else if(full_type.id()==ID_array)
312  {
313  const array_typet &array_type=to_array_type(full_type);
314 
315  if(array_type.size().is_nil())
316  {
317  entry.size=0;
318  entry.subtype=array_type.subtype();
319  }
320  else
321  {
322  const auto array_size = numeric_cast<mp_integer>(array_type.size());
323  if(!array_size.has_value())
324  {
325  error().source_location = array_type.size().source_location();
326  error() << "array has non-constant size '"
327  << to_string(array_type.size()) << "'" << eom;
328  throw 0;
329  }
330 
331  entry.size = numeric_cast_v<std::size_t>(*array_size);
332  entry.subtype=array_type.subtype();
333  }
334  }
335  else if(full_type.id()==ID_vector)
336  {
337  const vector_typet &vector_type=to_vector_type(full_type);
338 
339  const auto vector_size = numeric_cast<mp_integer>(vector_type.size());
340 
341  if(!vector_size.has_value())
342  {
343  error().source_location = vector_type.size().source_location();
344  error() << "vector has non-constant size '"
345  << to_string(vector_type.size()) << "'" << eom;
346  throw 0;
347  }
348 
349  entry.size = numeric_cast_v<std::size_t>(*vector_size);
350  entry.subtype=vector_type.subtype();
351  }
352  else
353  UNREACHABLE;
354 
355  designator.push_entry(entry);
356 }
357 
358 exprt::operandst::const_iterator c_typecheck_baset::do_designated_initializer(
359  exprt &result,
360  designatort &designator,
361  const exprt &initializer_list,
362  exprt::operandst::const_iterator init_it,
363  bool force_constant)
364 {
365  // copy the value, we may need to adjust it
366  exprt value=*init_it;
367 
368  assert(!designator.empty());
369 
370  if(value.id()==ID_designated_initializer)
371  {
372  assert(value.operands().size()==1);
373 
374  designator=
376  designator.front().type,
377  static_cast<const exprt &>(value.find(ID_designator)));
378 
379  assert(!designator.empty());
380 
381  // discard the return value
383  result, designator, value, value.operands().begin(), force_constant);
384  return ++init_it;
385  }
386 
387  exprt *dest=&result;
388 
389  // first phase: follow given designator
390 
391  for(size_t i=0; i<designator.size(); i++)
392  {
393  size_t index=designator[i].index;
394  const typet &type=designator[i].type;
395  const typet &full_type=follow(type);
396 
397  if(full_type.id()==ID_array ||
398  full_type.id()==ID_vector)
399  {
400  // zero_initializer may have built an array_of expression for a large
401  // array; as we have a designated initializer we need to have an array of
402  // individual objects
403  if(dest->id() == ID_array_of)
404  {
405  const array_typet array_type = to_array_type(dest->type());
406  const auto array_size = numeric_cast<mp_integer>(array_type.size());
407  if(!array_size.has_value())
408  {
410  error() << "cannot zero-initialize array with subtype '"
411  << to_string(full_type.subtype()) << "'" << eom;
412  throw 0;
413  }
414  const exprt zero = to_array_of_expr(*dest).what();
415  *dest = array_exprt{{}, array_type};
416  dest->operands().resize(numeric_cast_v<std::size_t>(*array_size), zero);
417  }
418 
419  if(index>=dest->operands().size())
420  {
421  if(full_type.id()==ID_array &&
422  (to_array_type(full_type).size().is_zero() ||
423  to_array_type(full_type).size().is_nil()))
424  {
425  // we are willing to grow an incomplete or zero-sized array
426  const auto zero = zero_initializer(
427  full_type.subtype(), value.source_location(), *this);
428  if(!zero.has_value())
429  {
431  error() << "cannot zero-initialize array with subtype '"
432  << to_string(full_type.subtype()) << "'" << eom;
433  throw 0;
434  }
435  dest->operands().resize(
436  numeric_cast_v<std::size_t>(index) + 1, *zero);
437 
438  // todo: adjust type!
439  }
440  else
441  {
443  error() << "array index designator " << index
444  << " out of bounds (" << dest->operands().size()
445  << ")" << eom;
446  throw 0;
447  }
448  }
449 
450  dest = &(dest->operands()[numeric_cast_v<std::size_t>(index)]);
451  }
452  else if(full_type.id()==ID_struct)
453  {
454  const struct_typet::componentst &components=
455  to_struct_type(full_type).components();
456 
457  if(index>=dest->operands().size())
458  {
460  error() << "structure member designator " << index
461  << " out of bounds (" << dest->operands().size()
462  << ")" << eom;
463  throw 0;
464  }
465 
466  DATA_INVARIANT(index<components.size(),
467  "member designator is bounded by components size");
468  DATA_INVARIANT(components[index].type().id()!=ID_code &&
469  !components[index].get_is_padding(),
470  "member designator points at data member");
471 
472  dest=&(dest->operands()[index]);
473  }
474  else if(full_type.id()==ID_union)
475  {
476  const union_typet &union_type=to_union_type(full_type);
477 
478  const union_typet::componentst &components=
479  union_type.components();
480 
481  DATA_INVARIANT(index<components.size(),
482  "member designator is bounded by components size");
483 
484  const union_typet::componentt &component=union_type.components()[index];
485 
486  if(dest->id()==ID_union &&
487  dest->get(ID_component_name)==component.get_name())
488  {
489  // Already right union component. We can initialize multiple submembers,
490  // so do not overwrite this.
491  }
492  else
493  {
494  // Note that gcc issues a warning if the union component is switched.
495  // Build a union expression from given component.
496  const auto zero =
497  zero_initializer(component.type(), value.source_location(), *this);
498  if(!zero.has_value())
499  {
501  error() << "cannot zero-initialize union component of type '"
502  << to_string(component.type()) << "'" << eom;
503  throw 0;
504  }
505  union_exprt union_expr(component.get_name(), *zero, type);
506  union_expr.add_source_location()=value.source_location();
507  *dest=union_expr;
508  }
509 
510  dest = &(to_union_expr(*dest).op());
511  }
512  else
513  UNREACHABLE;
514  }
515 
516  // second phase: assign value
517  // for this, we may need to go down, adding to the designator
518 
519  while(true)
520  {
521  // see what type we have to initialize
522 
523  const typet &type=designator.back().subtype;
524  const typet &full_type=follow(type);
525 
526  // do we initialize a scalar?
527  if(full_type.id()!=ID_struct &&
528  full_type.id()!=ID_union &&
529  full_type.id()!=ID_array &&
530  full_type.id()!=ID_vector)
531  {
532  // The initializer for a scalar shall be a single expression,
533  // * optionally enclosed in braces. *
534 
535  if(value.id()==ID_initializer_list &&
536  value.operands().size()==1)
537  {
538  *dest =
539  do_initializer_rec(to_unary_expr(value).op(), type, force_constant);
540  }
541  else
542  *dest=do_initializer_rec(value, type, force_constant);
543 
544  assert(full_type==follow(dest->type()));
545 
546  return ++init_it; // done
547  }
548 
549  // union? The component in the zero initializer might
550  // not be the first one.
551  if(full_type.id()==ID_union)
552  {
553  const union_typet &union_type=to_union_type(full_type);
554 
555  const union_typet::componentst &components=
556  union_type.components();
557 
558  if(!components.empty())
559  {
561  union_type.components().front();
562 
563  const auto zero =
564  zero_initializer(component.type(), value.source_location(), *this);
565  if(!zero.has_value())
566  {
568  error() << "cannot zero-initialize union component of type '"
569  << to_string(component.type()) << "'" << eom;
570  throw 0;
571  }
572  union_exprt union_expr(component.get_name(), *zero, type);
573  union_expr.add_source_location()=value.source_location();
574  *dest=union_expr;
575  }
576  }
577 
578  // see what initializer we are given
579  if(value.id()==ID_initializer_list)
580  {
581  *dest=do_initializer_rec(value, type, force_constant);
582  return ++init_it; // done
583  }
584  else if(value.id()==ID_string_constant)
585  {
586  // We stop for initializers that are string-constants,
587  // which are like arrays. We only do so if we are to
588  // initialize an array of scalars.
589  if(
590  full_type.id() == ID_array &&
591  (full_type.subtype().id() == ID_signedbv ||
592  full_type.subtype().id() == ID_unsignedbv))
593  {
594  *dest=do_initializer_rec(value, type, force_constant);
595  return ++init_it; // done
596  }
597  }
598  else if(follow(value.type())==full_type)
599  {
600  // a struct/union/vector can be initialized directly with
601  // an expression of the right type. This doesn't
602  // work with arrays, unfortunately.
603  if(full_type.id()==ID_struct ||
604  full_type.id()==ID_union ||
605  full_type.id()==ID_vector)
606  {
607  *dest=value;
608  return ++init_it; // done
609  }
610  }
611 
612  assert(full_type.id()==ID_struct ||
613  full_type.id()==ID_union ||
614  full_type.id()==ID_array ||
615  full_type.id()==ID_vector);
616 
617  // we are initializing a compound type, and enter it!
618  // this may change the type, full_type might not be valid any more
619  const typet dest_type=full_type;
620  const bool vla_permitted=designator.back().vla_permitted;
621  designator_enter(type, designator);
622 
623  // GCC permits (though issuing a warning with -Wall) composite
624  // types built from flat initializer lists
625  if(dest->operands().empty())
626  {
628  warning() << "initialisation of " << dest_type.id()
629  << " requires initializer list, found " << value.id()
630  << " instead" << eom;
631 
632  // in case of a variable-length array consume all remaining
633  // initializer elements
634  if(vla_permitted &&
635  dest_type.id()==ID_array &&
636  (to_array_type(dest_type).size().is_zero() ||
637  to_array_type(dest_type).size().is_nil()))
638  {
639  value.id(ID_initializer_list);
640  value.operands().clear();
641  for( ; init_it!=initializer_list.operands().end(); ++init_it)
642  value.copy_to_operands(*init_it);
643  *dest=do_initializer_rec(value, dest_type, force_constant);
644 
645  return init_it;
646  }
647  else
648  {
650  error() << "cannot initialize type '" << to_string(dest_type)
651  << "' using value '" << to_string(value) << "'" << eom;
652  throw 0;
653  }
654  }
655 
656  dest = &(to_multi_ary_expr(*dest).op0());
657 
658  // we run into another loop iteration
659  }
660 
661  return ++init_it;
662 }
663 
665 {
666  assert(!designator.empty());
667 
668  while(true)
669  {
670  designatort::entryt &entry=designator[designator.size()-1];
671  const typet &full_type=follow(entry.type);
672 
673  entry.index++;
674 
675  if(full_type.id()==ID_array &&
676  to_array_type(full_type).size().is_nil())
677  return; // we will keep going forever
678 
679  if(full_type.id()==ID_struct &&
680  entry.index<entry.size)
681  {
682  // need to adjust subtype
683  const struct_typet &struct_type=
684  to_struct_type(full_type);
685  const struct_typet::componentst &components=
686  struct_type.components();
687  assert(components.size()==entry.size);
688 
689  // we skip over any padding or code
690  // we also skip over anonymous members
691  while(entry.index < entry.size &&
692  (components[entry.index].get_is_padding() ||
693  (components[entry.index].get_anonymous() &&
694  components[entry.index].type().id() != ID_struct_tag &&
695  components[entry.index].type().id() != ID_union_tag) ||
696  components[entry.index].type().id() == ID_code))
697  {
698  entry.index++;
699  }
700 
701  if(entry.index<entry.size)
702  entry.subtype=components[entry.index].type();
703  }
704 
705  if(entry.index<entry.size)
706  return; // done
707 
708  if(designator.size()==1)
709  return; // done
710 
711  // pop entry
712  designator.pop_entry();
713 
714  assert(!designator.empty());
715  }
716 }
717 
719  const typet &src_type,
720  const exprt &src)
721 {
722  assert(!src.operands().empty());
723 
724  typet type=src_type;
725  designatort designator;
726 
727  forall_operands(it, src)
728  {
729  const exprt &d_op=*it;
730  designatort::entryt entry(type);
731  const typet &full_type=follow(entry.type);
732 
733  if(full_type.id()==ID_array)
734  {
735  if(d_op.id()!=ID_index)
736  {
738  error() << "expected array index designator" << eom;
739  throw 0;
740  }
741 
742  exprt tmp_index = to_unary_expr(d_op).op();
743  make_constant_index(tmp_index);
744 
745  mp_integer index, size;
746 
747  if(to_integer(to_constant_expr(tmp_index), index))
748  {
750  error() << "expected constant array index designator" << eom;
751  throw 0;
752  }
753 
754  if(to_array_type(full_type).size().is_nil())
755  size=0;
756  else if(
757  const auto size_opt =
758  numeric_cast<mp_integer>(to_array_type(full_type).size()))
759  size = *size_opt;
760  else
761  {
763  error() << "expected constant array size" << eom;
764  throw 0;
765  }
766 
767  entry.index = numeric_cast_v<std::size_t>(index);
768  entry.size = numeric_cast_v<std::size_t>(size);
769  entry.subtype=full_type.subtype();
770  }
771  else if(full_type.id()==ID_struct ||
772  full_type.id()==ID_union)
773  {
774  const struct_union_typet &struct_union_type=
775  to_struct_union_type(full_type);
776 
777  if(d_op.id()!=ID_member)
778  {
780  error() << "expected member designator" << eom;
781  throw 0;
782  }
783 
784  const irep_idt &component_name=d_op.get(ID_component_name);
785 
786  if(struct_union_type.has_component(component_name))
787  {
788  // a direct member
789  entry.index=struct_union_type.component_number(component_name);
790  entry.size=struct_union_type.components().size();
791  entry.subtype=struct_union_type.components()[entry.index].type();
792  }
793  else
794  {
795  // We will search for anonymous members,
796  // in a loop. This isn't supported by gcc, but icc does allow it.
797 
798  bool found=false, repeat;
799  typet tmp_type=entry.type;
800 
801  do
802  {
803  repeat=false;
804  std::size_t number = 0;
805  const struct_union_typet::componentst &components=
807 
808  for(const auto &c : components)
809  {
810  if(c.get_name() == component_name)
811  {
812  // done!
813  entry.index=number;
814  entry.size=components.size();
815  entry.subtype = c.type();
816  entry.type=tmp_type;
817  }
818  else if(
819  c.get_anonymous() &&
820  (c.type().id() == ID_struct_tag ||
821  c.type().id() == ID_union_tag) &&
822  has_component_rec(c.type(), component_name, *this))
823  {
824  entry.index=number;
825  entry.size=components.size();
826  entry.subtype = c.type();
827  entry.type=tmp_type;
828  tmp_type=entry.subtype;
829  designator.push_entry(entry);
830  found=repeat=true;
831  break;
832  }
833 
834  ++number;
835  }
836  }
837  while(repeat);
838 
839  if(!found)
840  {
842  error() << "failed to find struct component '" << component_name
843  << "' in initialization of '" << to_string(struct_union_type)
844  << "'" << eom;
845  throw 0;
846  }
847  }
848  }
849  else
850  {
852  error() << "designated initializers cannot initialize '"
853  << to_string(full_type) << "'" << eom;
854  throw 0;
855  }
856 
857  type=entry.subtype;
858  designator.push_entry(entry);
859  }
860 
861  assert(!designator.empty());
862 
863  return designator;
864 }
865 
867  const exprt &value,
868  const typet &type,
869  bool force_constant)
870 {
871  assert(value.id()==ID_initializer_list);
872 
873  const typet &full_type=follow(type);
874 
875  exprt result;
876  if(full_type.id()==ID_struct ||
877  full_type.id()==ID_union ||
878  full_type.id()==ID_vector)
879  {
880  // start with zero everywhere
881  const auto zero = zero_initializer(type, value.source_location(), *this);
882  if(!zero.has_value())
883  {
885  error() << "cannot zero-initialize '" << to_string(full_type) << "'"
886  << eom;
887  throw 0;
888  }
889  result = *zero;
890  }
891  else if(full_type.id()==ID_array)
892  {
893  if(to_array_type(full_type).size().is_nil())
894  {
895  // start with empty array
896  result=exprt(ID_array, full_type);
897  result.add_source_location()=value.source_location();
898  }
899  else
900  {
901  // start with zero everywhere
902  const auto zero = zero_initializer(type, value.source_location(), *this);
903  if(!zero.has_value())
904  {
906  error() << "cannot zero-initialize '" << to_string(full_type) << "'"
907  << eom;
908  throw 0;
909  }
910  result = *zero;
911  }
912 
913  // 6.7.9, 14: An array of character type may be initialized by a character
914  // string literal or UTF-8 string literal, optionally enclosed in braces.
915  if(
916  value.operands().size() >= 1 &&
917  to_multi_ary_expr(value).op0().id() == ID_string_constant &&
918  (full_type.subtype().id() == ID_signedbv ||
919  full_type.subtype().id() == ID_unsignedbv) &&
920  to_bitvector_type(full_type.subtype()).get_width() ==
921  char_type().get_width())
922  {
923  if(value.operands().size()>1)
924  {
926  warning() << "ignoring excess initializers" << eom;
927  }
928 
929  return do_initializer_rec(
930  to_multi_ary_expr(value).op0(), type, force_constant);
931  }
932  }
933  else
934  {
935  // The initializer for a scalar shall be a single expression,
936  // * optionally enclosed in braces. *
937 
938  if(value.operands().size()==1)
939  return do_initializer_rec(
940  to_unary_expr(value).op(), type, force_constant);
941 
943  error() << "cannot initialize '" << to_string(full_type)
944  << "' with an initializer list" << eom;
945  throw 0;
946  }
947 
948  designatort current_designator;
949 
950  designator_enter(type, current_designator);
951 
952  const exprt::operandst &operands=value.operands();
953  for(exprt::operandst::const_iterator it=operands.begin();
954  it!=operands.end(); ) // no ++it
955  {
957  result, current_designator, value, it, force_constant);
958 
959  // increase designator -- might go up
960  increment_designator(current_designator);
961  }
962 
963  // make sure we didn't mess up index computation
964  if(full_type.id()==ID_struct)
965  {
966  assert(result.operands().size()==
967  to_struct_type(full_type).components().size());
968  }
969 
970  if(full_type.id()==ID_array &&
971  to_array_type(full_type).size().is_nil())
972  {
973  // make complete by setting array size
974  size_t size=result.operands().size();
975  result.type().id(ID_array);
976  result.type().set(ID_size, from_integer(size, index_type()));
977  }
978 
979  return result;
980 }
c_typecheck_baset::do_initializer
virtual void do_initializer(exprt &initializer, const typet &type, bool force_constant)
Definition: c_typecheck_initializer.cpp:25
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:150
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:316
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:358
Forall_operands
#define Forall_operands(it, expr)
Definition: expr.h:24
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:1384
irept::make_nil
void make_nil()
Definition: irep.h:475
typet
The type of an expression, extends irept.
Definition: type.h:29
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: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
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:1567
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:1412
string_constant.h
exprt
Base class for all expressions.
Definition: expr.h:53
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:1613
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:192
vector_typet
The vector type.
Definition: std_types.h:1750
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
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:3552
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:866
designatort::pop_entry
void pop_entry()
Definition: designator.h:50
array_typet::size
const exprt & size() const
Definition: std_types.h:973
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
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:402
expr_initializer.h
Expression Initialization.
messaget::result
mstreamt & result() const
Definition: message.h:409
messaget::error
mstreamt & error() const
Definition: message.h:399
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:44
messaget::mstreamt::source_location
source_locationt source_location
Definition: message.h:247
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:18
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:231
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:3573
irept::is_nil
bool is_nil() const
Definition: irep.h:398
irept::id
const irep_idt & id() const
Definition: irep.h:418
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:55
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:281
cprover_prefix.h
vector_typet::size
const constant_exprt & size() const
Definition: std_types.cpp:268
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:266
c_typecheck_baset::typecheck_expr
virtual void typecheck_expr(exprt &expr)
Definition: c_typecheck_expr.cpp:41
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:1041
struct_union_typet::componentt
Definition: std_types.h:64
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:53
array_typet
Arrays with given size.
Definition: std_types.h:965
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:718
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:1011
designatort::entryt::type
typet type
Definition: designator.h:28
symbolt::is_static_lifetime
bool is_static_lifetime
Definition: symbol.h:65
to_vector_type
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition: std_types.h:1775
has_prefix
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
anonymous_member.h
C Language Type Checking.
c_typecheck_baset::increment_designator
void increment_designator(designatort &designator)
Definition: c_typecheck_initializer.cpp:664
exprt::operands
operandst & operands()
Definition: expr.h:95
to_union_type
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition: std_types.h:422
designatort::entryt::subtype
typet subtype
Definition: designator.h:28
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:259
messaget::warning
mstreamt & warning() const
Definition: message.h:404
multi_ary_exprt::op0
exprt & op0()
Definition: std_expr.h:811
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:866
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:254
array_exprt
Array constructor from list of elements.
Definition: std_expr.h:1432
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:1089
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:3939