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