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