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