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