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(old_symbol.type.get_bool(ID_C_inlined) &&
340  {
341  // overwrite "extern inline" properties
342  old_symbol.is_extern=new_symbol.is_extern;
343  old_symbol.is_file_local=new_symbol.is_file_local;
344 
345  // remove parameter declarations to avoid conflicts
346  const code_typet::parameterst &old_p=old_ct.parameters();
347  for(code_typet::parameterst::const_iterator
348  p_it=old_p.begin();
349  p_it!=old_p.end();
350  p_it++)
351  {
352  const irep_idt &identifier=p_it->get_identifier();
353 
354  symbol_tablet::symbolst::const_iterator p_s_it=
355  symbol_table.symbols.find(identifier);
356  if(p_s_it!=symbol_table.symbols.end())
357  symbol_table.erase(p_s_it);
358  }
359  }
360  else
361  {
362  error().source_location=new_symbol.location;
363  error() << "function body `" << new_symbol.display_name()
364  << "' defined twice" << eom;
365  throw 0;
366  }
367  }
368  else if(inlined)
369  {
370  // preserve "extern inline" properties
371  old_symbol.is_extern=new_symbol.is_extern;
372  old_symbol.is_file_local=new_symbol.is_file_local;
373  }
374  else if(new_symbol.is_weak)
375  {
376  // weak symbols
377  old_symbol.is_weak=true;
378  }
379 
380  if(new_symbol.is_macro)
381  old_symbol.is_macro=true;
382  else
383  typecheck_function_body(new_symbol);
384 
385  // overwrite location
386  old_symbol.location=new_symbol.location;
387 
388  // move body
389  old_symbol.value.swap(new_symbol.value);
390 
391  // overwrite type (because of parameter names)
392  old_symbol.type=new_symbol.type;
393  }
394 
395  return;
396  }
397 
398  if(final_old!=final_new)
399  {
400  if(final_old.id()==ID_array &&
401  to_array_type(final_old).size().is_nil() &&
402  final_new.id()==ID_array &&
403  to_array_type(final_new).size().is_not_nil() &&
404  final_old.subtype()==final_new.subtype())
405  {
406  // we don't do symbol types for arrays anymore
407  PRECONDITION(old_symbol.type.id()!=ID_symbol);
408  old_symbol.type=new_symbol.type;
409  }
410  else if((final_old.id()==ID_incomplete_c_enum ||
411  final_old.id()==ID_c_enum) &&
412  (final_new.id()==ID_incomplete_c_enum ||
413  final_new.id()==ID_c_enum))
414  {
415  // this is ok for now
416  }
417  else if(final_old.id()==ID_pointer &&
418  follow(final_old).subtype().id()==ID_code &&
419  to_code_type(follow(final_old).subtype()).has_ellipsis() &&
420  final_new.id()==ID_pointer &&
421  follow(final_new).subtype().id()==ID_code)
422  {
423  // to allow
424  // int (*f) ();
425  // int (*f) (int)=0;
426  old_symbol.type=new_symbol.type;
427  }
428  else if(final_old.id()==ID_pointer &&
429  follow(final_old).subtype().id()==ID_code &&
430  final_new.id()==ID_pointer &&
431  follow(final_new).subtype().id()==ID_code &&
432  to_code_type(follow(final_new).subtype()).has_ellipsis())
433  {
434  // to allow
435  // int (*f) (int)=0;
436  // int (*f) ();
437  }
438  else
439  {
440  error().source_location=new_symbol.location;
441  error() << "symbol `" << new_symbol.display_name()
442  << "' redefined with a different type:\n"
443  << "Original: " << to_string(old_symbol.type) << "\n"
444  << " New: " << to_string(new_symbol.type) << eom;
445  throw 0;
446  }
447  }
448  else // finals are equal
449  {
450  }
451 
452  // do value
453  if(new_symbol.value.is_not_nil())
454  {
455  // see if we already have one
456  if(old_symbol.value.is_not_nil())
457  {
458  if(new_symbol.value.get_bool(ID_C_zero_initializer))
459  {
460  // do nothing
461  }
462  else if(old_symbol.value.get_bool(ID_C_zero_initializer))
463  {
464  old_symbol.value=new_symbol.value;
465  old_symbol.type=new_symbol.type;
466  }
467  else
468  {
469  if(new_symbol.is_macro &&
470  (final_new.id()==ID_incomplete_c_enum ||
471  final_new.id()==ID_c_enum) &&
472  old_symbol.value.is_constant() &&
473  new_symbol.value.is_constant() &&
474  old_symbol.value.get(ID_value)==new_symbol.value.get(ID_value))
475  {
476  // ignore
477  }
478  else
479  {
481  warning() << "symbol `" << new_symbol.display_name()
482  << "' already has an initial value" << eom;
483  }
484  }
485  }
486  else
487  {
488  old_symbol.value=new_symbol.value;
489  old_symbol.type=new_symbol.type;
490  old_symbol.is_macro=new_symbol.is_macro;
491  }
492  }
493 
494  // take care of some flags
495  if(old_symbol.is_extern && !new_symbol.is_extern)
496  old_symbol.location=new_symbol.location;
497 
498  old_symbol.is_extern=old_symbol.is_extern && new_symbol.is_extern;
499 
500  // We should likely check is_volatile and
501  // is_thread_local for consistency. GCC complains if these
502  // mismatch.
503 }
504 
506 {
507  code_typet &code_type=to_code_type(symbol.type);
508 
509  assert(symbol.value.is_not_nil());
510 
511  // reset labels
512  labels_used.clear();
513  labels_defined.clear();
514 
515  // fix type
516  symbol.value.type()=code_type;
517 
518  // set return type
519  return_type=code_type.return_type();
520 
521  unsigned anon_counter=0;
522 
523  // Add the parameter declarations into the symbol table.
524  code_typet::parameterst &parameters=code_type.parameters();
525  for(code_typet::parameterst::iterator
526  p_it=parameters.begin();
527  p_it!=parameters.end();
528  p_it++)
529  {
530  // may be anonymous
531  if(p_it->get_base_name().empty())
532  {
533  irep_idt base_name="#anon"+std::to_string(anon_counter++);
534  p_it->set_base_name(base_name);
535  }
536 
537  // produce identifier
538  irep_idt base_name=p_it->get_base_name();
539  irep_idt identifier=id2string(symbol.name)+"::"+id2string(base_name);
540 
541  p_it->set_identifier(identifier);
542 
543  parameter_symbolt p_symbol;
544 
545  p_symbol.type=p_it->type();
546  p_symbol.name=identifier;
547  p_symbol.base_name=base_name;
548  p_symbol.location=p_it->source_location();
549 
550  symbolt *new_p_symbol;
551  move_symbol(p_symbol, new_p_symbol);
552  }
553 
554  // typecheck the body code
555  typecheck_code(to_code(symbol.value));
556 
557  // special case for main()
558  if(symbol.name==ID_main)
559  add_argc_argv(symbol);
560 
561  // check the labels
562  for(std::map<irep_idt, source_locationt>::const_iterator
563  it=labels_used.begin(); it!=labels_used.end(); it++)
564  {
565  if(labels_defined.find(it->first)==labels_defined.end())
566  {
567  error().source_location=it->second;
568  error() << "branching label `" << it->first
569  << "' is not defined in function" << eom;
570  throw 0;
571  }
572  }
573 }
574 
576  const irep_idt &asm_label,
577  symbolt &symbol)
578 {
579  const irep_idt orig_name=symbol.name;
580 
581  // restrict renaming to functions and global variables;
582  // procedure-local ones would require fixing the scope, as we
583  // do for parameters below
584  if(!asm_label.empty() &&
585  !symbol.is_type &&
586  (symbol.type.id()==ID_code || symbol.is_static_lifetime))
587  {
588  symbol.name=asm_label;
589  symbol.base_name=asm_label;
590  }
591 
592  if(symbol.name!=orig_name)
593  {
594  if(!asm_label_map.insert(
595  std::make_pair(orig_name, asm_label)).second)
596  {
597  if(asm_label_map[orig_name]!=asm_label)
598  {
599  error().source_location=symbol.location;
600  error() << "error: replacing asm renaming "
601  << asm_label_map[orig_name] << " by "
602  << asm_label << eom;
603  throw 0;
604  }
605  }
606  }
607  else if(asm_label.empty())
608  {
609  asm_label_mapt::const_iterator entry=
610  asm_label_map.find(symbol.name);
611  if(entry!=asm_label_map.end())
612  {
613  symbol.name=entry->second;
614  symbol.base_name=entry->second;
615  }
616  }
617 
618  if(symbol.name!=orig_name &&
619  symbol.type.id()==ID_code &&
620  symbol.value.is_not_nil() && !symbol.is_macro)
621  {
622  const code_typet &code_type=to_code_type(symbol.type);
623 
624  for(code_typet::parameterst::const_iterator
625  p_it=code_type.parameters().begin();
626  p_it!=code_type.parameters().end();
627  ++p_it)
628  {
629  const irep_idt &p_bn=p_it->get_base_name();
630  if(p_bn.empty())
631  continue;
632 
633  irep_idt p_id=id2string(orig_name)+"::"+id2string(p_bn);
634  irep_idt p_new_id=id2string(symbol.name)+"::"+id2string(p_bn);
635 
636  if(!asm_label_map.insert(
637  std::make_pair(p_id, p_new_id)).second)
638  assert(asm_label_map[p_id]==p_new_id);
639  }
640  }
641 }
642 
644  ansi_c_declarationt &declaration)
645 {
646  if(declaration.get_is_static_assert())
647  {
648  assert(declaration.operands().size()==2);
649  typecheck_expr(declaration.op0());
650  typecheck_expr(declaration.op1());
651  }
652  else
653  {
654  // get storage spec
655  c_storage_spect c_storage_spec(declaration.type());
656 
657  // first typecheck the type of the declaration
658  typecheck_type(declaration.type());
659 
660  // mark as 'already typechecked'
661  make_already_typechecked(declaration.type());
662 
663  codet contract;
664 
665  {
666  exprt spec_requires=
667  static_cast<const exprt&>(declaration.find(ID_C_spec_requires));
668  contract.add(ID_C_spec_requires).swap(spec_requires);
669 
670  exprt spec_ensures=
671  static_cast<const exprt&>(declaration.find(ID_C_spec_ensures));
672  contract.add(ID_C_spec_ensures).swap(spec_ensures);
673  }
674 
675  // Now do declarators, if any.
676  for(ansi_c_declarationt::declaratorst::iterator
677  d_it=declaration.declarators().begin();
678  d_it!=declaration.declarators().end();
679  d_it++)
680  {
681  c_storage_spect full_spec(declaration.full_type(*d_it));
682  full_spec|=c_storage_spec;
683 
684  declaration.set_is_inline(full_spec.is_inline);
685  declaration.set_is_static(full_spec.is_static);
686  declaration.set_is_extern(full_spec.is_extern);
687  declaration.set_is_thread_local(full_spec.is_thread_local);
688  declaration.set_is_register(full_spec.is_register);
689  declaration.set_is_typedef(full_spec.is_typedef);
690  declaration.set_is_weak(full_spec.is_weak);
691  declaration.set_is_used(full_spec.is_used);
692  declaration.set_is_always_inline(full_spec.is_always_inline);
693 
694  symbolt symbol;
695  declaration.to_symbol(*d_it, symbol);
696  current_symbol=symbol;
697 
698  // now check other half of type
699  typecheck_type(symbol.type);
700 
701  if(!full_spec.alias.empty())
702  {
703  if(symbol.value.is_not_nil())
704  {
705  error().source_location=symbol.location;
706  error() << "alias attribute cannot be used with a body"
707  << eom;
708  throw 0;
709  }
710 
711  // alias function need not have been declared yet, thus
712  // can't lookup
713  // also cater for renaming/placement in sections
714  const auto &renaming_entry = asm_label_map.find(full_spec.alias);
715  if(renaming_entry == asm_label_map.end())
716  symbol.value = symbol_exprt(full_spec.alias);
717  else
718  symbol.value = symbol_exprt(renaming_entry->second);
719  symbol.is_macro=true;
720  }
721 
722  if(full_spec.section.empty())
723  apply_asm_label(full_spec.asm_label, symbol);
724  else
725  {
726  // section name is not empty, do a bit of parsing
727  std::string asm_name = id2string(full_spec.section);
728 
729  if(asm_name[0] == '.')
730  {
731  std::string::size_type primary_section = asm_name.find('.', 1);
732 
733  if(primary_section != std::string::npos)
734  asm_name.resize(primary_section);
735  }
736 
737  asm_name += "$$";
738 
739  if(!full_spec.asm_label.empty())
740  asm_name+=id2string(full_spec.asm_label);
741  else
742  asm_name+=id2string(symbol.name);
743 
744  apply_asm_label(asm_name, symbol);
745  }
746 
747  irep_idt identifier=symbol.name;
748  d_it->set_name(identifier);
749 
750  typecheck_symbol(symbol);
751 
752  // add code contract (if any); we typecheck this after the
753  // function body done above, so as to have parameter symbols
754  // available
755  symbolt &new_symbol=*symbol_table.get_writeable(identifier);
756 
757  typecheck_spec_expr(contract, ID_C_spec_requires);
758 
759  typet ret_type=empty_typet();
760  if(new_symbol.type.id()==ID_code)
761  ret_type=to_code_type(new_symbol.type).return_type();
762  assert(parameter_map.empty());
763  if(ret_type.id()!=ID_empty)
764  parameter_map["__CPROVER_return_value"]=ret_type;
765  typecheck_spec_expr(contract, ID_C_spec_ensures);
766  parameter_map.clear();
767 
768  if(contract.find(ID_C_spec_requires).is_not_nil())
769  new_symbol.type.add(ID_C_spec_requires)=
770  contract.find(ID_C_spec_requires);
771  if(contract.find(ID_C_spec_ensures).is_not_nil())
772  new_symbol.type.add(ID_C_spec_ensures)=
773  contract.find(ID_C_spec_ensures);
774  }
775  }
776 }
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:102
const std::string & id2string(const irep_idt &d)
Definition: irep.h:43
bool is_not_nil() const
Definition: irep.h:103
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:987
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:189
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:106
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:230
std::string type2c(const typet &type, const namespacet &ns)
Definition: expr2c.cpp:3975
const exprt & size() const
Definition: std_types.h:1014
virtual void typecheck_expr(exprt &expr)
void set_is_always_inline(bool is_always_inline)
void set_is_register(bool is_register)
const typet & follow(const typet &) const
Definition: namespace.cpp:55
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:1045
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:3967
const irep_idt module
void typecheck_symbol(symbolt &symbol)
const std::string & id_string() const
Definition: irep.h:192
void swap(irept &irep)
Definition: irep.h:231
bool is_weak
Definition: symbol.h:68
const codet & to_code(const exprt &expr)
Definition: std_code.h:74
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:61
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:214
virtual void typecheck_code(codet &code)
bool is_lvalue
Definition: symbol.h:68