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  if(index>=dest->operands().size())
401  {
402  if(full_type.id()==ID_array &&
403  (to_array_type(full_type).size().is_zero() ||
404  to_array_type(full_type).size().is_nil()))
405  {
406  // we are willing to grow an incomplete or zero-sized array
407  const auto zero = zero_initializer(
408  full_type.subtype(), value.source_location(), *this);
409  if(!zero.has_value())
410  {
412  error() << "cannot zero-initialize array with subtype '"
413  << to_string(full_type.subtype()) << "'" << eom;
414  throw 0;
415  }
416  dest->operands().resize(
417  numeric_cast_v<std::size_t>(index) + 1, *zero);
418 
419  // todo: adjust type!
420  }
421  else
422  {
424  error() << "array index designator " << index
425  << " out of bounds (" << dest->operands().size()
426  << ")" << eom;
427  throw 0;
428  }
429  }
430 
431  dest = &(dest->operands()[numeric_cast_v<std::size_t>(index)]);
432  }
433  else if(full_type.id()==ID_struct)
434  {
435  const struct_typet::componentst &components=
436  to_struct_type(full_type).components();
437 
438  if(index>=dest->operands().size())
439  {
441  error() << "structure member designator " << index
442  << " out of bounds (" << dest->operands().size()
443  << ")" << eom;
444  throw 0;
445  }
446 
447  DATA_INVARIANT(index<components.size(),
448  "member designator is bounded by components size");
449  DATA_INVARIANT(components[index].type().id()!=ID_code &&
450  !components[index].get_is_padding(),
451  "member designator points at data member");
452 
453  dest=&(dest->operands()[index]);
454  }
455  else if(full_type.id()==ID_union)
456  {
457  const union_typet &union_type=to_union_type(full_type);
458 
459  const union_typet::componentst &components=
460  union_type.components();
461 
462  DATA_INVARIANT(index<components.size(),
463  "member designator is bounded by components size");
464 
465  const union_typet::componentt &component=union_type.components()[index];
466 
467  if(dest->id()==ID_union &&
468  dest->get(ID_component_name)==component.get_name())
469  {
470  // Already right union component. We can initialize multiple submembers,
471  // so do not overwrite this.
472  }
473  else
474  {
475  // Note that gcc issues a warning if the union component is switched.
476  // Build a union expression from given component.
477  const auto zero =
478  zero_initializer(component.type(), value.source_location(), *this);
479  if(!zero.has_value())
480  {
482  error() << "cannot zero-initialize union component of type '"
483  << to_string(component.type()) << "'" << eom;
484  throw 0;
485  }
486  union_exprt union_expr(component.get_name(), *zero, type);
487  union_expr.add_source_location()=value.source_location();
488  *dest=union_expr;
489  }
490 
491  dest = &(to_union_expr(*dest).op());
492  }
493  else
494  UNREACHABLE;
495  }
496 
497  // second phase: assign value
498  // for this, we may need to go down, adding to the designator
499 
500  while(true)
501  {
502  // see what type we have to initialize
503 
504  const typet &type=designator.back().subtype;
505  const typet &full_type=follow(type);
506 
507  // do we initialize a scalar?
508  if(full_type.id()!=ID_struct &&
509  full_type.id()!=ID_union &&
510  full_type.id()!=ID_array &&
511  full_type.id()!=ID_vector)
512  {
513  // The initializer for a scalar shall be a single expression,
514  // * optionally enclosed in braces. *
515 
516  if(value.id()==ID_initializer_list &&
517  value.operands().size()==1)
518  {
519  *dest =
520  do_initializer_rec(to_unary_expr(value).op(), type, force_constant);
521  }
522  else
523  *dest=do_initializer_rec(value, type, force_constant);
524 
525  assert(full_type==follow(dest->type()));
526 
527  return ++init_it; // done
528  }
529 
530  // union? The component in the zero initializer might
531  // not be the first one.
532  if(full_type.id()==ID_union)
533  {
534  const union_typet &union_type=to_union_type(full_type);
535 
536  const union_typet::componentst &components=
537  union_type.components();
538 
539  if(!components.empty())
540  {
542  union_type.components().front();
543 
544  const auto zero =
545  zero_initializer(component.type(), value.source_location(), *this);
546  if(!zero.has_value())
547  {
549  error() << "cannot zero-initialize union component of type '"
550  << to_string(component.type()) << "'" << eom;
551  throw 0;
552  }
553  union_exprt union_expr(component.get_name(), *zero, type);
554  union_expr.add_source_location()=value.source_location();
555  *dest=union_expr;
556  }
557  }
558 
559  // see what initializer we are given
560  if(value.id()==ID_initializer_list)
561  {
562  *dest=do_initializer_rec(value, type, force_constant);
563  return ++init_it; // done
564  }
565  else if(value.id()==ID_string_constant)
566  {
567  // We stop for initializers that are string-constants,
568  // which are like arrays. We only do so if we are to
569  // initialize an array of scalars.
570  if(
571  full_type.id() == ID_array &&
572  (full_type.subtype().id() == ID_signedbv ||
573  full_type.subtype().id() == ID_unsignedbv))
574  {
575  *dest=do_initializer_rec(value, type, force_constant);
576  return ++init_it; // done
577  }
578  }
579  else if(follow(value.type())==full_type)
580  {
581  // a struct/union/vector can be initialized directly with
582  // an expression of the right type. This doesn't
583  // work with arrays, unfortunately.
584  if(full_type.id()==ID_struct ||
585  full_type.id()==ID_union ||
586  full_type.id()==ID_vector)
587  {
588  *dest=value;
589  return ++init_it; // done
590  }
591  }
592 
593  assert(full_type.id()==ID_struct ||
594  full_type.id()==ID_union ||
595  full_type.id()==ID_array ||
596  full_type.id()==ID_vector);
597 
598  // we are initializing a compound type, and enter it!
599  // this may change the type, full_type might not be valid any more
600  const typet dest_type=full_type;
601  const bool vla_permitted=designator.back().vla_permitted;
602  designator_enter(type, designator);
603 
604  // GCC permits (though issuing a warning with -Wall) composite
605  // types built from flat initializer lists
606  if(dest->operands().empty())
607  {
609  warning() << "initialisation of " << dest_type.id()
610  << " requires initializer list, found " << value.id()
611  << " instead" << eom;
612 
613  // in case of a variable-length array consume all remaining
614  // initializer elements
615  if(vla_permitted &&
616  dest_type.id()==ID_array &&
617  (to_array_type(dest_type).size().is_zero() ||
618  to_array_type(dest_type).size().is_nil()))
619  {
620  value.id(ID_initializer_list);
621  value.operands().clear();
622  for( ; init_it!=initializer_list.operands().end(); ++init_it)
623  value.copy_to_operands(*init_it);
624  *dest=do_initializer_rec(value, dest_type, force_constant);
625 
626  return init_it;
627  }
628  else
629  {
631  error() << "cannot initialize type '" << to_string(dest_type)
632  << "' using value '" << to_string(value) << "'" << eom;
633  throw 0;
634  }
635  }
636 
637  dest = &(to_multi_ary_expr(*dest).op0());
638 
639  // we run into another loop iteration
640  }
641 
642  return ++init_it;
643 }
644 
646 {
647  assert(!designator.empty());
648 
649  while(true)
650  {
651  designatort::entryt &entry=designator[designator.size()-1];
652  const typet &full_type=follow(entry.type);
653 
654  entry.index++;
655 
656  if(full_type.id()==ID_array &&
657  to_array_type(full_type).size().is_nil())
658  return; // we will keep going forever
659 
660  if(full_type.id()==ID_struct &&
661  entry.index<entry.size)
662  {
663  // need to adjust subtype
664  const struct_typet &struct_type=
665  to_struct_type(full_type);
666  const struct_typet::componentst &components=
667  struct_type.components();
668  assert(components.size()==entry.size);
669 
670  // we skip over any padding or code
671  // we also skip over anonymous members
672  while(entry.index < entry.size &&
673  (components[entry.index].get_is_padding() ||
674  (components[entry.index].get_anonymous() &&
675  components[entry.index].type().id() != ID_struct_tag &&
676  components[entry.index].type().id() != ID_union_tag) ||
677  components[entry.index].type().id() == ID_code))
678  {
679  entry.index++;
680  }
681 
682  if(entry.index<entry.size)
683  entry.subtype=components[entry.index].type();
684  }
685 
686  if(entry.index<entry.size)
687  return; // done
688 
689  if(designator.size()==1)
690  return; // done
691 
692  // pop entry
693  designator.pop_entry();
694 
695  assert(!designator.empty());
696  }
697 }
698 
700  const typet &src_type,
701  const exprt &src)
702 {
703  assert(!src.operands().empty());
704 
705  typet type=src_type;
706  designatort designator;
707 
708  forall_operands(it, src)
709  {
710  const exprt &d_op=*it;
711  designatort::entryt entry(type);
712  const typet &full_type=follow(entry.type);
713 
714  if(full_type.id()==ID_array)
715  {
716  if(d_op.id()!=ID_index)
717  {
719  error() << "expected array index designator" << eom;
720  throw 0;
721  }
722 
723  exprt tmp_index = to_unary_expr(d_op).op();
724  make_constant_index(tmp_index);
725 
726  mp_integer index, size;
727 
728  if(to_integer(to_constant_expr(tmp_index), index))
729  {
731  error() << "expected constant array index designator" << eom;
732  throw 0;
733  }
734 
735  if(to_array_type(full_type).size().is_nil())
736  size=0;
737  else if(
738  const auto size_opt =
739  numeric_cast<mp_integer>(to_array_type(full_type).size()))
740  size = *size_opt;
741  else
742  {
744  error() << "expected constant array size" << eom;
745  throw 0;
746  }
747 
748  entry.index = numeric_cast_v<std::size_t>(index);
749  entry.size = numeric_cast_v<std::size_t>(size);
750  entry.subtype=full_type.subtype();
751  }
752  else if(full_type.id()==ID_struct ||
753  full_type.id()==ID_union)
754  {
755  const struct_union_typet &struct_union_type=
756  to_struct_union_type(full_type);
757 
758  if(d_op.id()!=ID_member)
759  {
761  error() << "expected member designator" << eom;
762  throw 0;
763  }
764 
765  const irep_idt &component_name=d_op.get(ID_component_name);
766 
767  if(struct_union_type.has_component(component_name))
768  {
769  // a direct member
770  entry.index=struct_union_type.component_number(component_name);
771  entry.size=struct_union_type.components().size();
772  entry.subtype=struct_union_type.components()[entry.index].type();
773  }
774  else
775  {
776  // We will search for anonymous members,
777  // in a loop. This isn't supported by gcc, but icc does allow it.
778 
779  bool found=false, repeat;
780  typet tmp_type=entry.type;
781 
782  do
783  {
784  repeat=false;
785  std::size_t number = 0;
786  const struct_union_typet::componentst &components=
788 
789  for(const auto &c : components)
790  {
791  if(c.get_name() == component_name)
792  {
793  // done!
794  entry.index=number;
795  entry.size=components.size();
796  entry.subtype = c.type();
797  entry.type=tmp_type;
798  }
799  else if(
800  c.get_anonymous() &&
801  (c.type().id() == ID_struct_tag ||
802  c.type().id() == ID_union_tag) &&
803  has_component_rec(c.type(), component_name, *this))
804  {
805  entry.index=number;
806  entry.size=components.size();
807  entry.subtype = c.type();
808  entry.type=tmp_type;
809  tmp_type=entry.subtype;
810  designator.push_entry(entry);
811  found=repeat=true;
812  break;
813  }
814 
815  ++number;
816  }
817  }
818  while(repeat);
819 
820  if(!found)
821  {
823  error() << "failed to find struct component '" << component_name
824  << "' in initialization of '" << to_string(struct_union_type)
825  << "'" << eom;
826  throw 0;
827  }
828  }
829  }
830  else
831  {
833  error() << "designated initializers cannot initialize '"
834  << to_string(full_type) << "'" << eom;
835  throw 0;
836  }
837 
838  type=entry.subtype;
839  designator.push_entry(entry);
840  }
841 
842  assert(!designator.empty());
843 
844  return designator;
845 }
846 
848  const exprt &value,
849  const typet &type,
850  bool force_constant)
851 {
852  assert(value.id()==ID_initializer_list);
853 
854  const typet &full_type=follow(type);
855 
856  exprt result;
857  if(full_type.id()==ID_struct ||
858  full_type.id()==ID_union ||
859  full_type.id()==ID_vector)
860  {
861  // start with zero everywhere
862  const auto zero = zero_initializer(type, value.source_location(), *this);
863  if(!zero.has_value())
864  {
866  error() << "cannot zero-initialize '" << to_string(full_type) << "'"
867  << eom;
868  throw 0;
869  }
870  result = *zero;
871  }
872  else if(full_type.id()==ID_array)
873  {
874  if(to_array_type(full_type).size().is_nil())
875  {
876  // start with empty array
877  result=exprt(ID_array, full_type);
878  result.add_source_location()=value.source_location();
879  }
880  else
881  {
882  // start with zero everywhere
883  const auto zero = zero_initializer(type, value.source_location(), *this);
884  if(!zero.has_value())
885  {
887  error() << "cannot zero-initialize '" << to_string(full_type) << "'"
888  << eom;
889  throw 0;
890  }
891  result = *zero;
892  }
893 
894  // 6.7.9, 14: An array of character type may be initialized by a character
895  // string literal or UTF-8 string literal, optionally enclosed in braces.
896  if(
897  value.operands().size() >= 1 &&
898  to_multi_ary_expr(value).op0().id() == ID_string_constant &&
899  (full_type.subtype().id() == ID_signedbv ||
900  full_type.subtype().id() == ID_unsignedbv) &&
901  to_bitvector_type(full_type.subtype()).get_width() ==
902  char_type().get_width())
903  {
904  if(value.operands().size()>1)
905  {
907  warning() << "ignoring excess initializers" << eom;
908  }
909 
910  return do_initializer_rec(
911  to_multi_ary_expr(value).op0(), type, force_constant);
912  }
913  }
914  else
915  {
916  // The initializer for a scalar shall be a single expression,
917  // * optionally enclosed in braces. *
918 
919  if(value.operands().size()==1)
920  return do_initializer_rec(
921  to_unary_expr(value).op(), type, force_constant);
922 
924  error() << "cannot initialize '" << to_string(full_type)
925  << "' with an initializer list" << eom;
926  throw 0;
927  }
928 
929  designatort current_designator;
930 
931  designator_enter(type, current_designator);
932 
933  const exprt::operandst &operands=value.operands();
934  for(exprt::operandst::const_iterator it=operands.begin();
935  it!=operands.end(); ) // no ++it
936  {
938  result, current_designator, value, it, force_constant);
939 
940  // increase designator -- might go up
941  increment_designator(current_designator);
942  }
943 
944  // make sure we didn't mess up index computation
945  if(full_type.id()==ID_struct)
946  {
947  assert(result.operands().size()==
948  to_struct_type(full_type).components().size());
949  }
950 
951  if(full_type.id()==ID_array &&
952  to_array_type(full_type).size().is_nil())
953  {
954  // make complete by setting array size
955  size_t size=result.operands().size();
956  result.type().id(ID_array);
957  result.type().set(ID_size, from_integer(size, index_type()));
958  }
959 
960  return result;
961 }
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:148
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
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
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:1579
to_string_constant
const string_constantt & to_string_constant(const exprt &expr)
Definition: string_constant.h:31
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:1625
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:283
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:3448
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:847
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
messaget::result
mstreamt & result() const
Definition: message.h:395
messaget::error
mstreamt & error() const
Definition: message.h:385
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:244
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
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:3469
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:39
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:699
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_typecheck_baset::increment_designator
void increment_designator(designatort &designator)
Definition: c_typecheck_initializer.cpp:645
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:257
messaget::warning
mstreamt & warning() const
Definition: message.h:390
multi_ary_exprt::op0
exprt & op0()
Definition: std_expr.h:817
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:872
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:252
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:3968