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