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