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  {
63  err_location(value);
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  {
94  err_location(value);
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  {
102  err_location(value);
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(integer2size_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  exprt zero=
119  full_type.subtype(),
120  value.source_location(),
121  *this,
123  tmp.operands().resize(integer2size_t(array_size), zero);
124  }
125  }
126 
127  return tmp;
128  }
129 
130  if(value.id()==ID_string_constant &&
131  full_type.id()==ID_array &&
132  (full_type.subtype().id()==ID_signedbv ||
133  full_type.subtype().id()==ID_unsignedbv) &&
134  full_type.subtype().get(ID_width)==char_type().get(ID_width))
135  {
136  // will go away, to be replaced by the above block
137 
139  // adjust char type
140  tmp1.type().subtype()=full_type.subtype();
141 
142  exprt tmp2=tmp1.to_array_expr();
143 
144  if(full_type.id()==ID_array &&
145  to_array_type(full_type).is_complete())
146  {
147  // check size
148  mp_integer array_size;
149  if(to_integer(to_array_type(full_type).size(), array_size))
150  {
151  err_location(value);
152  error() << "array size needs to be constant, got "
153  << to_string(to_array_type(full_type).size()) << eom;
154  throw 0;
155  }
156 
157  if(array_size<0)
158  {
159  err_location(value);
160  error() << "array size must not be negative" << eom;
161  throw 0;
162  }
163 
164  if(mp_integer(tmp2.operands().size())>array_size)
165  {
166  // cut off long strings. gcc does a warning for this
167  tmp2.operands().resize(integer2size_t(array_size));
168  tmp2.type()=type;
169  }
170  else if(mp_integer(tmp2.operands().size())<array_size)
171  {
172  // fill up
173  tmp2.type()=type;
174  exprt zero=
176  full_type.subtype(),
177  value.source_location(),
178  *this,
180  tmp2.operands().resize(integer2size_t(array_size), zero);
181  }
182  }
183 
184  return tmp2;
185  }
186 
187  if(full_type.id()==ID_array &&
188  to_array_type(full_type).size().is_nil())
189  {
190  err_location(value);
191  error() << "type `" << to_string(full_type)
192  << "' cannot be initialized with `" << to_string(value)
193  << "'" << eom;
194  throw 0;
195  }
196 
197  if(value.id()==ID_designated_initializer)
198  {
199  err_location(value);
200  error() << "type `" << to_string(full_type)
201  << "' cannot be initialized with designated initializer"
202  << eom;
203  throw 0;
204  }
205 
206  exprt result=value;
207  implicit_typecast(result, type);
208  return result;
209 }
210 
212 {
213  // this one doesn't need initialization
214  if(has_prefix(id2string(symbol.name), CPROVER_PREFIX "constant_infinity"))
215  return;
216 
217  if(symbol.is_static_lifetime)
218  {
219  if(symbol.value.is_not_nil())
220  {
221  typecheck_expr(symbol.value);
222  do_initializer(symbol.value, symbol.type, true);
223 
224  // need to adjust size?
225  if(follow(symbol.type).id()==ID_array &&
226  to_array_type(follow(symbol.type)).size().is_nil())
227  symbol.type=symbol.value.type();
228  }
229  }
230  else if(!symbol.is_type)
231  {
232  if(symbol.is_macro)
233  {
234  // these must have a constant value
235  assert(symbol.value.is_not_nil());
236  typecheck_expr(symbol.value);
237  source_locationt location=symbol.value.source_location();
238  do_initializer(symbol.value, symbol.type, true);
239  make_constant(symbol.value);
240  }
241  else if(symbol.value.is_not_nil())
242  {
243  typecheck_expr(symbol.value);
244  do_initializer(symbol.value, symbol.type, true);
245 
246  // need to adjust size?
247  if(follow(symbol.type).id()==ID_array &&
248  to_array_type(follow(symbol.type)).size().is_nil())
249  symbol.type=symbol.value.type();
250  }
251  }
252 }
253 
255  const typet &type,
256  designatort &designator)
257 {
258  designatort::entryt entry(type);
259 
260  const typet &full_type=follow(type);
261 
262  if(full_type.id()==ID_struct)
263  {
264  const struct_typet &struct_type=to_struct_type(full_type);
265 
266  entry.size=struct_type.components().size();
267  entry.subtype.make_nil();
268  // only a top-level struct may end with a variable-length array
269  entry.vla_permitted=designator.empty();
270 
271  for(struct_typet::componentst::const_iterator
272  it=struct_type.components().begin();
273  it!=struct_type.components().end();
274  ++it)
275  {
276  if(it->type().id()!=ID_code &&
277  !it->get_is_padding())
278  {
279  entry.subtype=it->type();
280  break;
281  }
282 
283  ++entry.index;
284  }
285  }
286  else if(full_type.id()==ID_union)
287  {
288  const union_typet &union_type=to_union_type(full_type);
289 
290  if(union_type.components().empty())
291  {
292  entry.size=0;
293  entry.subtype.make_nil();
294  }
295  else
296  {
297  // The default is to initialize using the first member of the
298  // union.
299  entry.size=1;
300  entry.subtype=union_type.components().front().type();
301  }
302  }
303  else if(full_type.id()==ID_array)
304  {
305  const array_typet &array_type=to_array_type(full_type);
306 
307  if(array_type.size().is_nil())
308  {
309  entry.size=0;
310  entry.subtype=array_type.subtype();
311  }
312  else
313  {
314  mp_integer array_size;
315 
316  if(to_integer(array_type.size(), array_size))
317  {
318  err_location(array_type.size());
319  error() << "array has non-constant size `"
320  << to_string(array_type.size()) << "'" << eom;
321  throw 0;
322  }
323 
324  entry.size=integer2size_t(array_size);
325  entry.subtype=array_type.subtype();
326  }
327  }
328  else if(full_type.id()==ID_vector)
329  {
330  const vector_typet &vector_type=to_vector_type(full_type);
331 
332  mp_integer vector_size;
333 
334  if(to_integer(vector_type.size(), vector_size))
335  {
336  err_location(vector_type.size());
337  error() << "vector has non-constant size `"
338  << to_string(vector_type.size()) << "'" << eom;
339  throw 0;
340  }
341 
342  entry.size=integer2size_t(vector_size);
343  entry.subtype=vector_type.subtype();
344  }
345  else
346  UNREACHABLE;
347 
348  designator.push_entry(entry);
349 }
350 
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  exprt zero=
404  full_type.subtype(),
405  value.source_location(),
406  *this,
408  dest->operands().resize(integer2size_t(index)+1, zero);
409 
410  // todo: adjust type!
411  }
412  else
413  {
414  err_location(value);
415  error() << "array index designator " << index
416  << " out of bounds (" << dest->operands().size()
417  << ")" << eom;
418  throw 0;
419  }
420  }
421 
422  dest=&(dest->operands()[integer2size_t(index)]);
423  }
424  else if(full_type.id()==ID_struct)
425  {
426  const struct_typet::componentst &components=
427  to_struct_type(full_type).components();
428 
429  if(index>=dest->operands().size())
430  {
431  err_location(value);
432  error() << "structure member designator " << index
433  << " out of bounds (" << dest->operands().size()
434  << ")" << eom;
435  throw 0;
436  }
437 
438  DATA_INVARIANT(index<components.size(),
439  "member designator is bounded by components size");
440  DATA_INVARIANT(components[index].type().id()!=ID_code &&
441  !components[index].get_is_padding(),
442  "member designator points at data member");
443 
444  dest=&(dest->operands()[index]);
445  }
446  else if(full_type.id()==ID_union)
447  {
448  const union_typet &union_type=to_union_type(full_type);
449 
450  const union_typet::componentst &components=
451  union_type.components();
452 
453  DATA_INVARIANT(index<components.size(),
454  "member designator is bounded by components size");
455 
456  const union_typet::componentt &component=union_type.components()[index];
457 
458  if(dest->id()==ID_union &&
459  dest->get(ID_component_name)==component.get_name())
460  {
461  // Already right union component. We can initialize multiple submembers,
462  // so do not overwrite this.
463  }
464  else
465  {
466  // Note that gcc issues a warning if the union component is switched.
467  // Build a union expression from given component.
468  union_exprt union_expr(type);
469  union_expr.op()=
471  component.type(),
472  value.source_location(),
473  *this,
475  union_expr.add_source_location()=value.source_location();
476  union_expr.set_component_name(component.get_name());
477  *dest=union_expr;
478  }
479 
480  dest=&(dest->op0());
481  }
482  else
483  UNREACHABLE;
484  }
485 
486  // second phase: assign value
487  // for this, we may need to go down, adding to the designator
488 
489  while(true)
490  {
491  // see what type we have to initialize
492 
493  const typet &type=designator.back().subtype;
494  const typet &full_type=follow(type);
495  assert(full_type.id()!=ID_symbol);
496 
497  // do we initialize a scalar?
498  if(full_type.id()!=ID_struct &&
499  full_type.id()!=ID_union &&
500  full_type.id()!=ID_array &&
501  full_type.id()!=ID_vector)
502  {
503  // The initializer for a scalar shall be a single expression,
504  // * optionally enclosed in braces. *
505 
506  if(value.id()==ID_initializer_list &&
507  value.operands().size()==1)
508  *dest=do_initializer_rec(value.op0(), type, force_constant);
509  else
510  *dest=do_initializer_rec(value, type, force_constant);
511 
512  assert(full_type==follow(dest->type()));
513 
514  return ++init_it; // done
515  }
516 
517  // union? The component in the zero initializer might
518  // not be the first one.
519  if(full_type.id()==ID_union)
520  {
521  const union_typet &union_type=to_union_type(full_type);
522 
523  const union_typet::componentst &components=
524  union_type.components();
525 
526  if(!components.empty())
527  {
528  const union_typet::componentt &component=
529  union_type.components().front();
530 
531  union_exprt union_expr(type);
532  union_expr.op()=
534  component.type(),
535  value.source_location(),
536  *this,
538  union_expr.add_source_location()=value.source_location();
539  union_expr.set_component_name(component.get_name());
540  *dest=union_expr;
541  }
542  }
543 
544  // see what initializer we are given
545  if(value.id()==ID_initializer_list)
546  {
547  *dest=do_initializer_rec(value, type, force_constant);
548  return ++init_it; // done
549  }
550  else if(value.id()==ID_string_constant)
551  {
552  // We stop for initializers that are string-constants,
553  // which are like arrays. We only do so if we are to
554  // initialize an array of scalars.
555  if(full_type.id()==ID_array &&
556  (follow(full_type.subtype()).id()==ID_signedbv ||
557  follow(full_type.subtype()).id()==ID_unsignedbv))
558  {
559  *dest=do_initializer_rec(value, type, force_constant);
560  return ++init_it; // done
561  }
562  }
563  else if(follow(value.type())==full_type)
564  {
565  // a struct/union/vector can be initialized directly with
566  // an expression of the right type. This doesn't
567  // work with arrays, unfortunately.
568  if(full_type.id()==ID_struct ||
569  full_type.id()==ID_union ||
570  full_type.id()==ID_vector)
571  {
572  *dest=value;
573  return ++init_it; // done
574  }
575  }
576 
577  assert(full_type.id()==ID_struct ||
578  full_type.id()==ID_union ||
579  full_type.id()==ID_array ||
580  full_type.id()==ID_vector);
581 
582  // we are initializing a compound type, and enter it!
583  // this may change the type, full_type might not be valid any more
584  const typet dest_type=full_type;
585  const bool vla_permitted=designator.back().vla_permitted;
586  designator_enter(type, designator);
587 
588  // GCC permits (though issuing a warning with -Wall) composite
589  // types built from flat initializer lists
590  if(dest->operands().empty())
591  {
593  warning() << "initialisation of " << dest_type.id()
594  << " requires initializer list, found " << value.id()
595  << " instead" << eom;
596 
597  // in case of a variable-length array consume all remaining
598  // initializer elements
599  if(vla_permitted &&
600  dest_type.id()==ID_array &&
601  (to_array_type(dest_type).size().is_zero() ||
602  to_array_type(dest_type).size().is_nil()))
603  {
604  value.id(ID_initializer_list);
605  value.operands().clear();
606  for( ; init_it!=initializer_list.operands().end(); ++init_it)
607  value.copy_to_operands(*init_it);
608  *dest=do_initializer_rec(value, dest_type, force_constant);
609 
610  return init_it;
611  }
612  else
613  {
614  err_location(value);
615  error() << "cannot initialize type `"
616  << to_string(dest_type) << "' using value `"
617  << to_string(value) << "'" << eom;
618  throw 0;
619  }
620  }
621 
622  dest=&(dest->op0());
623 
624  // we run into another loop iteration
625  }
626 
627  return ++init_it;
628 }
629 
631 {
632  assert(!designator.empty());
633 
634  while(true)
635  {
636  designatort::entryt &entry=designator[designator.size()-1];
637  const typet &full_type=follow(entry.type);
638 
639  entry.index++;
640 
641  if(full_type.id()==ID_array &&
642  to_array_type(full_type).size().is_nil())
643  return; // we will keep going forever
644 
645  if(full_type.id()==ID_struct &&
646  entry.index<entry.size)
647  {
648  // need to adjust subtype
649  const struct_typet &struct_type=
650  to_struct_type(full_type);
651  const struct_typet::componentst &components=
652  struct_type.components();
653  assert(components.size()==entry.size);
654 
655  // we skip over any padding or code
656  while(entry.index<entry.size &&
657  (components[entry.index].get_is_padding() ||
658  components[entry.index].type().id()==ID_code))
659  entry.index++;
660 
661  if(entry.index<entry.size)
662  entry.subtype=components[entry.index].type();
663  }
664 
665  if(entry.index<entry.size)
666  return; // done
667 
668  if(designator.size()==1)
669  return; // done
670 
671  // pop entry
672  designator.pop_entry();
673 
674  assert(!designator.empty());
675  }
676 }
677 
679  const typet &src_type,
680  const exprt &src)
681 {
682  assert(!src.operands().empty());
683 
684  typet type=src_type;
685  designatort designator;
686 
687  forall_operands(it, src)
688  {
689  const exprt &d_op=*it;
690  designatort::entryt entry(type);
691  const typet &full_type=follow(entry.type);
692 
693  if(full_type.id()==ID_array)
694  {
695  if(d_op.id()!=ID_index)
696  {
697  err_location(d_op);
698  error() << "expected array index designator" << eom;
699  throw 0;
700  }
701 
702  assert(d_op.operands().size()==1);
703  exprt tmp_index=d_op.op0();
704  make_constant_index(tmp_index);
705 
706  mp_integer index, size;
707 
708  if(to_integer(tmp_index, index))
709  {
710  err_location(d_op.op0());
711  error() << "expected constant array index designator" << eom;
712  throw 0;
713  }
714 
715  if(to_array_type(full_type).size().is_nil())
716  size=0;
717  else if(to_integer(to_array_type(full_type).size(), size))
718  {
719  err_location(d_op.op0());
720  error() << "expected constant array size" << eom;
721  throw 0;
722  }
723 
724  entry.index=integer2size_t(index);
725  entry.size=integer2size_t(size);
726  entry.subtype=full_type.subtype();
727  }
728  else if(full_type.id()==ID_struct ||
729  full_type.id()==ID_union)
730  {
731  const struct_union_typet &struct_union_type=
732  to_struct_union_type(full_type);
733 
734  if(d_op.id()!=ID_member)
735  {
736  err_location(d_op);
737  error() << "expected member designator" << eom;
738  throw 0;
739  }
740 
741  const irep_idt &component_name=d_op.get(ID_component_name);
742 
743  if(struct_union_type.has_component(component_name))
744  {
745  // a direct member
746  entry.index=struct_union_type.component_number(component_name);
747  entry.size=struct_union_type.components().size();
748  entry.subtype=struct_union_type.components()[entry.index].type();
749  }
750  else
751  {
752  // We will search for anonymous members,
753  // in a loop. This isn't supported by gcc, but icc does allow it.
754 
755  bool found=false, repeat;
756  typet tmp_type=entry.type;
757 
758  do
759  {
760  repeat=false;
761  unsigned number=0;
762  const struct_union_typet::componentst &components=
764 
765  for(struct_union_typet::componentst::const_iterator
766  c_it=components.begin();
767  c_it!=components.end();
768  c_it++, number++)
769  {
770  if(c_it->get_name()==component_name)
771  {
772  // done!
773  entry.index=number;
774  entry.size=components.size();
775  entry.subtype=components[entry.index].type();
776  entry.type=tmp_type;
777  }
778  else if(c_it->get_anonymous() &&
779  (follow(c_it->type()).id()==ID_struct ||
780  follow(c_it->type()).id()==ID_union) &&
782  c_it->type(), component_name, *this))
783  {
784  entry.index=number;
785  entry.size=components.size();
786  entry.subtype=c_it->type();
787  entry.type=tmp_type;
788  tmp_type=entry.subtype;
789  designator.push_entry(entry);
790  found=repeat=true;
791  break;
792  }
793  }
794  }
795  while(repeat);
796 
797  if(!found)
798  {
799  err_location(d_op);
800  error() << "failed to find struct component `"
801  << component_name << "' in initialization of `"
802  << to_string(struct_union_type) << "'" << eom;
803  throw 0;
804  }
805  }
806  }
807  else
808  {
809  err_location(d_op);
810  error() << "designated initializers cannot initialize `"
811  << to_string(full_type) << "'" << eom;
812  throw 0;
813  }
814 
815  type=entry.subtype;
816  designator.push_entry(entry);
817  }
818 
819  assert(!designator.empty());
820 
821  return designator;
822 }
823 
825  const exprt &value,
826  const typet &type,
827  bool force_constant)
828 {
829  assert(value.id()==ID_initializer_list);
830 
831  const typet &full_type=follow(type);
832 
833  exprt result;
834  if(full_type.id()==ID_struct ||
835  full_type.id()==ID_union ||
836  full_type.id()==ID_vector)
837  {
838  // start with zero everywhere
839  result=
841  type, value.source_location(), *this, get_message_handler());
842  }
843  else if(full_type.id()==ID_array)
844  {
845  if(to_array_type(full_type).size().is_nil())
846  {
847  // start with empty array
848  result=exprt(ID_array, full_type);
849  result.add_source_location()=value.source_location();
850  }
851  else
852  {
853  // start with zero everywhere
854  result=
856  type, value.source_location(), *this, get_message_handler());
857  }
858 
859  // 6.7.9, 14: An array of character type may be initialized by a character
860  // string literal or UTF-8 string literal, optionally enclosed in braces.
861  if(value.operands().size()>=1 &&
862  value.op0().id()==ID_string_constant &&
863  (full_type.subtype().id()==ID_signedbv ||
864  full_type.subtype().id()==ID_unsignedbv) &&
865  full_type.subtype().get(ID_width)==char_type().get(ID_width))
866  {
867  if(value.operands().size()>1)
868  {
870  warning() << "ignoring excess initializers" << eom;
871  }
872 
873  return do_initializer_rec(value.op0(), type, force_constant);
874  }
875  }
876  else
877  {
878  // The initializer for a scalar shall be a single expression,
879  // * optionally enclosed in braces. *
880 
881  if(value.operands().size()==1)
882  return do_initializer_rec(value.op0(), type, force_constant);
883 
884  err_location(value);
885  error() << "cannot initialize `" << to_string(full_type)
886  << "' with an initializer list" << eom;
887  throw 0;
888  }
889 
890  designatort current_designator;
891 
892  designator_enter(type, current_designator);
893 
894  const exprt::operandst &operands=value.operands();
895  for(exprt::operandst::const_iterator it=operands.begin();
896  it!=operands.end(); ) // no ++it
897  {
899  result, current_designator, value, it, force_constant);
900 
901  // increase designator -- might go up
902  increment_designator(current_designator);
903  }
904 
905  // make sure we didn't mess up index computation
906  if(full_type.id()==ID_struct)
907  {
908  assert(result.operands().size()==
909  to_struct_type(full_type).components().size());
910  }
911 
912  if(full_type.id()==ID_array &&
913  to_array_type(full_type).size().is_nil())
914  {
915  // make complete by setting array size
916  size_t size=result.operands().size();
917  result.type().id(ID_array);
918  result.type().set(ID_size, from_integer(size, index_type()));
919  }
920 
921  return result;
922 }
const irep_idt & get_name() const
Definition: std_types.h:182
The type of an expression.
Definition: type.h:22
irep_idt name
The unique identifier.
Definition: symbol.h:43
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:72
#define CPROVER_PREFIX
bool empty() const
Definition: designator.h:36
virtual void make_constant(exprt &expr)
const exprt & op() const
Definition: std_expr.h:340
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:55
std::vector< componentt > componentst
Definition: std_types.h:243
void push_entry(const entryt &entry)
Definition: designator.h:45
exprt value
Initial value of symbol.
Definition: symbol.h:37
const componentst & components() const
Definition: std_types.h:245
void pop_entry()
Definition: designator.h:50
bool has_component_rec(const typet &type, const irep_idt &component_name, const namespacet &ns)
typet & type()
Definition: expr.h:56
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
Structure type.
Definition: std_types.h:297
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:240
virtual std::string to_string(const exprt &expr)
bool is_static_lifetime
Definition: symbol.h:67
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:307
Expression Initialization.
const irep_idt & id() const
Definition: irep.h:259
ANSI-C Language Type Checking.
const entryt & back() const
Definition: designator.h:40
const source_locationt & find_source_location() const
Definition: expr.cpp:246
source_locationt source_location
Definition: message.h:214
A constant-size array type.
Definition: std_types.h:1638
union constructor from single element
Definition: std_expr.h:1730
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
mstreamt & error() const
Definition: message.h:302
void increment_designator(designatort &designator)
const exprt & size() const
Definition: std_types.h:1648
const vector_typet & to_vector_type(const typet &type)
Cast a generic typet to a vector_typet.
Definition: std_types.h:1669
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
const exprt & size() const
Definition: std_types.h:1023
virtual void typecheck_expr(exprt &expr)
#define forall_operands(it, expr)
Definition: expr.h:17
void err_location(const source_locationt &loc)
Definition: typecheck.h:27
array_exprt to_array_expr() const
convert string into array constant
const typet & follow(const typet &) const
Definition: namespace.cpp:55
bitvector_typet index_type()
Definition: c_types.cpp:16
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Definition: std_types.h:318
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
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:255
exprt zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns, message_handlert &message_handler)
std::vector< exprt > operandst
Definition: expr.h:45
virtual void implicit_typecast(exprt &expr, const typet &type)
typet type
Type of symbol.
Definition: symbol.h:34
API to type classes.
message_handlert & get_message_handler()
Definition: message.h:153
Base type of C structs and unions, and C++ classes.
Definition: std_types.h:162
mstreamt & result() const
Definition: message.h:312
const string_constantt & to_string_constant(const exprt &expr)
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Definition: std_types.h:1054
Base class for all expressions.
Definition: expr.h:42
size_t size() const
Definition: designator.h:37
The union type.
Definition: std_types.h:458
std::size_t component_number(const irep_idt &component_name) const
Definition: std_types.cpp:29
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a generic typet to a struct_union_typet.
Definition: std_types.h:280
const union_typet & to_union_type(const typet &type)
Cast a generic typet to a union_typet.
Definition: std_types.h:476
const source_locationt & source_location() const
Definition: expr.h:125
#define UNREACHABLE
Definition: invariant.h:271
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:1033
#define Forall_operands(it, expr)
Definition: expr.h:23
void set_component_name(const irep_idt &component_name)
Definition: std_expr.h:1756
bool is_zero() const
Definition: expr.cpp:161
source_locationt & add_source_location()
Definition: expr.h:130
arrays with given size
Definition: std_types.h:1013
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:17
virtual void do_initializer(exprt &initializer, const typet &type, bool force_constant)
std::size_t integer2size_t(const mp_integer &n)
Definition: mp_arith.cpp:195
bool is_type
Definition: symbol.h:63
const typet & subtype() const
Definition: type.h:33
#define DATA_INVARIANT(CONDITION, REASON)
Definition: invariant.h:278
operandst & operands()
Definition: expr.h:66
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
const irept & find(const irep_namet &name) const
Definition: irep.cpp:285
bitvector_typet char_type()
Definition: c_types.cpp:114
bool is_macro
Definition: symbol.h:63
C Language Type Checking.