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