cprover
c_typecheck_type.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: C++ Language Type Checking
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "c_typecheck_base.h"
13 
14 #include <unordered_set>
15 
16 #include <util/arith_tools.h>
17 #include <util/c_types.h>
18 #include <util/config.h>
20 #include <util/simplify_expr.h>
21 
22 #include "ansi_c_convert_type.h"
23 #include "c_qualifiers.h"
24 #include "gcc_types.h"
25 #include "padding.h"
26 #include "type2name.h"
27 #include "typedef_type.h"
28 
30 {
31  // we first convert, and then check
32  {
33  ansi_c_convert_typet ansi_c_convert_type(get_message_handler());
34 
35  ansi_c_convert_type.read(type);
36  ansi_c_convert_type.write(type);
37  }
38 
39  if(type.id()==ID_already_typechecked)
40  {
41  // need to preserve any qualifiers
42  c_qualifierst c_qualifiers(type);
43  c_qualifiers+=c_qualifierst(type.subtype());
44  bool packed=type.get_bool(ID_C_packed);
45  exprt alignment=static_cast<const exprt &>(type.find(ID_C_alignment));
46  irept _typedef=type.find(ID_C_typedef);
47 
48  type=type.subtype();
49 
50  c_qualifiers.write(type);
51  if(packed)
52  type.set(ID_C_packed, true);
53  if(alignment.is_not_nil())
54  type.add(ID_C_alignment, alignment);
55  if(_typedef.is_not_nil())
56  type.add(ID_C_typedef, _typedef);
57 
58  return; // done
59  }
60 
61  // do we have alignment?
62  if(type.find(ID_C_alignment).is_not_nil())
63  {
64  exprt &alignment=static_cast<exprt &>(type.add(ID_C_alignment));
65  if(alignment.id()!=ID_default)
66  {
69  }
70  }
71 
72  if(type.id()==ID_code)
74  else if(type.id()==ID_array)
76  else if(type.id()==ID_pointer)
77  {
78  typecheck_type(type.subtype());
79  INVARIANT(!type.get(ID_width).empty(), "pointers must have width");
80  }
81  else if(type.id()==ID_struct ||
82  type.id()==ID_union)
84  else if(type.id()==ID_c_enum)
86  else if(type.id()==ID_c_enum_tag)
88  else if(type.id()==ID_c_bit_field)
90  else if(type.id()==ID_typeof)
92  else if(type.id() == ID_typedef_type)
94  else if(type.id() == ID_struct_tag ||
95  type.id() == ID_union_tag)
96  {
97  // nothing to do, these stay as is
98  }
99  else if(type.id()==ID_vector)
101  else if(type.id()==ID_custom_unsignedbv ||
102  type.id()==ID_custom_signedbv ||
103  type.id()==ID_custom_floatbv ||
104  type.id()==ID_custom_fixedbv)
105  typecheck_custom_type(type);
106  else if(type.id()==ID_gcc_attribute_mode)
107  {
108  // get that mode
109  const irep_idt gcc_attr_mode = type.get(ID_size);
110 
111  // A list of all modes is at
112  // http://www.delorie.com/gnu/docs/gcc/gccint_53.html
113  typecheck_type(type.subtype());
114 
115  typet underlying_type=type.subtype();
116 
117  // gcc allows this, but clang doesn't; it's a compiler hint only,
118  // but we'll try to interpret it the GCC way
119  if(underlying_type.id()==ID_c_enum_tag)
120  {
121  underlying_type=
122  follow_tag(to_c_enum_tag_type(underlying_type)).subtype();
123 
124  assert(underlying_type.id()==ID_signedbv ||
125  underlying_type.id()==ID_unsignedbv);
126  }
127 
128  if(underlying_type.id()==ID_signedbv ||
129  underlying_type.id()==ID_unsignedbv)
130  {
131  bool is_signed=underlying_type.id()==ID_signedbv;
132 
133  typet result;
134 
135  if(gcc_attr_mode == "__QI__") // 8 bits
136  {
137  if(is_signed)
139  else
141  }
142  else if(gcc_attr_mode == "__byte__") // 8 bits
143  {
144  if(is_signed)
146  else
148  }
149  else if(gcc_attr_mode == "__HI__") // 16 bits
150  {
151  if(is_signed)
153  else
155  }
156  else if(gcc_attr_mode == "__SI__") // 32 bits
157  {
158  if(is_signed)
160  else
162  }
163  else if(gcc_attr_mode == "__word__") // long int, we think
164  {
165  if(is_signed)
167  else
169  }
170  else if(gcc_attr_mode == "__pointer__") // size_t/ssize_t, we think
171  {
172  if(is_signed)
174  else
175  result=size_type();
176  }
177  else if(gcc_attr_mode == "__DI__") // 64 bits
178  {
180  {
181  if(is_signed)
183  else
185  }
186  else
187  {
188  assert(config.ansi_c.long_long_int_width==64);
189 
190  if(is_signed)
192  else
194  }
195  }
196  else if(gcc_attr_mode == "__TI__") // 128 bits
197  {
198  if(is_signed)
200  else
202  }
203  else if(gcc_attr_mode == "__V2SI__") // vector of 2 ints, deprecated
204  {
205  if(is_signed)
207  signed_int_type(),
208  from_integer(2, size_type()));
209  else
212  from_integer(2, size_type()));
213  }
214  else if(gcc_attr_mode == "__V4SI__") // vector of 4 ints, deprecated
215  {
216  if(is_signed)
218  signed_int_type(),
219  from_integer(4, size_type()));
220  else
223  from_integer(4, size_type()));
224  }
225  else // give up, just use subtype
226  result=type.subtype();
227 
228  // save the location
229  result.add_source_location()=type.source_location();
230 
231  if(type.subtype().id()==ID_c_enum_tag)
232  {
233  const irep_idt &tag_name=
234  to_c_enum_tag_type(type.subtype()).get_identifier();
236  }
237 
238  type=result;
239  }
240  else if(underlying_type.id()==ID_floatbv)
241  {
242  typet result;
243 
244  if(gcc_attr_mode == "__SF__") // 32 bits
245  result=float_type();
246  else if(gcc_attr_mode == "__DF__") // 64 bits
248  else if(gcc_attr_mode == "__TF__") // 128 bits
250  else if(gcc_attr_mode == "__V2SF__") // deprecated vector of 2 floats
252  else if(gcc_attr_mode == "__V2DF__") // deprecated vector of 2 doubles
254  else if(gcc_attr_mode == "__V4SF__") // deprecated vector of 4 floats
256  else if(gcc_attr_mode == "__V4DF__") // deprecated vector of 4 doubles
258  else // give up, just use subtype
259  result=type.subtype();
260 
261  // save the location
262  result.add_source_location()=type.source_location();
263 
264  type=result;
265  }
266  else if(underlying_type.id()==ID_complex)
267  {
268  // gcc allows this, but clang doesn't -- see enums above
269  typet result;
270 
271  if(gcc_attr_mode == "__SC__") // 32 bits
272  result=float_type();
273  else if(gcc_attr_mode == "__DC__") // 64 bits
275  else if(gcc_attr_mode == "__TC__") // 128 bits
277  else // give up, just use subtype
278  result=type.subtype();
279 
280  // save the location
281  result.add_source_location()=type.source_location();
282 
283  type=complex_typet(result);
284  }
285  else
286  {
288  error() << "attribute mode `" << gcc_attr_mode
289  << "' applied to inappropriate type `" << to_string(type) << "'"
290  << eom;
291  throw 0;
292  }
293  }
294 
295  // do a mild bit of rule checking
296 
297  if(type.get_bool(ID_C_restricted) &&
298  type.id()!=ID_pointer &&
299  type.id()!=ID_array)
300  {
302  error() << "only a pointer can be 'restrict'" << eom;
303  throw 0;
304  }
305 }
306 
308 {
309  // they all have a width
310  exprt size_expr=
311  static_cast<const exprt &>(type.find(ID_size));
312 
313  typecheck_expr(size_expr);
314  source_locationt source_location=size_expr.source_location();
315  make_constant_index(size_expr);
316 
317  mp_integer size_int;
318  if(to_integer(size_expr, size_int))
319  {
320  error().source_location=source_location;
321  error() << "failed to convert bit vector width to constant" << eom;
322  throw 0;
323  }
324 
325  if(size_int<1)
326  {
327  error().source_location=source_location;
328  error() << "bit vector width invalid" << eom;
329  throw 0;
330  }
331 
332  type.remove(ID_size);
333  type.set(ID_width, integer2string(size_int));
334 
335  // depending on type, there may be a number of fractional bits
336 
337  if(type.id()==ID_custom_unsignedbv)
338  type.id(ID_unsignedbv);
339  else if(type.id()==ID_custom_signedbv)
340  type.id(ID_signedbv);
341  else if(type.id()==ID_custom_fixedbv)
342  {
343  type.id(ID_fixedbv);
344 
345  exprt f_expr=
346  static_cast<const exprt &>(type.find(ID_f));
347 
348  const source_locationt fraction_source_location =
349  f_expr.find_source_location();
350 
351  typecheck_expr(f_expr);
352 
353  make_constant_index(f_expr);
354 
355  mp_integer f_int;
356  if(to_integer(f_expr, f_int))
357  {
358  error().source_location = fraction_source_location;
359  error() << "failed to convert number of fraction bits to constant" << eom;
360  throw 0;
361  }
362 
363  if(f_int<0 || f_int>size_int)
364  {
365  error().source_location = fraction_source_location;
366  error() << "fixedbv fraction width invalid" << eom;
367  throw 0;
368  }
369 
370  type.remove(ID_f);
371  type.set(ID_integer_bits, integer2string(size_int-f_int));
372  }
373  else if(type.id()==ID_custom_floatbv)
374  {
375  type.id(ID_floatbv);
376 
377  exprt f_expr=
378  static_cast<const exprt &>(type.find(ID_f));
379 
380  const source_locationt fraction_source_location =
381  f_expr.find_source_location();
382 
383  typecheck_expr(f_expr);
384 
385  make_constant_index(f_expr);
386 
387  mp_integer f_int;
388  if(to_integer(f_expr, f_int))
389  {
390  error().source_location = fraction_source_location;
391  error() << "failed to convert number of fraction bits to constant" << eom;
392  throw 0;
393  }
394 
395  if(f_int<1 || f_int+1>=size_int)
396  {
397  error().source_location = fraction_source_location;
398  error() << "floatbv fraction width invalid" << eom;
399  throw 0;
400  }
401 
402  type.remove(ID_f);
403  type.set(ID_f, integer2string(f_int));
404  }
405  else
406  UNREACHABLE;
407 }
408 
410 {
411  // the return type is still 'subtype()'
412  type.return_type()=type.subtype();
413  type.remove_subtype();
414 
415  code_typet::parameterst &parameters=type.parameters();
416 
417  // if we don't have any parameters, we assume it's (...)
418  if(parameters.empty())
419  {
420  type.make_ellipsis();
421  }
422  else // we do have parameters
423  {
424  // is the last one ellipsis?
425  if(type.parameters().back().id()==ID_ellipsis)
426  {
427  type.make_ellipsis();
428  type.parameters().pop_back();
429  }
430 
431  parameter_map.clear();
432 
433  for(auto &param : type.parameters())
434  {
435  // turn the declarations into parameters
436  if(param.id()==ID_declaration)
437  {
438  ansi_c_declarationt &declaration=
439  to_ansi_c_declaration(param);
440 
441  code_typet::parametert parameter;
442 
443  // first fix type
444  typet &param_type = parameter.type();
445  param_type = declaration.full_type(declaration.declarator());
446  std::list<codet> tmp_clean_code;
447  tmp_clean_code.swap(clean_code); // ignore side-effects
448  typecheck_type(param_type);
449  tmp_clean_code.swap(clean_code);
450  adjust_function_parameter(param_type);
451 
452  // adjust the identifier
453  irep_idt identifier=declaration.declarator().get_name();
454 
455  // abstract or not?
456  if(identifier.empty())
457  {
458  // abstract
459  parameter.add_source_location()=declaration.type().source_location();
460  }
461  else
462  {
463  // make visible now, later parameters might use it
464  parameter_map[identifier] = param_type;
465  parameter.set_base_name(declaration.declarator().get_base_name());
466  parameter.add_source_location()=
467  declaration.declarator().source_location();
468  }
469 
470  // put the parameter in place of the declaration
471  param.swap(parameter);
472  }
473  }
474 
475  parameter_map.clear();
476 
477  if(parameters.size()==1 &&
478  follow(parameters[0].type()).id()==ID_empty)
479  {
480  // if we just have one parameter of type void, remove it
481  parameters.clear();
482  }
483  }
484 
485  typecheck_type(type.return_type());
486 
487  // 6.7.6.3:
488  // "A function declarator shall not specify a return type that
489  // is a function type or an array type."
490 
491  const typet &decl_return_type = follow(type.return_type());
492 
493  if(decl_return_type.id() == ID_array)
494  {
496  error() << "function must not return array" << eom;
497  throw 0;
498  }
499 
500  if(decl_return_type.id() == ID_code)
501  {
503  error() << "function must not return function type" << eom;
504  throw 0;
505  }
506 }
507 
509 {
510  exprt &size=type.size();
511  const source_locationt size_source_location = size.find_source_location();
512 
513  // check subtype
514  typecheck_type(type.subtype());
515 
516  // we don't allow void as subtype
517  if(type.subtype().id() == ID_empty)
518  {
520  error() << "array of voids" << eom;
521  throw 0;
522  }
523 
524  // we don't allow incomplete structs or unions as subtype
525  if(
526  follow(type.subtype()).id() == ID_incomplete_struct ||
527  follow(type.subtype()).id() == ID_incomplete_union)
528  {
529  // ISO/IEC 9899 6.7.5.2
531  error() << "array has incomplete element type" << eom;
532  throw 0;
533  }
534 
535  // we don't allow functions as subtype
536  if(type.subtype().id() == ID_code)
537  {
538  // ISO/IEC 9899 6.7.5.2
540  error() << "array of function element type" << eom;
541  throw 0;
542  }
543 
544  // check size, if any
545 
546  if(size.is_not_nil())
547  {
548  typecheck_expr(size);
549  make_index_type(size);
550 
551  // The size need not be a constant!
552  // We simplify it, for the benefit of array initialisation.
553 
554  exprt tmp_size=size;
555  add_rounding_mode(tmp_size);
556  simplify(tmp_size, *this);
557 
558  if(tmp_size.is_constant())
559  {
560  mp_integer s;
561  if(to_integer(tmp_size, s))
562  {
563  error().source_location = size_source_location;
564  error() << "failed to convert constant: "
565  << tmp_size.pretty() << eom;
566  throw 0;
567  }
568 
569  if(s<0)
570  {
571  error().source_location = size_source_location;
572  error() << "array size must not be negative, "
573  "but got " << s << eom;
574  throw 0;
575  }
576 
577  size=tmp_size;
578  }
579  else if(tmp_size.id()==ID_infinity)
580  {
581  size=tmp_size;
582  }
583  else if(tmp_size.id()==ID_symbol &&
584  tmp_size.type().get_bool(ID_C_constant))
585  {
586  // We allow a constant variable as array size, assuming
587  // it won't change.
588  // This criterion can be tricked:
589  // Of course we can modify a 'const' symbol, e.g.,
590  // using a pointer type cast. Interestingly,
591  // at least gcc 4.2.1 makes the very same mistake!
592  size=tmp_size;
593  }
594  else
595  {
596  // not a constant and not infinity
597 
599 
601  {
603  error() << "array size of static symbol `"
604  << current_symbol.base_name << "' is not constant" << eom;
605  throw 0;
606  }
607 
608  // Need to pull out! We insert new symbol.
609  unsigned count=0;
610  irep_idt temp_identifier;
611  std::string suffix;
612 
613  do
614  {
615  suffix="$array_size"+std::to_string(count);
616  temp_identifier=id2string(current_symbol.name)+suffix;
617  count++;
618  }
619  while(symbol_table.symbols.find(temp_identifier)!=
620  symbol_table.symbols.end());
621 
622  // add the symbol to symbol table
623  auxiliary_symbolt new_symbol;
624  new_symbol.name=temp_identifier;
625  new_symbol.pretty_name=id2string(current_symbol.pretty_name)+suffix;
626  new_symbol.base_name=id2string(current_symbol.base_name)+suffix;
627  new_symbol.type=size.type();
628  new_symbol.type.set(ID_C_constant, true);
629  new_symbol.value=size;
630  new_symbol.location = size_source_location;
631  new_symbol.mode = mode;
632 
633  symbol_table.add(new_symbol);
634 
635  // produce the code that declares and initializes the symbol
636  symbol_exprt symbol_expr;
637  symbol_expr.set_identifier(temp_identifier);
638  symbol_expr.type()=new_symbol.type;
639 
640  code_declt declaration(symbol_expr);
641  declaration.add_source_location() = size_source_location;
642 
643  code_assignt assignment;
644  assignment.lhs()=symbol_expr;
645  assignment.rhs()=size;
646  assignment.add_source_location() = size_source_location;
647 
648  // store the code
649  clean_code.push_back(declaration);
650  clean_code.push_back(assignment);
651 
652  // fix type
653  size=symbol_expr;
654  }
655  }
656 }
657 
659 {
660  exprt &size=type.size();
661  source_locationt source_location=size.find_source_location();
662 
663  typecheck_expr(size);
664 
665  typet &subtype=type.subtype();
666  typecheck_type(subtype);
667 
668  // we are willing to combine 'vector' with various
669  // other types, but not everything!
670 
671  if(subtype.id()!=ID_signedbv &&
672  subtype.id()!=ID_unsignedbv &&
673  subtype.id()!=ID_floatbv &&
674  subtype.id()!=ID_fixedbv)
675  {
676  error().source_location=source_location;
677  error() << "cannot make a vector of subtype "
678  << to_string(subtype) << eom;
679  throw 0;
680  }
681 
682  make_constant_index(size);
683 
684  mp_integer s;
685  if(to_integer(size, s))
686  {
687  error().source_location=source_location;
688  error() << "failed to convert constant: "
689  << size.pretty() << eom;
690  throw 0;
691  }
692 
693  if(s<=0)
694  {
695  error().source_location=source_location;
696  error() << "vector size must be positive, "
697  "but got " << s << eom;
698  throw 0;
699  }
700 
701  // the subtype must have constant size
702  exprt size_expr=size_of_expr(type.subtype(), *this);
703 
704  simplify(size_expr, *this);
705 
706  mp_integer sub_size;
707 
708  if(to_integer(size_expr, sub_size))
709  {
710  error().source_location=source_location;
711  error() << "failed to determine size of vector base type `"
712  << to_string(type.subtype()) << "'" << eom;
713  throw 0;
714  }
715 
716  if(sub_size==0)
717  {
718  error().source_location=source_location;
719  error() << "type had size 0: `"
720  << to_string(type.subtype()) << "'" << eom;
721  throw 0;
722  }
723 
724  // adjust by width of base type
725  if(s%sub_size!=0)
726  {
727  error().source_location=source_location;
728  error() << "vector size (" << s
729  << ") expected to be multiple of base type size (" << sub_size
730  << ")" << eom;
731  throw 0;
732  }
733 
734  s/=sub_size;
735 
736  type.size()=from_integer(s, signed_size_type());
737 }
738 
740 {
741  // These get replaced by symbol types later.
742  irep_idt identifier;
743 
744  bool have_body=type.find(ID_components).is_not_nil();
745 
746  c_qualifierst original_qualifiers(type);
747 
748  // the type symbol, which may get re-used in other declarations, must not
749  // carry any qualifiers (other than transparent_union, which isn't really a
750  // qualifier)
751  c_qualifierst remove_qualifiers;
752  remove_qualifiers.is_transparent_union =
753  original_qualifiers.is_transparent_union;
754  remove_qualifiers.write(type);
755 
756  if(type.find(ID_tag).is_nil())
757  {
758  // Anonymous? Must come with body.
759  assert(have_body);
760 
761  // produce symbol
762  symbolt compound_symbol;
763  compound_symbol.is_type=true;
764  compound_symbol.type=type;
765  compound_symbol.location=type.source_location();
766 
768 
769  std::string typestr=type2name(compound_symbol.type);
770  compound_symbol.base_name="#anon-"+typestr;
771  compound_symbol.name="tag-#anon#"+typestr;
772  identifier=compound_symbol.name;
773 
774  // We might already have the same anonymous union/struct,
775  // and this is simply ok. Note that the C standard treats
776  // these as different types.
777  if(symbol_table.symbols.find(identifier)==symbol_table.symbols.end())
778  {
779  symbolt *new_symbol;
780  move_symbol(compound_symbol, new_symbol);
781  }
782  }
783  else
784  {
785  identifier=type.find(ID_tag).get(ID_identifier);
786 
787  // does it exist already?
788  symbol_tablet::symbolst::const_iterator s_it=
789  symbol_table.symbols.find(identifier);
790 
791  if(s_it==symbol_table.symbols.end())
792  {
793  // no, add new symbol
794  irep_idt base_name=type.find(ID_tag).get(ID_C_base_name);
795  type.remove(ID_tag);
796  type.set(ID_tag, base_name);
797 
798  symbolt compound_symbol;
799  compound_symbol.is_type=true;
800  compound_symbol.name=identifier;
801  compound_symbol.base_name=base_name;
802  compound_symbol.type=type;
803  compound_symbol.location=type.source_location();
804  compound_symbol.pretty_name=id2string(type.id())+" "+id2string(base_name);
805 
806  typet new_type=compound_symbol.type;
807 
808  if(compound_symbol.type.id()==ID_struct)
809  compound_symbol.type.id(ID_incomplete_struct);
810  else if(compound_symbol.type.id()==ID_union)
811  compound_symbol.type.id(ID_incomplete_union);
812  else
813  UNREACHABLE;
814 
815  symbolt *new_symbol;
816  move_symbol(compound_symbol, new_symbol);
817 
818  if(have_body)
819  {
821 
822  new_symbol->type.swap(new_type);
823  }
824  }
825  else
826  {
827  // yes, it exists already
828  if(s_it->second.type.id()==ID_incomplete_struct ||
829  s_it->second.type.id()==ID_incomplete_union)
830  {
831  // Maybe we got a body now.
832  if(have_body)
833  {
834  irep_idt base_name=type.find(ID_tag).get(ID_C_base_name);
835  type.remove(ID_tag);
836  type.set(ID_tag, base_name);
837 
839  symbol_table.get_writeable_ref(s_it->first).type.swap(type);
840  }
841  }
842  else if(have_body)
843  {
845  error() << "redefinition of body of `"
846  << s_it->second.pretty_name << "'" << eom;
847  throw 0;
848  }
849  }
850  }
851 
852  typet tag_type;
853 
854  if(type.id() == ID_union || type.id() == ID_incomplete_union)
855  tag_type = union_tag_typet(identifier);
856  else if(type.id() == ID_struct || type.id() == ID_incomplete_struct)
857  tag_type = struct_tag_typet(identifier);
858  else
859  UNREACHABLE;
860 
861  tag_type.add_source_location() = type.source_location();
862  type.swap(tag_type);
863 
864  original_qualifiers.write(type);
865 }
866 
868  struct_union_typet &type)
869 {
870  struct_union_typet::componentst &components=type.components();
871 
872  struct_union_typet::componentst old_components;
873  old_components.swap(components);
874 
875  // We get these as declarations!
876  for(auto &decl : old_components)
877  {
878  // the arguments are member declarations or static assertions
879  assert(decl.id()==ID_declaration);
880 
881  ansi_c_declarationt &declaration=
882  to_ansi_c_declaration(static_cast<exprt &>(decl));
883 
884  if(declaration.get_is_static_assert())
885  {
886  struct_union_typet::componentt new_component;
887  new_component.id(ID_static_assert);
888  new_component.add_source_location()=declaration.source_location();
889  new_component.operands().swap(declaration.operands());
890  assert(new_component.operands().size()==2);
891  components.push_back(new_component);
892  }
893  else
894  {
895  // do first half of type
896  typecheck_type(declaration.type());
897  make_already_typechecked(declaration.type());
898 
899  for(const auto &declarator : declaration.declarators())
900  {
901  struct_union_typet::componentt new_component(
902  declarator.get_base_name(), declaration.full_type(declarator));
903 
904  // There may be a declarator, which we use as location for
905  // the component. Otherwise, use location of the declaration.
906  const source_locationt source_location =
907  declarator.get_name().empty() ? declaration.source_location()
908  : declarator.source_location();
909 
910  new_component.add_source_location() = source_location;
911  new_component.set_pretty_name(declarator.get_base_name());
912 
913  typecheck_type(new_component.type());
914 
915  if(!is_complete_type(new_component.type()) &&
916  (new_component.type().id()!=ID_array ||
917  !to_array_type(new_component.type()).is_incomplete()))
918  {
919  error().source_location = source_location;
920  error() << "incomplete type not permitted here" << eom;
921  throw 0;
922  }
923 
924  components.push_back(new_component);
925  }
926  }
927  }
928 
929  unsigned anon_member_counter=0;
930 
931  // scan for anonymous members, and name them
932  for(auto &member : components)
933  {
934  if(!member.get_name().empty())
935  continue;
936 
937  member.set_name("$anon"+std::to_string(anon_member_counter++));
938  member.set_anonymous(true);
939  }
940 
941  // scan for duplicate members
942 
943  {
944  std::unordered_set<irep_idt> members;
945 
946  for(const auto &c : components)
947  {
948  if(!members.insert(c.get_name()).second)
949  {
950  error().source_location = c.source_location();
951  error() << "duplicate member '" << c.get_name() << '\'' << eom;
952  throw 0;
953  }
954  }
955  }
956 
957  // We allow an incomplete (C99) array as _last_ member!
958  // Zero-length is allowed everywhere.
959 
960  if(type.id()==ID_struct ||
961  type.id()==ID_union)
962  {
963  for(struct_union_typet::componentst::iterator
964  it=components.begin();
965  it!=components.end();
966  it++)
967  {
968  typet &c_type=it->type();
969 
970  if(c_type.id()==ID_array &&
971  to_array_type(c_type).is_incomplete())
972  {
973  // needs to be last member
974  if(type.id()==ID_struct && it!=--components.end())
975  {
976  error().source_location=it->source_location();
977  error() << "flexible struct member must be last member" << eom;
978  throw 0;
979  }
980 
981  // make it zero-length
982  c_type.id(ID_array);
983  c_type.set(ID_size, from_integer(0, index_type()));
984  }
985  }
986  }
987 
988  // We may add some minimal padding inside and at
989  // the end of structs and
990  // as additional member for unions.
991 
992  if(type.id()==ID_struct)
993  add_padding(to_struct_type(type), *this);
994  else if(type.id()==ID_union)
995  add_padding(to_union_type(type), *this);
996 
997  // Now remove zero-width bit-fields, these are just
998  // for adjusting alignment.
999  for(struct_typet::componentst::iterator
1000  it=components.begin();
1001  it!=components.end();
1002  ) // blank
1003  {
1004  if(it->type().id()==ID_c_bit_field &&
1005  to_c_bit_field_type(it->type()).get_width()==0)
1006  it=components.erase(it);
1007  else
1008  it++;
1009  }
1010 
1011  // finally, check _Static_assert inside the compound
1012  for(struct_union_typet::componentst::iterator
1013  it=components.begin();
1014  it!=components.end();
1015  ) // no it++
1016  {
1017  if(it->id()==ID_static_assert)
1018  {
1019  assert(it->operands().size()==2);
1020  exprt &assertion=it->op0();
1021  typecheck_expr(assertion);
1022  typecheck_expr(it->op1());
1023  assertion.make_typecast(bool_typet());
1024  make_constant(assertion);
1025 
1026  if(assertion.is_false())
1027  {
1028  error().source_location=it->source_location();
1029  error() << "failed _Static_assert" << eom;
1030  throw 0;
1031  }
1032  else if(!assertion.is_true())
1033  {
1034  // should warn/complain
1035  }
1036 
1037  it=components.erase(it);
1038  }
1039  else
1040  it++;
1041  }
1042 }
1043 
1045  const mp_integer &min_value,
1046  const mp_integer &max_value) const
1047 {
1049  {
1050  return signed_int_type();
1051  }
1052  else
1053  {
1054  // enum constants are at least 'int', but may be made larger.
1055  // 'Packing' has no influence.
1056  if(max_value<(mp_integer(1)<<(config.ansi_c.int_width-1)) &&
1057  min_value>=-(mp_integer(1)<<(config.ansi_c.int_width-1)))
1058  return signed_int_type();
1059  else if(max_value<(mp_integer(1)<<config.ansi_c.int_width) &&
1060  min_value>=0)
1061  return unsigned_int_type();
1063  min_value>=0)
1064  return unsigned_long_int_type();
1066  min_value>=0)
1067  return unsigned_long_long_int_type();
1068  else if(max_value<(mp_integer(1)<<(config.ansi_c.long_int_width-1)) &&
1069  min_value>=-(mp_integer(1)<<(config.ansi_c.long_int_width-1)))
1070  return signed_long_int_type();
1071  else
1072  return signed_long_long_int_type();
1073  }
1074 }
1075 
1077  const mp_integer &min_value,
1078  const mp_integer &max_value,
1079  bool is_packed) const
1080 {
1082  {
1083  return signed_int_type();
1084  }
1085  else
1086  {
1087  if(min_value<0)
1088  {
1089  // We'll want a signed type.
1090 
1091  if(is_packed)
1092  {
1093  // If packed, there are smaller options.
1094  if(max_value<(mp_integer(1)<<(config.ansi_c.char_width-1)) &&
1095  min_value>=-(mp_integer(1)<<(config.ansi_c.char_width-1)))
1096  return signed_char_type();
1097  else if(max_value<(mp_integer(1)<<(config.ansi_c.short_int_width-1)) &&
1098  min_value>=-(mp_integer(1)<<(config.ansi_c.short_int_width-1)))
1099  return signed_short_int_type();
1100  }
1101 
1102  if(max_value<(mp_integer(1)<<(config.ansi_c.int_width-1)) &&
1103  min_value>=-(mp_integer(1)<<(config.ansi_c.int_width-1)))
1104  return signed_int_type();
1105  else if(max_value<(mp_integer(1)<<(config.ansi_c.long_int_width-1)) &&
1106  min_value>=-(mp_integer(1)<<(config.ansi_c.long_int_width-1)))
1107  return signed_long_int_type();
1108  else
1109  return signed_long_long_int_type();
1110  }
1111  else
1112  {
1113  // We'll want an unsigned type.
1114 
1115  if(is_packed)
1116  {
1117  // If packed, there are smaller options.
1119  return unsigned_char_type();
1121  return unsigned_short_int_type();
1122  }
1123 
1125  return unsigned_int_type();
1127  return unsigned_long_int_type();
1128  else
1129  return unsigned_long_long_int_type();
1130  }
1131  }
1132 }
1133 
1135 {
1136  // These come with the declarations
1137  // of the enum constants as operands.
1138 
1139  exprt &as_expr=static_cast<exprt &>(static_cast<irept &>(type));
1140  source_locationt source_location=type.source_location();
1141 
1142  // We allow empty enums in the grammar to get better
1143  // error messages.
1144  if(as_expr.operands().empty())
1145  {
1146  error().source_location=source_location;
1147  error() << "empty enum" << eom;
1148  throw 0;
1149  }
1150 
1151  // enums start at zero;
1152  // we also track min and max to find a nice base type
1153  mp_integer value=0, min_value=0, max_value=0;
1154 
1155  std::list<c_enum_typet::c_enum_membert> enum_members;
1156 
1157  // We need to determine a width, and a signedness
1158  // to obtain an 'underlying type'.
1159  // We just do int, but gcc might pick smaller widths
1160  // if the type is marked as 'packed'.
1161  // gcc/clang may also pick a larger width. Visual Studio doesn't.
1162 
1163  for(auto &op : as_expr.operands())
1164  {
1165  ansi_c_declarationt &declaration=to_ansi_c_declaration(op);
1166  exprt &v=declaration.declarator().value();
1167 
1168  if(v.is_not_nil()) // value given?
1169  {
1170  exprt tmp_v=v;
1171  typecheck_expr(tmp_v);
1172  add_rounding_mode(tmp_v);
1173  simplify(tmp_v, *this);
1174  if(tmp_v.is_true())
1175  value=1;
1176  else if(tmp_v.is_false())
1177  value=0;
1178  else if(!to_integer(tmp_v, value))
1179  {
1180  }
1181  else
1182  {
1184  error() << "enum is not a constant";
1185  throw 0;
1186  }
1187  }
1188 
1189  if(value<min_value)
1190  min_value=value;
1191  if(value>max_value)
1192  max_value=value;
1193 
1194  typet constant_type=
1195  enum_constant_type(min_value, max_value);
1196 
1197  v=from_integer(value, constant_type);
1198 
1199  declaration.type()=constant_type;
1200  typecheck_declaration(declaration);
1201 
1202  irep_idt base_name=
1203  declaration.declarator().get_base_name();
1204 
1205  irep_idt identifier=
1206  declaration.declarator().get_name();
1207 
1208  // store
1210  member.set_identifier(identifier);
1211  member.set_base_name(base_name);
1212  member.set_value(integer2string(value));
1213  enum_members.push_back(member);
1214 
1215  // produce value for next constant
1216  ++value;
1217  }
1218 
1219  // Remove these now; we add them to the
1220  // c_enum symbol later.
1221  as_expr.operands().clear();
1222 
1223  bool is_packed=type.get_bool(ID_C_packed);
1224 
1225  // tag?
1226  if(type.find(ID_tag).is_nil())
1227  {
1228  // None, it's anonymous. We generate a tag.
1229  std::string anon_identifier="#anon_enum";
1230 
1231  for(const auto &member : enum_members)
1232  {
1233  anon_identifier+='$';
1234  anon_identifier+=id2string(member.get_base_name());
1235  anon_identifier+='=';
1236  anon_identifier+=id2string(member.get_value());
1237  }
1238 
1239  if(is_packed)
1240  anon_identifier+="#packed";
1241 
1242  type.add(ID_tag).set(ID_identifier, anon_identifier);
1243  }
1244 
1245  irept &tag=type.add(ID_tag);
1246  irep_idt base_name=tag.get(ID_C_base_name);
1247  irep_idt identifier=tag.get(ID_identifier);
1248 
1249  // Put into symbol table
1250  symbolt enum_tag_symbol;
1251 
1252  enum_tag_symbol.is_type=true;
1253  enum_tag_symbol.type=type;
1254  enum_tag_symbol.location=source_location;
1255  enum_tag_symbol.is_file_local=true;
1256  enum_tag_symbol.base_name=base_name;
1257  enum_tag_symbol.name=identifier;
1258 
1259  // throw in the enum members as 'body'
1260  irept::subt &body=enum_tag_symbol.type.add(ID_body).get_sub();
1261 
1262  for(const auto &member : enum_members)
1263  body.push_back(member);
1264 
1265  // We use a subtype to store the underlying type.
1266  typet underlying_type=
1267  enum_underlying_type(min_value, max_value, is_packed);
1268 
1269  enum_tag_symbol.type.subtype()=underlying_type;
1270 
1271  // is it in the symbol table already?
1272  symbol_tablet::symbolst::const_iterator s_it=
1273  symbol_table.symbols.find(identifier);
1274 
1275  if(s_it!=symbol_table.symbols.end())
1276  {
1277  // Yes.
1278  const symbolt &symbol=s_it->second;
1279 
1280  if(symbol.type.id()==ID_incomplete_c_enum)
1281  {
1282  // Ok, overwrite the type in the symbol table.
1283  // This gives us the members and the subtype.
1284  symbol_table.get_writeable_ref(symbol.name).type=enum_tag_symbol.type;
1285  }
1286  else if(symbol.type.id()==ID_c_enum)
1287  {
1288  // We might already have the same anonymous enum, and this is
1289  // simply ok. Note that the C standard treats these as
1290  // different types.
1291  if(!base_name.empty())
1292  {
1294  error() << "redeclaration of enum tag" << eom;
1295  throw 0;
1296  }
1297  }
1298  else
1299  {
1300  error().source_location=source_location;
1301  error() << "use of tag that does not match previous declaration" << eom;
1302  throw 0;
1303  }
1304  }
1305  else
1306  {
1307  symbolt *new_symbol;
1308  move_symbol(enum_tag_symbol, new_symbol);
1309  }
1310 
1311  // We produce a c_enum_tag as the resulting type.
1312  type.id(ID_c_enum_tag);
1313  type.remove(ID_tag);
1314  type.set(ID_identifier, identifier);
1315 }
1316 
1318 {
1319  // It's just a tag.
1320 
1321  if(type.find(ID_tag).is_nil())
1322  {
1324  error() << "anonymous enum tag without members" << eom;
1325  throw 0;
1326  }
1327 
1328  source_locationt source_location=type.source_location();
1329 
1330  irept &tag=type.add(ID_tag);
1331  irep_idt base_name=tag.get(ID_C_base_name);
1332  irep_idt identifier=tag.get(ID_identifier);
1333 
1334  // is it in the symbol table?
1335  symbol_tablet::symbolst::const_iterator s_it=
1336  symbol_table.symbols.find(identifier);
1337 
1338  if(s_it!=symbol_table.symbols.end())
1339  {
1340  // Yes.
1341  const symbolt &symbol=s_it->second;
1342 
1343  if(symbol.type.id()!=ID_c_enum &&
1344  symbol.type.id()!=ID_incomplete_c_enum)
1345  {
1346  error().source_location=source_location;
1347  error() << "use of tag that does not match previous declaration" << eom;
1348  throw 0;
1349  }
1350  }
1351  else
1352  {
1353  // no, add it as an incomplete c_enum
1354  typet new_type(ID_incomplete_c_enum);
1355  new_type.subtype()=signed_int_type(); // default
1356  new_type.add(ID_tag)=tag;
1357 
1358  symbolt enum_tag_symbol;
1359 
1360  enum_tag_symbol.is_type=true;
1361  enum_tag_symbol.type=new_type;
1362  enum_tag_symbol.location=source_location;
1363  enum_tag_symbol.is_file_local=true;
1364  enum_tag_symbol.base_name=base_name;
1365  enum_tag_symbol.name=identifier;
1366 
1367  symbolt *new_symbol;
1368  move_symbol(enum_tag_symbol, new_symbol);
1369  }
1370 
1371  // Clean up resulting type
1372  type.remove(ID_tag);
1373  type.set_identifier(identifier);
1374 }
1375 
1377 {
1378  typecheck_type(type.subtype());
1379 
1380  mp_integer i;
1381 
1382  {
1383  exprt &width_expr=static_cast<exprt &>(type.add(ID_size));
1384 
1385  typecheck_expr(width_expr);
1386  make_constant_index(width_expr);
1387 
1388  if(to_integer(width_expr, i))
1389  {
1391  error() << "failed to convert bit field width" << eom;
1392  throw 0;
1393  }
1394 
1395  if(i<0)
1396  {
1398  error() << "bit field width is negative" << eom;
1399  throw 0;
1400  }
1401 
1402  type.set_width(numeric_cast_v<std::size_t>(i));
1403  type.remove(ID_size);
1404  }
1405 
1406  const typet &subtype=follow(type.subtype());
1407 
1408  std::size_t sub_width=0;
1409 
1410  if(subtype.id()==ID_bool)
1411  {
1412  // This is the 'proper' bool.
1413  sub_width=1;
1414  }
1415  else if(subtype.id()==ID_signedbv ||
1416  subtype.id()==ID_unsignedbv ||
1417  subtype.id()==ID_c_bool)
1418  {
1419  sub_width=to_bitvector_type(subtype).get_width();
1420  }
1421  else if(subtype.id()==ID_c_enum_tag)
1422  {
1423  // These point to an enum, which has a sub-subtype,
1424  // which may be smaller or larger than int, and we thus have
1425  // to check.
1426  const typet &c_enum_type=
1427  follow_tag(to_c_enum_tag_type(subtype));
1428 
1429  if(c_enum_type.id()==ID_incomplete_c_enum)
1430  {
1432  error() << "bit field has incomplete enum type" << eom;
1433  throw 0;
1434  }
1435 
1436  sub_width = c_enum_type.subtype().get_size_t(ID_width);
1437  }
1438  else
1439  {
1441  error() << "bit field with non-integer type: "
1442  << to_string(subtype) << eom;
1443  throw 0;
1444  }
1445 
1446  if(i>sub_width)
1447  {
1449  error() << "bit field (" << i
1450  << " bits) larger than type (" << sub_width << " bits)"
1451  << eom;
1452  throw 0;
1453  }
1454 }
1455 
1457 {
1458  // save location
1459  source_locationt source_location=type.source_location();
1460 
1461  // retain the qualifiers as is
1462  c_qualifierst c_qualifiers;
1463  c_qualifiers.read(type);
1464 
1465  if(!((const exprt &)type).has_operands())
1466  {
1467  typet t=static_cast<const typet &>(type.find(ID_type_arg));
1468  typecheck_type(t);
1469  type.swap(t);
1470  }
1471  else
1472  {
1473  exprt expr=((const exprt &)type).op0();
1474  typecheck_expr(expr);
1475 
1476  // undo an implicit address-of
1477  if(expr.id()==ID_address_of &&
1478  expr.get_bool(ID_C_implicit))
1479  {
1480  assert(expr.operands().size()==1);
1481  exprt tmp;
1482  tmp.swap(expr.op0());
1483  expr.swap(tmp);
1484  }
1485 
1486  type.swap(expr.type());
1487  }
1488 
1489  type.add_source_location()=source_location;
1490  c_qualifiers.write(type);
1491 }
1492 
1494 {
1495  const irep_idt &identifier = to_typedef_type(type).get_identifier();
1496 
1497  symbol_tablet::symbolst::const_iterator s_it =
1498  symbol_table.symbols.find(identifier);
1499 
1500  if(s_it == symbol_table.symbols.end())
1501  {
1503  error() << "typedef symbol `" << identifier << "' not found" << eom;
1504  throw 0;
1505  }
1506 
1507  const symbolt &symbol = s_it->second;
1508 
1509  if(!symbol.is_type)
1510  {
1512  error() << "expected type symbol for typedef" << eom;
1513  throw 0;
1514  }
1515 
1516  // overwrite, but preserve (add) any qualifiers and other flags
1517 
1518  c_qualifierst c_qualifiers(type);
1519  bool is_packed = type.get_bool(ID_C_packed);
1520  irept alignment = type.find(ID_C_alignment);
1521 
1522  c_qualifiers += c_qualifierst(symbol.type);
1523  type = symbol.type;
1524  c_qualifiers.write(type);
1525 
1526  if(is_packed)
1527  type.set(ID_C_packed, true);
1528  if(alignment.is_not_nil())
1529  type.set(ID_C_alignment, alignment);
1530 
1531  // CPROVER extensions
1532  if(symbol.base_name == CPROVER_PREFIX "rational")
1533  {
1534  type=rational_typet();
1535  }
1536  else if(symbol.base_name == CPROVER_PREFIX "integer")
1537  {
1538  type=integer_typet();
1539  }
1540 }
1541 
1543 {
1544  if(type.id()==ID_array)
1545  {
1546  source_locationt source_location=type.source_location();
1547  type=pointer_type(type.subtype());
1548  type.add_source_location()=source_location;
1549  }
1550  else if(type.id()==ID_code)
1551  {
1552  // see ISO/IEC 9899:1999 page 199 clause 8,
1553  // may be hidden in typedef
1554  source_locationt source_location=type.source_location();
1555  type=pointer_type(type);
1556  type.add_source_location()=source_location;
1557  }
1558  else if(type.id()==ID_KnR)
1559  {
1560  // any KnR args without type yet?
1561  type=signed_int_type(); // the default is integer!
1562  // no source location
1563  }
1564 }
static std::string type2name(const typet &type, const namespacet &ns, symbol_numbert &symbol_number)
Definition: type2name.cpp:95
virtual void typecheck_typeof_type(typet &type)
The type of an expression, extends irept.
Definition: type.h:27
irep_idt name
The unique identifier.
Definition: symbol.h:40
signedbv_typet gcc_signed_int128_type()
Definition: gcc_types.cpp:83
exprt size_of_expr(const typet &type, const namespacet &ns)
bool is_signed(const typet &t)
Convenience function – is the type signed?
Definition: util.cpp:45
struct configt::ansi_ct ansi_c
virtual bool is_complete_type(const typet &type) const
BigInt mp_integer
Definition: mp_arith.h:22
void typecheck_declaration(ansi_c_declarationt &)
Base type of functions.
Definition: std_types.h:751
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
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:106
exprt & op0()
Definition: expr.h:84
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:640
#define CPROVER_PREFIX
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Definition: std_types.h:1158
std::vector< irept > subt
Definition: irep.h:160
virtual void make_constant(exprt &expr)
irep_idt mode
Language mode.
Definition: symbol.h:49
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
void move_symbol(symbolt &symbol, symbolt *&new_symbol)
unsignedbv_typet unsigned_int_type()
Definition: c_types.cpp:44
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:982
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
Unbounded, signed rational numbers.
std::vector< componentt > componentst
Definition: std_types.h:203
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:99
std::vector< parametert > parameterst
Definition: std_types.h:754
exprt value
Initial value of symbol.
Definition: symbol.h:34
A union tag type, i.e., union_typet with an identifier.
Definition: std_types.h:557
const componentst & components() const
Definition: std_types.h:205
id_type_mapt parameter_map
bool is_incomplete() const
Definition: std_types.h:1025
A struct tag type, i.e., struct_typet with an identifier.
Definition: std_types.h:517
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:90
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:52
typet & type()
Return the type of the expression.
Definition: expr.h:68
void set_identifier(const irep_idt &identifier)
Definition: std_types.h:661
unsignedbv_typet size_type()
Definition: c_types.cpp:58
unsignedbv_typet gcc_unsigned_int128_type()
Definition: gcc_types.cpp:76
The Boolean type.
Definition: std_types.h:28
Symbol table entry.
Definition: symbol.h:27
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:239
configt config
Definition: config.cpp:24
void set_identifier(const irep_idt &identifier)
Definition: std_types.h:474
virtual std::string to_string(const exprt &expr)
std::size_t char_width
Definition: config.h:33
virtual void typecheck_compound_type(struct_union_typet &type)
const typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:90
Type for C bit fields These are both &#39;bitvector_typet&#39; (they have a width) and &#39;type_with_subtypet&#39; (...
Definition: std_types.h:1462
typet full_type(const ansi_c_declaratort &) const
signedbv_typet signed_size_type()
Definition: c_types.cpp:74
bool is_static_lifetime
Definition: symbol.h:65
const irep_idt & get_identifier() const
Definition: typedef_type.h:29
subt & get_sub()
Definition: irep.h:317
void set_base_name(const irep_idt &name)
Definition: std_types.h:823
symbol_tablet & symbol_table
virtual void typecheck_typedef_type(typet &type)
virtual void typecheck_c_enum_tag_type(c_enum_tag_typet &type)
const irep_idt & id() const
Definition: irep.h:259
exprt & lhs()
Definition: std_code.h:269
irep_idt get_base_name() const
std::size_t long_long_int_width
Definition: config.h:35
void add_padding(struct_typet &type, const namespacet &ns)
Definition: padding.cpp:442
void set_value(const irep_idt &value)
Definition: std_types.h:659
ANSI-C Language Type Checking.
virtual void typecheck_c_enum_type(typet &type)
void remove_subtype()
Definition: type.h:59
ANSI-C Language Type Checking.
A codet representing the declaration of a local variable.
Definition: std_code.h:352
flavourt mode
Definition: config.h:115
const irep_idt mode
exprt & rhs()
Definition: std_code.h:274
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
Definition: expr.cpp:229
void make_already_typechecked(typet &dest)
source_locationt source_location
Definition: message.h:236
The vector type.
Definition: std_types.h:1755
virtual void make_index_type(exprt &expr)
mp_integer alignment(const typet &type, const namespacet &ns)
Definition: padding.cpp:21
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:212
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
Definition: symbol.h:148
mstreamt & error() const
Definition: message.h:386
const exprt & size() const
Definition: std_types.h:1765
bool is_transparent_union
Definition: c_qualifiers.h:97
irep_idt get_name() const
virtual void read(const typet &src) override
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
signedbv_typet signed_long_int_type()
Definition: c_types.cpp:80
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition: std_types.h:1793
std::size_t int_width
Definition: config.h:30
const exprt & size() const
Definition: std_types.h:1010
virtual void typecheck_expr(exprt &expr)
Base class for tree-like data structures with sharing.
Definition: irep.h:156
typet enum_constant_type(const mp_integer &min, const mp_integer &max) const
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
std::list< codet > clean_code
const symbolst & symbols
ANSI-C Language Conversion.
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:83
std::size_t get_width() const
Definition: std_types.h:1117
typet enum_underlying_type(const mp_integer &min, const mp_integer &max, bool is_packed) const
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
Definition: std_types.h:737
virtual void typecheck_custom_type(typet &type)
virtual void adjust_function_parameter(typet &type) const
void make_ellipsis()
Definition: std_types.h:873
Pointer Logic.
const source_locationt & source_location() const
Definition: type.h:62
signedbv_typet signed_short_int_type()
Definition: c_types.cpp:37
Unbounded, signed integers (mathematical integers, not bitvectors)
static eomt eom
Definition: message.h:284
Complex numbers made of pair of given subtype.
Definition: std_types.h:1807
const typedef_typet & to_typedef_type(const typet &type)
Cast a generic typet to a typedef_typet.
Definition: typedef_type.h:45
Type Naming for C.
floatbv_typet float_type()
Definition: c_types.cpp:185
typet type
Type of symbol.
Definition: symbol.h:31
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
virtual void typecheck_code_type(code_typet &type)
void read(const typet &type)
message_handlert & get_message_handler()
Definition: message.h:174
virtual void typecheck_vector_type(vector_typet &type)
Base type for structs and unions.
Definition: std_types.h:114
mstreamt & result() const
Definition: message.h:396
virtual void typecheck_compound_body(struct_union_typet &type)
unsignedbv_typet unsigned_short_int_type()
Definition: c_types.cpp:51
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
floatbv_typet double_type()
Definition: c_types.cpp:193
const parameterst & parameters() const
Definition: std_types.h:893
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition: std_types.h:260
source_locationt & add_source_location()
Definition: type.h:67
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
static mp_integer max_value(const typet &type)
Get max value for an integer type.
bool is_file_local
Definition: symbol.h:66
virtual void make_constant_index(exprt &expr)
irept & add(const irep_namet &name)
Definition: irep.cpp:305
void set_identifier(const irep_idt &identifier)
Definition: std_expr.h:171
void swap(irept &irep)
Definition: irep.h:303
virtual void write(typet &src) const override
source_locationt & add_source_location()
Definition: expr.h:233
unsignedbv_typet unsigned_long_long_int_type()
Definition: c_types.cpp:101
Arrays with given size.
Definition: std_types.h:1000
std::string::const_iterator end() const
Definition: dstring.h:160
virtual void typecheck_array_type(array_typet &type)
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a typet to a c_bit_field_typet.
Definition: std_types.h:1491
static void add_rounding_mode(exprt &)
Expression to hold a symbol (variable)
Definition: std_expr.h:143
virtual void typecheck_type(typet &type)
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:19
floatbv_typet gcc_float128_type()
Definition: gcc_types.cpp:58
signedbv_typet signed_int_type()
Definition: c_types.cpp:30
ansi_c_declarationt & to_ansi_c_declaration(exprt &expr)
unsignedbv_typet unsigned_char_type()
Definition: c_types.cpp:135
void remove(const irep_namet &name)
Definition: irep.cpp:269
bool is_type
Definition: symbol.h:61
const typet & subtype() const
Definition: type.h:38
unsignedbv_typet unsigned_long_int_type()
Definition: c_types.cpp:94
signedbv_typet signed_long_long_int_type()
Definition: c_types.cpp:87
operandst & operands()
Definition: expr.h:78
std::size_t long_int_width
Definition: config.h:31
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
virtual void typecheck_c_bit_field_type(c_bit_field_typet &type)
std::size_t get_size_t(const irep_namet &name) const
Definition: irep.cpp:254
bool empty() const
Definition: dstring.h:75
const irept & find(const irep_namet &name) const
Definition: irep.cpp:284
signedbv_typet signed_char_type()
Definition: c_types.cpp:142
C enum tag type, i.e., c_enum_typet with an identifier.
Definition: std_types.h:711
const typet & return_type() const
Definition: std_types.h:883
A codet representing an assignment in the program.
Definition: std_code.h:256
void set_base_name(const irep_idt &base_name)
Definition: std_types.h:666
std::size_t short_int_width
Definition: config.h:34
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:286
bool simplify(exprt &expr, const namespacet &ns)
void set_width(std::size_t width)
Definition: std_types.h:1122
const ansi_c_declaratort & declarator() const