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