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