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