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