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