cprover
c_typecheck_base.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: ANSI-C Conversion / Type Checking
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "c_typecheck_base.h"
13 
14 #include <util/c_types.h>
15 #include <util/config.h>
16 #include <util/invariant.h>
17 #include <util/prefix.h>
18 #include <util/std_types.h>
19 
20 #include "c_storage_spec.h"
21 #include "expr2c.h"
22 #include "type2name.h"
23 
24 std::string c_typecheck_baset::to_string(const exprt &expr)
25 {
26  return expr2c(expr, *this);
27 }
28 
29 std::string c_typecheck_baset::to_string(const typet &type)
30 {
31  return type2c(type, *this);
32 }
33 
34 void c_typecheck_baset::move_symbol(symbolt &symbol, symbolt *&new_symbol)
35 {
36  symbol.mode=mode;
37  symbol.module=module;
38 
39  if(symbol_table.move(symbol, new_symbol))
40  {
42  error() << "failed to move symbol '" << symbol.name << "' into symbol table"
43  << eom;
44  throw 0;
45  }
46 }
47 
49 {
50  bool is_function=symbol.type.id()==ID_code;
51 
52  const typet &final_type=follow(symbol.type);
53 
54  // set a few flags
55  symbol.is_lvalue=!symbol.is_type && !symbol.is_macro;
56 
57  irep_idt root_name=symbol.base_name;
58  irep_idt new_name=symbol.name;
59 
60  if(symbol.is_file_local)
61  {
62  // file-local stuff -- stays as is
63  // collisions are resolved during linking
64  }
65  else if(symbol.is_extern && !is_function)
66  {
67  // variables marked as "extern" go into the global namespace
68  // and have static lifetime
69  new_name=root_name;
70  symbol.is_static_lifetime=true;
71 
72  if(symbol.value.is_not_nil())
73  {
74  // According to the C standard this should be an error, but at least some
75  // versions of Visual Studio insist to use this in their C library, and
76  // GCC just warns as well.
78  warning() << "`extern' symbol should not have an initializer" << eom;
79  }
80  }
81  else if(!is_function && symbol.value.id()==ID_code)
82  {
84  error() << "only functions can have a function body" << eom;
85  throw 0;
86  }
87 
88  // set the pretty name
89  if(symbol.is_type && final_type.id() == ID_struct)
90  {
91  symbol.pretty_name="struct "+id2string(symbol.base_name);
92  }
93  else if(symbol.is_type && final_type.id() == ID_union)
94  {
95  symbol.pretty_name="union "+id2string(symbol.base_name);
96  }
97  else if(symbol.is_type && final_type.id() == ID_c_enum)
98  {
99  symbol.pretty_name="enum "+id2string(symbol.base_name);
100  }
101  else
102  {
103  symbol.pretty_name=new_name;
104  }
105 
106  // see if we have it already
107  symbol_tablet::symbolst::const_iterator old_it=
108  symbol_table.symbols.find(symbol.name);
109 
110  if(old_it==symbol_table.symbols.end())
111  {
112  // just put into symbol_table
113  symbolt *new_symbol;
114  move_symbol(symbol, new_symbol);
115 
116  typecheck_new_symbol(*new_symbol);
117  }
118  else
119  {
120  if(old_it->second.is_type!=symbol.is_type)
121  {
122  error().source_location=symbol.location;
123  error() << "redeclaration of '" << symbol.display_name()
124  << "' as a different kind of symbol" << eom;
125  throw 0;
126  }
127 
128  symbolt &existing_symbol = symbol_table.get_writeable_ref(symbol.name);
129  if(symbol.is_type)
130  typecheck_redefinition_type(existing_symbol, symbol);
131  else
132  typecheck_redefinition_non_type(existing_symbol, symbol);
133  }
134 }
135 
137 {
138  if(symbol.is_parameter)
140 
141  // check initializer, if needed
142 
143  if(symbol.type.id()==ID_code)
144  {
145  if(symbol.value.is_not_nil() &&
146  !symbol.is_macro)
147  {
148  typecheck_function_body(symbol);
149  }
150  else
151  {
152  // we don't need the identifiers
153  for(auto &parameter : to_code_type(symbol.type).parameters())
154  parameter.set_identifier(irep_idt());
155  }
156  }
157  else if(!symbol.is_macro)
158  {
159  // check the initializer
160  do_initializer(symbol);
161  }
162 }
163 
165  symbolt &old_symbol,
166  symbolt &new_symbol)
167 {
168  const typet &final_old=follow(old_symbol.type);
169  const typet &final_new=follow(new_symbol.type);
170 
171  // see if we had something incomplete before
172  if(
173  (final_old.id() == ID_struct &&
174  to_struct_type(final_old).is_incomplete()) ||
175  (final_old.id() == ID_union && to_union_type(final_old).is_incomplete()) ||
176  (final_old.id() == ID_c_enum && to_c_enum_type(final_old).is_incomplete()))
177  {
178  // is the new one complete?
179  if(
180  final_new.id() == final_old.id() &&
181  ((final_new.id() == ID_struct &&
182  !to_struct_type(final_new).is_incomplete()) ||
183  (final_new.id() == ID_union &&
184  !to_union_type(final_new).is_incomplete()) ||
185  (final_new.id() == ID_c_enum &&
186  !to_c_enum_type(final_new).is_incomplete())))
187  {
188  // overwrite location
189  old_symbol.location=new_symbol.location;
190 
191  // move body
192  old_symbol.type.swap(new_symbol.type);
193  }
194  else if(new_symbol.type.id()==old_symbol.type.id())
195  return; // ignore
196  else
197  {
198  error().source_location=new_symbol.location;
199  error() << "conflicting definition of type symbol '"
200  << new_symbol.display_name() << '\'' << eom;
201  throw 0;
202  }
203  }
204  else
205  {
206  // see if new one is just a tag
207  if(
208  (final_new.id() == ID_struct &&
209  to_struct_type(final_new).is_incomplete()) ||
210  (final_new.id() == ID_union &&
211  to_union_type(final_new).is_incomplete()) ||
212  (final_new.id() == ID_c_enum &&
213  to_c_enum_type(final_new).is_incomplete()))
214  {
215  if(final_old.id() == final_new.id())
216  {
217  // just ignore silently
218  }
219  else
220  {
221  // arg! new tag type
222  error().source_location=new_symbol.location;
223  error() << "conflicting definition of tag symbol '"
224  << new_symbol.display_name() << '\'' << eom;
225  throw 0;
226  }
227  }
229  final_new.id()==ID_c_enum && final_old.id()==ID_c_enum)
230  {
231  // under Windows, ignore this silently;
232  // MSC doesn't think this is a problem, but GCC complains.
233  }
235  final_new.id()==ID_pointer && final_old.id()==ID_pointer &&
236  follow(final_new.subtype()).id()==ID_c_enum &&
237  follow(final_old.subtype()).id()==ID_c_enum)
238  {
239  // under Windows, ignore this silently;
240  // MSC doesn't think this is a problem, but GCC complains.
241  }
242  else
243  {
244  // see if it changed
245  if(follow(new_symbol.type)!=follow(old_symbol.type))
246  {
247  error().source_location=new_symbol.location;
248  error() << "type symbol '" << new_symbol.display_name()
249  << "' defined twice:\n"
250  << "Original: " << to_string(old_symbol.type) << "\n"
251  << " New: " << to_string(new_symbol.type) << eom;
252  throw 0;
253  }
254  }
255  }
256 }
257 
259  symbolt &old_symbol,
260  symbolt &new_symbol)
261 {
262  const typet &final_old=follow(old_symbol.type);
263  const typet &initial_new=follow(new_symbol.type);
264 
265  if(final_old.id()==ID_array &&
266  to_array_type(final_old).size().is_not_nil() &&
267  initial_new.id()==ID_array &&
268  to_array_type(initial_new).size().is_nil() &&
269  final_old.subtype()==initial_new.subtype())
270  {
271  // this is ok, just use old type
272  new_symbol.type=old_symbol.type;
273  }
274  else if(final_old.id()==ID_array &&
275  to_array_type(final_old).size().is_nil() &&
276  initial_new.id()==ID_array &&
277  to_array_type(initial_new).size().is_not_nil() &&
278  final_old.subtype()==initial_new.subtype())
279  {
280  // update the type to enable the use of sizeof(x) on the
281  // right-hand side of a definition of x
282  old_symbol.type=new_symbol.type;
283  }
284 
285  // do initializer, this may change the type
286  if(new_symbol.type.id() != ID_code && !new_symbol.is_macro)
287  do_initializer(new_symbol);
288 
289  const typet &final_new=follow(new_symbol.type);
290 
291  // K&R stuff?
292  if(old_symbol.type.id()==ID_KnR)
293  {
294  // check the type
295  if(final_new.id()==ID_code)
296  {
297  error().source_location=new_symbol.location;
298  error() << "function type not allowed for K&R function parameter"
299  << eom;
300  throw 0;
301  }
302 
303  // fix up old symbol -- we now got the type
304  old_symbol.type=new_symbol.type;
305  return;
306  }
307 
308  if(final_new.id()==ID_code)
309  {
310  if(final_old.id()!=ID_code)
311  {
312  error().source_location=new_symbol.location;
313  error() << "error: function symbol '" << new_symbol.display_name()
314  << "' redefined with a different type:\n"
315  << "Original: " << to_string(old_symbol.type) << "\n"
316  << " New: " << to_string(new_symbol.type) << eom;
317  throw 0;
318  }
319 
320  code_typet &old_ct=to_code_type(old_symbol.type);
321  code_typet &new_ct=to_code_type(new_symbol.type);
322 
323  const bool inlined = old_ct.get_inlined() || new_ct.get_inlined();
324 
325  if(old_ct.has_ellipsis() && !new_ct.has_ellipsis())
326  old_ct=new_ct;
327  else if(!old_ct.has_ellipsis() && new_ct.has_ellipsis())
328  new_ct=old_ct;
329 
330  if(inlined)
331  {
332  old_ct.set_inlined(true);
333  new_ct.set_inlined(true);
334  }
335 
336  // do body
337 
338  if(new_symbol.value.is_not_nil())
339  {
340  if(old_symbol.value.is_not_nil())
341  {
342  // gcc allows re-definition if the first
343  // definition is marked as "extern inline"
344 
345  if(
346  old_ct.get_inlined() &&
351  {
352  // overwrite "extern inline" properties
353  old_symbol.is_extern=new_symbol.is_extern;
354  old_symbol.is_file_local=new_symbol.is_file_local;
355 
356  // remove parameter declarations to avoid conflicts
357  for(const auto &old_parameter : old_ct.parameters())
358  {
359  const irep_idt &identifier = old_parameter.get_identifier();
360 
361  symbol_tablet::symbolst::const_iterator p_s_it=
362  symbol_table.symbols.find(identifier);
363  if(p_s_it!=symbol_table.symbols.end())
364  symbol_table.erase(p_s_it);
365  }
366  }
367  else
368  {
369  error().source_location=new_symbol.location;
370  error() << "function body '" << new_symbol.display_name()
371  << "' defined twice" << eom;
372  throw 0;
373  }
374  }
375  else if(inlined)
376  {
377  // preserve "extern inline" properties
378  old_symbol.is_extern=new_symbol.is_extern;
379  old_symbol.is_file_local=new_symbol.is_file_local;
380  }
381  else if(new_symbol.is_weak)
382  {
383  // weak symbols
384  old_symbol.is_weak=true;
385  }
386 
387  if(new_symbol.is_macro)
388  old_symbol.is_macro=true;
389  else
390  typecheck_function_body(new_symbol);
391 
392  // overwrite location
393  old_symbol.location=new_symbol.location;
394 
395  // move body
396  old_symbol.value.swap(new_symbol.value);
397 
398  // overwrite type (because of parameter names)
399  old_symbol.type=new_symbol.type;
400  }
401 
402  return;
403  }
404 
405  if(final_old!=final_new)
406  {
407  if(final_old.id()==ID_array &&
408  to_array_type(final_old).size().is_nil() &&
409  final_new.id()==ID_array &&
410  to_array_type(final_new).size().is_not_nil() &&
411  final_old.subtype()==final_new.subtype())
412  {
413  old_symbol.type=new_symbol.type;
414  }
415  else if(
416  final_old.id() == ID_pointer && final_old.subtype().id() == ID_code &&
417  to_code_type(final_old.subtype()).has_ellipsis() &&
418  final_new.id() == ID_pointer && final_new.subtype().id() == ID_code)
419  {
420  // to allow
421  // int (*f) ();
422  // int (*f) (int)=0;
423  old_symbol.type=new_symbol.type;
424  }
425  else if(
426  final_old.id() == ID_pointer && final_old.subtype().id() == ID_code &&
427  final_new.id() == ID_pointer && final_new.subtype().id() == ID_code &&
428  to_code_type(final_new.subtype()).has_ellipsis())
429  {
430  // to allow
431  // int (*f) (int)=0;
432  // int (*f) ();
433  }
434  else
435  {
436  error().source_location=new_symbol.location;
437  error() << "symbol '" << new_symbol.display_name()
438  << "' redefined with a different type:\n"
439  << "Original: " << to_string(old_symbol.type) << "\n"
440  << " New: " << to_string(new_symbol.type) << eom;
441  throw 0;
442  }
443  }
444  else // finals are equal
445  {
446  }
447 
448  // do value
449  if(new_symbol.value.is_not_nil())
450  {
451  // see if we already have one
452  if(old_symbol.value.is_not_nil())
453  {
454  if(new_symbol.value.get_bool(ID_C_zero_initializer))
455  {
456  // do nothing
457  }
458  else if(old_symbol.value.get_bool(ID_C_zero_initializer))
459  {
460  old_symbol.value=new_symbol.value;
461  old_symbol.type=new_symbol.type;
462  }
463  else
464  {
465  if(
466  new_symbol.is_macro && final_new.id() == ID_c_enum &&
467  old_symbol.value.is_constant() && new_symbol.value.is_constant() &&
468  old_symbol.value.get(ID_value) == new_symbol.value.get(ID_value))
469  {
470  // ignore
471  }
472  else
473  {
475  warning() << "symbol '" << new_symbol.display_name()
476  << "' already has an initial value" << eom;
477  }
478  }
479  }
480  else
481  {
482  old_symbol.value=new_symbol.value;
483  old_symbol.type=new_symbol.type;
484  old_symbol.is_macro=new_symbol.is_macro;
485  }
486  }
487 
488  // take care of some flags
489  if(old_symbol.is_extern && !new_symbol.is_extern)
490  old_symbol.location=new_symbol.location;
491 
492  old_symbol.is_extern=old_symbol.is_extern && new_symbol.is_extern;
493 
494  // We should likely check is_volatile and
495  // is_thread_local for consistency. GCC complains if these
496  // mismatch.
497 }
498 
500 {
501  code_typet &code_type=to_code_type(symbol.type);
502 
503  assert(symbol.value.is_not_nil());
504 
505  // reset labels
506  labels_used.clear();
507  labels_defined.clear();
508 
509  // fix type
510  symbol.value.type()=code_type;
511 
512  // set return type
513  return_type=code_type.return_type();
514 
515  unsigned anon_counter=0;
516 
517  // Add the parameter declarations into the symbol table.
518  for(auto &p : code_type.parameters())
519  {
520  // may be anonymous
521  if(p.get_base_name().empty())
522  {
523  irep_idt base_name="#anon"+std::to_string(anon_counter++);
524  p.set_base_name(base_name);
525  }
526 
527  // produce identifier
528  irep_idt base_name = p.get_base_name();
529  irep_idt identifier=id2string(symbol.name)+"::"+id2string(base_name);
530 
531  p.set_identifier(identifier);
532 
533  parameter_symbolt p_symbol;
534 
535  p_symbol.type = p.type();
536  p_symbol.name=identifier;
537  p_symbol.base_name=base_name;
538  p_symbol.location = p.source_location();
539 
540  symbolt *new_p_symbol;
541  move_symbol(p_symbol, new_p_symbol);
542  }
543 
544  // typecheck the body code
545  typecheck_code(to_code(symbol.value));
546 
547  // check the labels
548  for(const auto &label : labels_used)
549  {
550  if(labels_defined.find(label.first) == labels_defined.end())
551  {
552  error().source_location = label.second;
553  error() << "branching label '" << label.first
554  << "' is not defined in function" << eom;
555  throw 0;
556  }
557  }
558 }
559 
561  const irep_idt &asm_label,
562  symbolt &symbol)
563 {
564  const irep_idt orig_name=symbol.name;
565 
566  // restrict renaming to functions and global variables;
567  // procedure-local ones would require fixing the scope, as we
568  // do for parameters below
569  if(!asm_label.empty() &&
570  !symbol.is_type &&
571  (symbol.type.id()==ID_code || symbol.is_static_lifetime))
572  {
573  symbol.name=asm_label;
574  symbol.base_name=asm_label;
575  }
576 
577  if(symbol.name!=orig_name)
578  {
579  if(!asm_label_map.insert(
580  std::make_pair(orig_name, asm_label)).second)
581  {
582  if(asm_label_map[orig_name]!=asm_label)
583  {
584  error().source_location=symbol.location;
585  error() << "error: replacing asm renaming "
586  << asm_label_map[orig_name] << " by "
587  << asm_label << eom;
588  throw 0;
589  }
590  }
591  }
592  else if(asm_label.empty())
593  {
594  asm_label_mapt::const_iterator entry=
595  asm_label_map.find(symbol.name);
596  if(entry!=asm_label_map.end())
597  {
598  symbol.name=entry->second;
599  symbol.base_name=entry->second;
600  }
601  }
602 
603  if(symbol.name!=orig_name &&
604  symbol.type.id()==ID_code &&
605  symbol.value.is_not_nil() && !symbol.is_macro)
606  {
607  const code_typet &code_type=to_code_type(symbol.type);
608 
609  for(const auto &p : code_type.parameters())
610  {
611  const irep_idt &p_bn = p.get_base_name();
612  if(p_bn.empty())
613  continue;
614 
615  irep_idt p_id=id2string(orig_name)+"::"+id2string(p_bn);
616  irep_idt p_new_id=id2string(symbol.name)+"::"+id2string(p_bn);
617 
618  if(!asm_label_map.insert(
619  std::make_pair(p_id, p_new_id)).second)
620  assert(asm_label_map[p_id]==p_new_id);
621  }
622  }
623 }
624 
626  ansi_c_declarationt &declaration)
627 {
628  if(declaration.get_is_static_assert())
629  {
630  auto &static_assert_expr = to_binary_expr(declaration);
631  typecheck_expr(static_assert_expr.op0());
632  typecheck_expr(static_assert_expr.op1());
633  }
634  else
635  {
636  // get storage spec
637  c_storage_spect c_storage_spec(declaration.type());
638 
639  // first typecheck the type of the declaration
640  typecheck_type(declaration.type());
641 
642  // mark as 'already typechecked'
644 
645  irept contract;
646 
647  {
648  exprt spec_assigns = declaration.spec_assigns();
649  contract.add(ID_C_spec_assigns).swap(spec_assigns);
650 
651  exprt spec_ensures = declaration.spec_ensures();
652  contract.add(ID_C_spec_ensures).swap(spec_ensures);
653 
654  exprt spec_requires = declaration.spec_requires();
655  contract.add(ID_C_spec_requires).swap(spec_requires);
656  }
657 
658  // Now do declarators, if any.
659  for(auto &declarator : declaration.declarators())
660  {
661  c_storage_spect full_spec(declaration.full_type(declarator));
662  full_spec|=c_storage_spec;
663 
664  declaration.set_is_inline(full_spec.is_inline);
665  declaration.set_is_static(full_spec.is_static);
666  declaration.set_is_extern(full_spec.is_extern);
667  declaration.set_is_thread_local(full_spec.is_thread_local);
668  declaration.set_is_register(full_spec.is_register);
669  declaration.set_is_typedef(full_spec.is_typedef);
670  declaration.set_is_weak(full_spec.is_weak);
671  declaration.set_is_used(full_spec.is_used);
672 
673  symbolt symbol;
674  declaration.to_symbol(declarator, symbol);
675  current_symbol=symbol;
676 
677  // now check other half of type
678  typecheck_type(symbol.type);
679 
680  if(!full_spec.alias.empty())
681  {
682  if(symbol.value.is_not_nil())
683  {
684  error().source_location=symbol.location;
685  error() << "alias attribute cannot be used with a body"
686  << eom;
687  throw 0;
688  }
689 
690  // alias function need not have been declared yet, thus
691  // can't lookup
692  // also cater for renaming/placement in sections
693  const auto &renaming_entry = asm_label_map.find(full_spec.alias);
694  if(renaming_entry == asm_label_map.end())
695  symbol.value = symbol_exprt::typeless(full_spec.alias);
696  else
697  symbol.value = symbol_exprt::typeless(renaming_entry->second);
698  symbol.is_macro=true;
699  }
700 
701  if(full_spec.section.empty())
702  apply_asm_label(full_spec.asm_label, symbol);
703  else
704  {
705  // section name is not empty, do a bit of parsing
706  std::string asm_name = id2string(full_spec.section);
707 
708  if(asm_name[0] == '.')
709  {
710  std::string::size_type primary_section = asm_name.find('.', 1);
711 
712  if(primary_section != std::string::npos)
713  asm_name.resize(primary_section);
714  }
715 
716  asm_name += "$$";
717 
718  if(!full_spec.asm_label.empty())
719  asm_name+=id2string(full_spec.asm_label);
720  else
721  asm_name+=id2string(symbol.name);
722 
723  apply_asm_label(asm_name, symbol);
724  }
725 
726  irep_idt identifier=symbol.name;
727  declarator.set_name(identifier);
728 
729  // If the declarator is for a function definition, typecheck it.
730  if(can_cast_type<code_typet>(declarator.type()))
731  {
732  typecheck_assigns(to_code_type(declarator.type()), contract);
733  }
734 
735  typecheck_symbol(symbol);
736 
737  // add code contract (if any); we typecheck this after the
738  // function body done above, so as to have parameter symbols
739  // available
740  symbolt &new_symbol = symbol_table.get_writeable_ref(identifier);
741 
743  static_cast<codet &>(contract), ID_C_spec_assigns);
744  typecheck_spec_expr(static_cast<codet &>(contract), ID_C_spec_requires);
745 
746  typet ret_type = void_type();
747  if(new_symbol.type.id()==ID_code)
748  ret_type=to_code_type(new_symbol.type).return_type();
749  assert(parameter_map.empty());
750  if(ret_type.id()!=ID_empty)
751  parameter_map[CPROVER_PREFIX "return_value"] = ret_type;
752  typecheck_spec_expr(static_cast<codet &>(contract), ID_C_spec_ensures);
753  parameter_map.clear();
754 
755  irept assigns_to_add = contract.find(ID_C_spec_assigns);
756  if(assigns_to_add.is_not_nil())
757  new_symbol.type.add(ID_C_spec_assigns) = assigns_to_add;
758  irept requires_to_add = contract.find(ID_C_spec_requires);
759  if(requires_to_add.is_not_nil())
760  new_symbol.type.add(ID_C_spec_requires) = requires_to_add;
761  irept ensures_to_add = contract.find(ID_C_spec_ensures);
762  if(ensures_to_add.is_not_nil())
763  new_symbol.type.add(ID_C_spec_ensures) = ensures_to_add;
764  }
765  }
766 }
c_typecheck_baset::do_initializer
virtual void do_initializer(exprt &initializer, const typet &type, bool force_constant)
Definition: c_typecheck_initializer.cpp:25
c_typecheck_baset::typecheck_assigns_exprs
virtual void typecheck_assigns_exprs(codet &code, const irep_idt &spec)
Definition: c_typecheck_code.cpp:858
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
c_typecheck_baset::typecheck_new_symbol
void typecheck_new_symbol(symbolt &symbol)
Definition: c_typecheck_base.cpp:136
code_typet::has_ellipsis
bool has_ellipsis() const
Definition: std_types.h:813
ansi_c_declarationt::spec_requires
const exprt & spec_requires() const
Definition: ansi_c_declaration.h:253
typet::subtype
const typet & subtype() const
Definition: type.h:47
ansi_c_declarationt::declarators
const declaratorst & declarators() const
Definition: ansi_c_declaration.h:217
c_typecheck_baset::current_symbol
symbolt current_symbol
Definition: c_typecheck_base.h:70
symbolt::is_macro
bool is_macro
Definition: symbol.h:61
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:303
symbolt::display_name
const irep_idt & display_name() const
Return language specific display name if present.
Definition: symbol.h:55
to_c_enum_type
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
Definition: std_types.h:681
typet
The type of an expression, extends irept.
Definition: type.h:29
c_typecheck_base.h
ANSI-C Language Type Checking.
c_typecheck_baset::typecheck_declaration
void typecheck_declaration(ansi_c_declarationt &)
Definition: c_typecheck_base.cpp:625
c_typecheck_baset::to_string
virtual std::string to_string(const exprt &expr)
Definition: c_typecheck_base.cpp:24
c_storage_spec.h
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
configt::ansi_ct::os
ost os
Definition: config.h:80
irept::add
irept & add(const irep_namet &name)
Definition: irep.cpp:113
symbol_exprt::typeless
static symbol_exprt typeless(const irep_idt &id)
Generate a symbol_exprt without a proper type.
Definition: std_expr.h:101
configt::ansi_ct::flavourt::VISUAL_STUDIO
@ VISUAL_STUDIO
type2name.h
Type Naming for C.
irept::find
const irept & find(const irep_namet &name) const
Definition: irep.cpp:103
prefix.h
invariant.h
c_storage_spect::section
irep_idt section
Definition: c_storage_spec.h:52
c_storage_spect::is_extern
bool is_extern
Definition: c_storage_spec.h:44
exprt
Base class for all expressions.
Definition: expr.h:53
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
irep_idt
dstringt irep_idt
Definition: irep.h:32
c_typecheck_baset::move_symbol
void move_symbol(symbolt &symbol, symbolt *&new_symbol)
Definition: c_typecheck_base.cpp:34
c_typecheck_baset::typecheck_type
virtual void typecheck_type(typet &type)
Definition: c_typecheck_type.cpp:31
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:55
messaget::eom
static eomt eom
Definition: message.h:297
c_typecheck_baset::typecheck_spec_expr
virtual void typecheck_spec_expr(codet &code, const irep_idt &spec)
Definition: c_typecheck_code.cpp:797
c_storage_spect::is_register
bool is_register
Definition: c_storage_spec.h:44
configt::ansi_c
struct configt::ansi_ct ansi_c
void_type
empty_typet void_type()
Definition: c_types.cpp:253
configt::ansi_ct::flavourt::ARM
@ ARM
ansi_c_declarationt::get_is_static_assert
bool get_is_static_assert() const
Definition: ansi_c_declaration.h:179
configt::ansi_ct::flavourt::CLANG
@ CLANG
ansi_c_declarationt::set_is_typedef
void set_is_typedef(bool is_typedef)
Definition: ansi_c_declaration.h:84
symbolt::pretty_name
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:52
to_code
const codet & to_code(const exprt &expr)
Definition: std_code.h:155
to_binary_expr
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:678
c_typecheck_baset::typecheck_redefinition_non_type
void typecheck_redefinition_non_type(symbolt &old_symbol, symbolt &new_symbol)
Definition: c_typecheck_base.cpp:258
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
irept::get_bool
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:64
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:402
c_typecheck_baset::module
const irep_idt module
Definition: c_typecheck_base.h:68
can_cast_type< code_typet >
bool can_cast_type< code_typet >(const typet &type)
Check whether a reference to a typet is a code_typet.
Definition: std_types.h:933
c_typecheck_baset::asm_label_map
asm_label_mapt asm_label_map
Definition: c_typecheck_base.h:276
c_typecheck_baset::typecheck_assigns
virtual void typecheck_assigns(const code_typet &function_declarator, const irept &spec)
Definition: c_typecheck_code.cpp:808
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:946
symbolt::mode
irep_idt mode
Language mode.
Definition: symbol.h:49
c_storage_spect::is_inline
bool is_inline
Definition: c_storage_spec.h:45
messaget::error
mstreamt & error() const
Definition: message.h:399
ansi_c_declarationt::set_is_register
void set_is_register(bool is_register)
Definition: ansi_c_declaration.h:144
c_typecheck_baset::typecheck_function_body
void typecheck_function_body(symbolt &symbol)
Definition: c_typecheck_base.cpp:499
symbol_table_baset::get_writeable_ref
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
Definition: symbol_table_base.h:121
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
ansi_c_declarationt::set_is_weak
void set_is_weak(bool is_weak)
Definition: ansi_c_declaration.h:194
messaget::mstreamt::source_location
source_locationt source_location
Definition: message.h:247
expr2c.h
expr2c
std::string expr2c(const exprt &expr, const namespacet &ns, const expr2c_configurationt &configuration)
Definition: expr2c.cpp:3878
c_typecheck_baset::typecheck_symbol
void typecheck_symbol(symbolt &symbol)
Definition: c_typecheck_base.cpp:48
exprt::find_source_location
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
Definition: expr.cpp:231
std_types.h
Pre-defined types.
code_typet::set_inlined
void set_inlined(bool value)
Definition: std_types.h:872
ansi_c_declarationt::to_symbol
void to_symbol(const ansi_c_declaratort &, symbolt &symbol) const
Definition: ansi_c_declaration.cpp:126
c_storage_spect::asm_label
irep_idt asm_label
Definition: c_storage_spec.h:51
c_typecheck_baset::symbol_table
symbol_tablet & symbol_table
Definition: c_typecheck_base.h:67
c_typecheck_baset::typecheck_code
virtual void typecheck_code(codet &code)
Definition: c_typecheck_code.cpp:26
irept::swap
void swap(irept &irep)
Definition: irep.h:463
code_typet
Base type of functions.
Definition: std_types.h:736
symbolt::is_parameter
bool is_parameter
Definition: symbol.h:67
configt::ansi_ct::ost::OS_WIN
@ OS_WIN
irept::id
const irep_idt & id() const
Definition: irep.h:418
c_storage_spect::alias
irep_idt alias
Definition: c_storage_spec.h:48
dstringt::empty
bool empty() const
Definition: dstring.h:88
c_typecheck_baset::typecheck_redefinition_type
void typecheck_redefinition_type(symbolt &old_symbol, symbolt &new_symbol)
Definition: c_typecheck_base.cpp:164
c_storage_spect::is_used
bool is_used
Definition: c_storage_spec.h:45
c_storage_spect
Definition: c_storage_spec.h:16
ansi_c_declarationt::spec_assigns
const exprt & spec_assigns() const
Definition: ansi_c_declaration.h:248
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:857
c_typecheck_baset::parameter_map
id_type_mapt parameter_map
Definition: c_typecheck_base.h:73
c_typecheck_baset::labels_used
std::map< irep_idt, source_locationt > labels_used
Definition: c_typecheck_base.h:160
symbol_tablet::move
virtual bool move(symbolt &symbol, symbolt *&new_symbol) override
Move a symbol into the symbol table.
Definition: symbol_table.cpp:69
c_typecheck_baset::typecheck_expr
virtual void typecheck_expr(exprt &expr)
Definition: c_typecheck_expr.cpp:41
config
configt config
Definition: config.cpp:24
ansi_c_declarationt::spec_ensures
const exprt & spec_ensures() const
Definition: ansi_c_declaration.h:258
ansi_c_declarationt::set_is_thread_local
void set_is_thread_local(bool is_thread_local)
Definition: ansi_c_declaration.h:154
configt::ansi_ct::mode
flavourt mode
Definition: config.h:116
symbolt::value
exprt value
Initial value of symbol.
Definition: symbol.h:34
ansi_c_declarationt
Definition: ansi_c_declaration.h:73
symbolt::is_extern
bool is_extern
Definition: symbol.h:66
ansi_c_declarationt::set_is_static
void set_is_static(bool is_static)
Definition: ansi_c_declaration.h:104
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:51
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
symbolt::location
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
c_typecheck_baset::labels_defined
std::map< irep_idt, source_locationt > labels_defined
Definition: c_typecheck_base.h:160
symbolt
Symbol table entry.
Definition: symbol.h:28
symbol_table_baset::symbols
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Definition: symbol_table_base.h:30
exprt::is_constant
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:85
ansi_c_declarationt::set_is_extern
void set_is_extern(bool is_extern)
Definition: ansi_c_declaration.h:174
symbolt::is_type
bool is_type
Definition: symbol.h:61
c_typecheck_baset::return_type
typet return_type
Definition: c_typecheck_base.h:157
CPROVER_PREFIX
#define CPROVER_PREFIX
Definition: cprover_prefix.h:14
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1011
ansi_c_declarationt::full_type
typet full_type(const ansi_c_declaratort &) const
Definition: ansi_c_declaration.cpp:94
symbolt::is_static_lifetime
bool is_static_lifetime
Definition: symbol.h:65
c_storage_spect::is_weak
bool is_weak
Definition: c_storage_spec.h:45
code_typet::get_inlined
bool get_inlined() const
Definition: std_types.h:867
config.h
already_typechecked_typet::make_already_typechecked
static void make_already_typechecked(typet &type)
Definition: c_typecheck_base.h:309
configt::ansi_ct::flavourt::GCC
@ GCC
code_typet::return_type
const typet & return_type() const
Definition: std_types.h:847
irept
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:394
symbol_tablet::erase
virtual void erase(const symbolst::const_iterator &entry) override
Remove a symbol from the symbol table.
Definition: symbol_table.cpp:92
c_storage_spect::is_thread_local
bool is_thread_local
Definition: c_storage_spec.h:45
c_storage_spect::is_static
bool is_static
Definition: c_storage_spec.h:44
symbolt::is_file_local
bool is_file_local
Definition: symbol.h:66
symbolt::is_lvalue
bool is_lvalue
Definition: symbol.h:66
type2c
std::string type2c(const typet &type, const namespacet &ns, const expr2c_configurationt &configuration)
Definition: expr2c.cpp:3894
parameter_symbolt
Symbol table entry of function parameterThis is a symbol generated as part of type checking.
Definition: symbol.h:184
to_union_type
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition: std_types.h:422
size_type
unsignedbv_typet size_type()
Definition: c_types.cpp:58
symbolt::module
irep_idt module
Name of module the symbol belongs to.
Definition: symbol.h:43
c_storage_spect::is_typedef
bool is_typedef
Definition: c_storage_spec.h:44
messaget::warning
mstreamt & warning() const
Definition: message.h:404
c_typecheck_baset::mode
const irep_idt mode
Definition: c_typecheck_base.h:69
c_types.h
symbolt::is_weak
bool is_weak
Definition: symbol.h:67
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
c_typecheck_baset::apply_asm_label
void apply_asm_label(const irep_idt &asm_label, symbolt &symbol)
Definition: c_typecheck_base.cpp:560
ansi_c_declarationt::set_is_inline
void set_is_inline(bool is_inline)
Definition: ansi_c_declaration.h:164
ansi_c_declarationt::set_is_used
void set_is_used(bool is_used)
Definition: ansi_c_declaration.h:204
c_typecheck_baset::adjust_function_parameter
virtual void adjust_function_parameter(typet &type) const
Definition: c_typecheck_type.cpp:1621
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:35