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