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