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  if(type.find(ID_tag).is_nil())
765  {
766  // Anonymous? Must come with body.
767  assert(have_body);
768 
769  // produce symbol
770  symbolt compound_symbol;
771  compound_symbol.is_type=true;
772  compound_symbol.type=type;
773  compound_symbol.location=type.source_location();
774 
776 
777  std::string typestr = type2name(compound_symbol.type, *this);
778  compound_symbol.base_name = "#anon#" + typestr;
779  compound_symbol.name="tag-#anon#"+typestr;
780  identifier=compound_symbol.name;
781 
782  // We might already have the same anonymous union/struct,
783  // and this is simply ok. Note that the C standard treats
784  // these as different types.
785  if(symbol_table.symbols.find(identifier)==symbol_table.symbols.end())
786  {
787  symbolt *new_symbol;
788  move_symbol(compound_symbol, new_symbol);
789  }
790  }
791  else
792  {
793  identifier=type.find(ID_tag).get(ID_identifier);
794 
795  // does it exist already?
796  symbol_tablet::symbolst::const_iterator s_it=
797  symbol_table.symbols.find(identifier);
798 
799  if(s_it==symbol_table.symbols.end())
800  {
801  // no, add new symbol
802  irep_idt base_name=type.find(ID_tag).get(ID_C_base_name);
803  type.remove(ID_tag);
804  type.set(ID_tag, base_name);
805 
806  symbolt compound_symbol;
807  compound_symbol.is_type=true;
808  compound_symbol.name=identifier;
809  compound_symbol.base_name=base_name;
810  compound_symbol.type=type;
811  compound_symbol.location=type.source_location();
812  compound_symbol.pretty_name=id2string(type.id())+" "+id2string(base_name);
813 
814  typet new_type=compound_symbol.type;
815 
816  // mark as incomplete
817  to_struct_union_type(compound_symbol.type).make_incomplete();
818 
819  symbolt *new_symbol;
820  move_symbol(compound_symbol, new_symbol);
821 
822  if(have_body)
823  {
825 
826  new_symbol->type.swap(new_type);
827  }
828  }
829  else
830  {
831  // yes, it exists already
832  if(
833  s_it->second.type.id() == type.id() &&
834  to_struct_union_type(s_it->second.type).is_incomplete())
835  {
836  // Maybe we got a body now.
837  if(have_body)
838  {
839  irep_idt base_name=type.find(ID_tag).get(ID_C_base_name);
840  type.remove(ID_tag);
841  type.set(ID_tag, base_name);
842 
844  symbol_table.get_writeable_ref(s_it->first).type.swap(type);
845  }
846  }
847  else if(have_body)
848  {
850  error() << "redefinition of body of '" << s_it->second.pretty_name
851  << "'" << eom;
852  throw 0;
853  }
854  }
855  }
856 
857  typet tag_type;
858 
859  if(type.id() == ID_union)
860  tag_type = union_tag_typet(identifier);
861  else if(type.id() == ID_struct)
862  tag_type = struct_tag_typet(identifier);
863  else
864  UNREACHABLE;
865 
866  tag_type.add_source_location() = type.source_location();
867  type.swap(tag_type);
868 
869  original_qualifiers.write(type);
870 }
871 
873  struct_union_typet &type)
874 {
875  struct_union_typet::componentst &components=type.components();
876 
877  struct_union_typet::componentst old_components;
878  old_components.swap(components);
879 
880  // We get these as declarations!
881  for(auto &decl : old_components)
882  {
883  // the arguments are member declarations or static assertions
884  assert(decl.id()==ID_declaration);
885 
886  ansi_c_declarationt &declaration=
887  to_ansi_c_declaration(static_cast<exprt &>(decl));
888 
889  if(declaration.get_is_static_assert())
890  {
891  struct_union_typet::componentt new_component;
892  new_component.id(ID_static_assert);
893  new_component.add_source_location()=declaration.source_location();
894  new_component.operands().swap(declaration.operands());
895  assert(new_component.operands().size()==2);
896  components.push_back(new_component);
897  }
898  else
899  {
900  // do first half of type
901  typecheck_type(declaration.type());
903 
904  for(const auto &declarator : declaration.declarators())
905  {
906  struct_union_typet::componentt new_component(
907  declarator.get_base_name(), declaration.full_type(declarator));
908 
909  // There may be a declarator, which we use as location for
910  // the component. Otherwise, use location of the declaration.
911  const source_locationt source_location =
912  declarator.get_name().empty() ? declaration.source_location()
913  : declarator.source_location();
914 
915  new_component.add_source_location() = source_location;
916  new_component.set_pretty_name(declarator.get_base_name());
917 
918  typecheck_type(new_component.type());
919 
920  if(!is_complete_type(new_component.type()) &&
921  (new_component.type().id()!=ID_array ||
922  !to_array_type(new_component.type()).is_incomplete()))
923  {
924  error().source_location = source_location;
925  error() << "incomplete type not permitted here" << eom;
926  throw 0;
927  }
928 
929  components.push_back(new_component);
930  }
931  }
932  }
933 
934  unsigned anon_member_counter=0;
935 
936  // scan for anonymous members, and name them
937  for(auto &member : components)
938  {
939  if(!member.get_name().empty())
940  continue;
941 
942  member.set_name("$anon"+std::to_string(anon_member_counter++));
943  member.set_anonymous(true);
944  }
945 
946  // scan for duplicate members
947 
948  {
949  std::unordered_set<irep_idt> members;
950 
951  for(const auto &c : components)
952  {
953  if(!members.insert(c.get_name()).second)
954  {
955  error().source_location = c.source_location();
956  error() << "duplicate member '" << c.get_name() << '\'' << eom;
957  throw 0;
958  }
959  }
960  }
961 
962  // We allow an incomplete (C99) array as _last_ member!
963  // Zero-length is allowed everywhere.
964 
965  if(type.id()==ID_struct ||
966  type.id()==ID_union)
967  {
968  for(struct_union_typet::componentst::iterator
969  it=components.begin();
970  it!=components.end();
971  it++)
972  {
973  typet &c_type=it->type();
974 
975  if(c_type.id()==ID_array &&
976  to_array_type(c_type).is_incomplete())
977  {
978  // needs to be last member
979  if(type.id()==ID_struct && it!=--components.end())
980  {
981  error().source_location=it->source_location();
982  error() << "flexible struct member must be last member" << eom;
983  throw 0;
984  }
985 
986  // make it zero-length
987  c_type.id(ID_array);
988  c_type.set(ID_size, from_integer(0, index_type()));
989  }
990  }
991  }
992 
993  // We may add some minimal padding inside and at
994  // the end of structs and
995  // as additional member for unions.
996 
997  if(type.id()==ID_struct)
998  add_padding(to_struct_type(type), *this);
999  else if(type.id()==ID_union)
1000  add_padding(to_union_type(type), *this);
1001 
1002  // Now remove zero-width bit-fields, these are just
1003  // for adjusting alignment.
1004  for(struct_typet::componentst::iterator
1005  it=components.begin();
1006  it!=components.end();
1007  ) // blank
1008  {
1009  if(it->type().id()==ID_c_bit_field &&
1010  to_c_bit_field_type(it->type()).get_width()==0)
1011  it=components.erase(it);
1012  else
1013  it++;
1014  }
1015 
1016  // finally, check _Static_assert inside the compound
1017  for(struct_union_typet::componentst::iterator
1018  it=components.begin();
1019  it!=components.end();
1020  ) // no it++
1021  {
1022  if(it->id()==ID_static_assert)
1023  {
1024  exprt &assertion = to_binary_expr(*it).op0();
1025  typecheck_expr(assertion);
1027  assertion = typecast_exprt(assertion, bool_typet());
1028  make_constant(assertion);
1029 
1030  if(assertion.is_false())
1031  {
1032  error().source_location=it->source_location();
1033  error() << "failed _Static_assert" << eom;
1034  throw 0;
1035  }
1036  else if(!assertion.is_true())
1037  {
1038  // should warn/complain
1039  }
1040 
1041  it=components.erase(it);
1042  }
1043  else
1044  it++;
1045  }
1046 }
1047 
1049  const mp_integer &min_value,
1050  const mp_integer &max_value) const
1051 {
1053  {
1054  return signed_int_type();
1055  }
1056  else
1057  {
1058  // enum constants are at least 'int', but may be made larger.
1059  // 'Packing' has no influence.
1060  if(max_value<(mp_integer(1)<<(config.ansi_c.int_width-1)) &&
1061  min_value>=-(mp_integer(1)<<(config.ansi_c.int_width-1)))
1062  return signed_int_type();
1063  else if(max_value<(mp_integer(1)<<config.ansi_c.int_width) &&
1064  min_value>=0)
1065  return unsigned_int_type();
1066  else if(max_value<(mp_integer(1)<<config.ansi_c.long_int_width) &&
1067  min_value>=0)
1068  return unsigned_long_int_type();
1069  else if(max_value<(mp_integer(1)<<config.ansi_c.long_long_int_width) &&
1070  min_value>=0)
1071  return unsigned_long_long_int_type();
1072  else if(max_value<(mp_integer(1)<<(config.ansi_c.long_int_width-1)) &&
1073  min_value>=-(mp_integer(1)<<(config.ansi_c.long_int_width-1)))
1074  return signed_long_int_type();
1075  else
1076  return signed_long_long_int_type();
1077  }
1078 }
1079 
1081  const mp_integer &min_value,
1082  const mp_integer &max_value,
1083  bool is_packed) const
1084 {
1086  {
1087  return signed_int_type();
1088  }
1089  else
1090  {
1091  if(min_value<0)
1092  {
1093  // We'll want a signed type.
1094 
1095  if(is_packed)
1096  {
1097  // If packed, there are smaller options.
1098  if(max_value<(mp_integer(1)<<(config.ansi_c.char_width-1)) &&
1099  min_value>=-(mp_integer(1)<<(config.ansi_c.char_width-1)))
1100  return signed_char_type();
1101  else if(max_value<(mp_integer(1)<<(config.ansi_c.short_int_width-1)) &&
1102  min_value>=-(mp_integer(1)<<(config.ansi_c.short_int_width-1)))
1103  return signed_short_int_type();
1104  }
1105 
1106  if(max_value<(mp_integer(1)<<(config.ansi_c.int_width-1)) &&
1107  min_value>=-(mp_integer(1)<<(config.ansi_c.int_width-1)))
1108  return signed_int_type();
1109  else if(max_value<(mp_integer(1)<<(config.ansi_c.long_int_width-1)) &&
1110  min_value>=-(mp_integer(1)<<(config.ansi_c.long_int_width-1)))
1111  return signed_long_int_type();
1112  else
1113  return signed_long_long_int_type();
1114  }
1115  else
1116  {
1117  // We'll want an unsigned type.
1118 
1119  if(is_packed)
1120  {
1121  // If packed, there are smaller options.
1122  if(max_value<(mp_integer(1)<<config.ansi_c.char_width))
1123  return unsigned_char_type();
1124  else if(max_value<(mp_integer(1)<<config.ansi_c.short_int_width))
1125  return unsigned_short_int_type();
1126  }
1127 
1128  if(max_value<(mp_integer(1)<<config.ansi_c.int_width))
1129  return unsigned_int_type();
1130  else if(max_value<(mp_integer(1)<<config.ansi_c.long_int_width))
1131  return unsigned_long_int_type();
1132  else
1133  return unsigned_long_long_int_type();
1134  }
1135  }
1136 }
1137 
1139 {
1140  // These come with the declarations
1141  // of the enum constants as operands.
1142 
1143  exprt &as_expr=static_cast<exprt &>(static_cast<irept &>(type));
1144  source_locationt source_location=type.source_location();
1145 
1146  // We allow empty enums in the grammar to get better
1147  // error messages.
1148  if(as_expr.operands().empty())
1149  {
1150  error().source_location=source_location;
1151  error() << "empty enum" << eom;
1152  throw 0;
1153  }
1154 
1155  // enums start at zero;
1156  // we also track min and max to find a nice base type
1157  mp_integer value=0, min_value=0, max_value=0;
1158 
1159  std::list<c_enum_typet::c_enum_membert> enum_members;
1160 
1161  // We need to determine a width, and a signedness
1162  // to obtain an 'underlying type'.
1163  // We just do int, but gcc might pick smaller widths
1164  // if the type is marked as 'packed'.
1165  // gcc/clang may also pick a larger width. Visual Studio doesn't.
1166 
1167  for(auto &op : as_expr.operands())
1168  {
1169  ansi_c_declarationt &declaration=to_ansi_c_declaration(op);
1170  exprt &v=declaration.declarator().value();
1171 
1172  if(v.is_not_nil()) // value given?
1173  {
1174  exprt tmp_v=v;
1175  typecheck_expr(tmp_v);
1176  add_rounding_mode(tmp_v);
1177  simplify(tmp_v, *this);
1178  if(tmp_v.is_true())
1179  value=1;
1180  else if(tmp_v.is_false())
1181  value=0;
1182  else if(
1183  tmp_v.id() == ID_constant &&
1184  !to_integer(to_constant_expr(tmp_v), value))
1185  {
1186  }
1187  else
1188  {
1190  error() << "enum is not a constant" << eom;
1191  throw 0;
1192  }
1193  }
1194 
1195  if(value<min_value)
1196  min_value=value;
1197  if(value>max_value)
1198  max_value=value;
1199 
1200  typet constant_type=
1201  enum_constant_type(min_value, max_value);
1202 
1203  v=from_integer(value, constant_type);
1204 
1205  declaration.type()=constant_type;
1206  typecheck_declaration(declaration);
1207 
1208  irep_idt base_name=
1209  declaration.declarator().get_base_name();
1210 
1211  irep_idt identifier=
1212  declaration.declarator().get_name();
1213 
1214  // store
1216  member.set_identifier(identifier);
1217  member.set_base_name(base_name);
1218  // Note: The value will be correctly set to a bv type when we know
1219  // the width of the bitvector
1220  member.set_value(integer2string(value));
1221  enum_members.push_back(member);
1222 
1223  // produce value for next constant
1224  ++value;
1225  }
1226 
1227  // Remove these now; we add them to the
1228  // c_enum symbol later.
1229  as_expr.operands().clear();
1230 
1231  bool is_packed=type.get_bool(ID_C_packed);
1232 
1233  // We use a subtype to store the underlying type.
1234  bitvector_typet underlying_type =
1235  enum_underlying_type(min_value, max_value, is_packed);
1236 
1237  // Get the width to make the values have a bitvector type
1238  std::size_t width = underlying_type.get_width();
1239  for(auto &member : enum_members)
1240  {
1241  // Note: This is inefficient as it first turns integers to strings
1242  // and then turns them back to bvrep
1243  auto value = string2integer(id2string(member.get_value()));
1244  member.set_value(integer2bvrep(value, width));
1245  }
1246 
1247  // tag?
1248  if(type.find(ID_tag).is_nil())
1249  {
1250  // None, it's anonymous. We generate a tag.
1251  std::string anon_identifier="#anon_enum";
1252 
1253  for(const auto &member : enum_members)
1254  {
1255  anon_identifier+='$';
1256  anon_identifier+=id2string(member.get_base_name());
1257  anon_identifier+='=';
1258  anon_identifier+=id2string(member.get_value());
1259  }
1260 
1261  if(is_packed)
1262  anon_identifier+="#packed";
1263 
1264  type.add(ID_tag).set(ID_identifier, anon_identifier);
1265  }
1266 
1267  irept &tag=type.add(ID_tag);
1268  irep_idt base_name=tag.get(ID_C_base_name);
1269  irep_idt identifier=tag.get(ID_identifier);
1270 
1271  // Put into symbol table
1272  symbolt enum_tag_symbol;
1273 
1274  enum_tag_symbol.is_type=true;
1275  enum_tag_symbol.type=type;
1276  enum_tag_symbol.location=source_location;
1277  enum_tag_symbol.is_file_local=true;
1278  enum_tag_symbol.base_name=base_name;
1279  enum_tag_symbol.name=identifier;
1280 
1281  // throw in the enum members as 'body'
1282  irept::subt &body=enum_tag_symbol.type.add(ID_body).get_sub();
1283 
1284  for(const auto &member : enum_members)
1285  body.push_back(member);
1286 
1287  enum_tag_symbol.type.subtype()=underlying_type;
1288 
1289  // is it in the symbol table already?
1290  symbol_tablet::symbolst::const_iterator s_it=
1291  symbol_table.symbols.find(identifier);
1292 
1293  if(s_it!=symbol_table.symbols.end())
1294  {
1295  // Yes.
1296  const symbolt &symbol=s_it->second;
1297 
1298  if(symbol.type.id() != ID_c_enum)
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  if(to_c_enum_type(symbol.type).is_incomplete())
1306  {
1307  // Ok, overwrite the type in the symbol table.
1308  // This gives us the members and the subtype.
1309  symbol_table.get_writeable_ref(symbol.name).type=enum_tag_symbol.type;
1310  }
1311  else
1312  {
1313  // We might already have the same anonymous enum, and this is
1314  // simply ok. Note that the C standard treats these as
1315  // different types.
1316  if(!base_name.empty())
1317  {
1319  error() << "redeclaration of enum tag" << eom;
1320  throw 0;
1321  }
1322  }
1323  }
1324  else
1325  {
1326  symbolt *new_symbol;
1327  move_symbol(enum_tag_symbol, new_symbol);
1328  }
1329 
1330  // We produce a c_enum_tag as the resulting type.
1331  type.id(ID_c_enum_tag);
1332  type.remove(ID_tag);
1333  type.set(ID_identifier, identifier);
1334 }
1335 
1337 {
1338  // It's just a tag.
1339 
1340  if(type.find(ID_tag).is_nil())
1341  {
1343  error() << "anonymous enum tag without members" << eom;
1344  throw 0;
1345  }
1346 
1347  source_locationt source_location=type.source_location();
1348 
1349  irept &tag=type.add(ID_tag);
1350  irep_idt base_name=tag.get(ID_C_base_name);
1351  irep_idt identifier=tag.get(ID_identifier);
1352 
1353  // is it in the symbol table?
1354  symbol_tablet::symbolst::const_iterator s_it=
1355  symbol_table.symbols.find(identifier);
1356 
1357  if(s_it!=symbol_table.symbols.end())
1358  {
1359  // Yes.
1360  const symbolt &symbol=s_it->second;
1361 
1362  if(symbol.type.id() != ID_c_enum)
1363  {
1364  error().source_location=source_location;
1365  error() << "use of tag that does not match previous declaration" << eom;
1366  throw 0;
1367  }
1368  }
1369  else
1370  {
1371  // no, add it as an incomplete c_enum
1372  c_enum_typet new_type(signed_int_type()); // default subtype
1373  new_type.add(ID_tag)=tag;
1374  new_type.make_incomplete();
1375 
1376  symbolt enum_tag_symbol;
1377 
1378  enum_tag_symbol.is_type=true;
1379  enum_tag_symbol.type=new_type;
1380  enum_tag_symbol.location=source_location;
1381  enum_tag_symbol.is_file_local=true;
1382  enum_tag_symbol.base_name=base_name;
1383  enum_tag_symbol.name=identifier;
1384 
1385  symbolt *new_symbol;
1386  move_symbol(enum_tag_symbol, new_symbol);
1387  }
1388 
1389  // Clean up resulting type
1390  type.remove(ID_tag);
1391  type.set_identifier(identifier);
1392 }
1393 
1395 {
1396  typecheck_type(type.subtype());
1397 
1398  mp_integer i;
1399 
1400  {
1401  exprt &width_expr=static_cast<exprt &>(type.add(ID_size));
1402 
1403  typecheck_expr(width_expr);
1404  make_constant_index(width_expr);
1405 
1406  if(to_integer(to_constant_expr(width_expr), i))
1407  {
1409  error() << "failed to convert bit field width" << eom;
1410  throw 0;
1411  }
1412 
1413  if(i<0)
1414  {
1416  error() << "bit field width is negative" << eom;
1417  throw 0;
1418  }
1419 
1420  type.set_width(numeric_cast_v<std::size_t>(i));
1421  type.remove(ID_size);
1422  }
1423 
1424  const typet &subtype = type.subtype();
1425 
1426  std::size_t sub_width=0;
1427 
1428  if(subtype.id()==ID_bool)
1429  {
1430  // This is the 'proper' bool.
1431  sub_width=1;
1432  }
1433  else if(subtype.id()==ID_signedbv ||
1434  subtype.id()==ID_unsignedbv ||
1435  subtype.id()==ID_c_bool)
1436  {
1437  sub_width=to_bitvector_type(subtype).get_width();
1438  }
1439  else if(subtype.id()==ID_c_enum_tag)
1440  {
1441  // These point to an enum, which has a sub-subtype,
1442  // which may be smaller or larger than int, and we thus have
1443  // to check.
1444  const auto &c_enum_type =
1446 
1447  if(c_enum_type.is_incomplete())
1448  {
1450  error() << "bit field has incomplete enum type" << eom;
1451  throw 0;
1452  }
1453 
1454  sub_width = to_bitvector_type(c_enum_type.subtype()).get_width();
1455  }
1456  else
1457  {
1459  error() << "bit field with non-integer type: "
1460  << to_string(subtype) << eom;
1461  throw 0;
1462  }
1463 
1464  if(i>sub_width)
1465  {
1467  error() << "bit field (" << i
1468  << " bits) larger than type (" << sub_width << " bits)"
1469  << eom;
1470  throw 0;
1471  }
1472 }
1473 
1475 {
1476  // save location
1477  source_locationt source_location=type.source_location();
1478 
1479  // retain the qualifiers as is
1480  c_qualifierst c_qualifiers;
1481  c_qualifiers.read(type);
1482 
1483  const auto &as_expr = (const exprt &)type;
1484 
1485  if(!as_expr.has_operands())
1486  {
1487  typet t=static_cast<const typet &>(type.find(ID_type_arg));
1488  typecheck_type(t);
1489  type.swap(t);
1490  }
1491  else
1492  {
1493  exprt expr = to_unary_expr(as_expr).op();
1494  typecheck_expr(expr);
1495 
1496  // undo an implicit address-of
1497  if(expr.id()==ID_address_of &&
1498  expr.get_bool(ID_C_implicit))
1499  {
1500  expr = to_address_of_expr(expr).object();
1501  }
1502 
1503  type.swap(expr.type());
1504  }
1505 
1506  type.add_source_location()=source_location;
1507  c_qualifiers.write(type);
1508 }
1509 
1511 {
1512  const irep_idt &identifier = to_typedef_type(type).get_identifier();
1513 
1514  symbol_tablet::symbolst::const_iterator s_it =
1515  symbol_table.symbols.find(identifier);
1516 
1517  if(s_it == symbol_table.symbols.end())
1518  {
1520  error() << "typedef symbol '" << identifier << "' not found" << eom;
1521  throw 0;
1522  }
1523 
1524  const symbolt &symbol = s_it->second;
1525 
1526  if(!symbol.is_type)
1527  {
1529  error() << "expected type symbol for typedef" << eom;
1530  throw 0;
1531  }
1532 
1533  // overwrite, but preserve (add) any qualifiers and other flags
1534 
1535  c_qualifierst c_qualifiers(type);
1536  bool is_packed = type.get_bool(ID_C_packed);
1537  irept alignment = type.find(ID_C_alignment);
1538 
1539  c_qualifiers += c_qualifierst(symbol.type);
1540  type = symbol.type;
1541  c_qualifiers.write(type);
1542 
1543  if(is_packed)
1544  type.set(ID_C_packed, true);
1545  if(alignment.is_not_nil())
1546  type.set(ID_C_alignment, alignment);
1547 
1548  // CPROVER extensions
1549  if(symbol.base_name == CPROVER_PREFIX "rational")
1550  {
1551  type=rational_typet();
1552  }
1553  else if(symbol.base_name == CPROVER_PREFIX "integer")
1554  {
1555  type=integer_typet();
1556  }
1557 }
1558 
1560 {
1561  if(type.id()==ID_array)
1562  {
1563  source_locationt source_location=type.source_location();
1564  type=pointer_type(type.subtype());
1565  type.add_source_location()=source_location;
1566  }
1567  else if(type.id()==ID_code)
1568  {
1569  // see ISO/IEC 9899:1999 page 199 clause 8,
1570  // may be hidden in typedef
1571  source_locationt source_location=type.source_location();
1572  type=pointer_type(type);
1573  type.add_source_location()=source_location;
1574  }
1575  else if(type.id()==ID_KnR)
1576  {
1577  // any KnR args without type yet?
1578  type=signed_int_type(); // the default is integer!
1579  // no source location
1580  }
1581 }
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
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:2050
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:2824
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:320
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:1048
c_typecheck_base.h
fresh_symbol.h
irept::pretty
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:488
ansi_c_convert_type.h
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:54
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
already_typechecked_typet
Definition: c_typecheck_base.h:297
irept::find
const irept & find(const irep_namet &name) const
Definition: irep.cpp:103
code_declt
A codet representing the declaration of a local variable.
Definition: std_code.h:405
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:1080
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
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:283
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:1394
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:237
to_already_typechecked_type
already_typechecked_typet & to_already_typechecked_type(typet &type)
Definition: c_typecheck_base.h:324
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:3448
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
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:395
messaget::error
mstreamt & error() const
Definition: message.h:385
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:2852
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
messaget::mstreamt::source_location
source_locationt source_location
Definition: message.h:244
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:79
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:315
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:1336
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
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:3469
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:1510
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:1474
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:249
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:310
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:39
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:181
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:304
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
c_typecheck_baset::typecheck_c_enum_type
virtual void typecheck_c_enum_type(typet &type)
Definition: c_typecheck_type.cpp:1138
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:257
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:2042
size_type
unsignedbv_typet size_type()
Definition: c_types.cpp:58
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:298
c_typecheck_baset::typecheck_code_type
virtual void typecheck_code_type(code_typet &type)
Definition: c_typecheck_type.cpp:421
binary_exprt::op1
exprt & op1()
Definition: expr.h:104
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:252
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:872
configt::ansi_ct::long_int_width
std::size_t long_int_width
Definition: config.h:32
binary_exprt::op0
exprt & op0()
Definition: expr.h:101
validation_modet::INVARIANT
@ INVARIANT
c_typecheck_baset::make_index_type
virtual void make_index_type(exprt &expr)
Definition: c_typecheck_expr.cpp:1212
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:1559
padding.h
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:3968
integer2string
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:106