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