CBMC
cpp_typecheck.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: C++ Language Type Checking
4 
5 Author: Daniel Kroening, kroening@cs.cmu.edu
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_CPP_CPP_TYPECHECK_H
13 #define CPROVER_CPP_CPP_TYPECHECK_H
14 
15 #include <util/std_code_base.h>
16 
18 
19 #include "cpp_parse_tree.h"
20 #include "cpp_scopes.h"
21 #include "cpp_typecheck_resolve.h"
22 #include "template_map.h"
23 
24 #include <list>
25 #include <set>
26 #include <unordered_set>
27 
28 class pointer_typet;
29 class reference_typet;
30 
31 bool cpp_typecheck(
32  cpp_parse_treet &cpp_parse_tree,
33  symbol_table_baset &symbol_table,
34  const std::string &module,
35  message_handlert &message_handler);
36 
37 bool cpp_typecheck(
38  exprt &expr,
39  message_handlert &message_handler,
40  const namespacet &ns);
41 
43 {
44 public:
46  cpp_parse_treet &_cpp_parse_tree,
47  symbol_table_baset &_symbol_table,
48  const std::string &_module,
50 
52  cpp_parse_treet &_cpp_parse_tree,
53  symbol_table_baset &_symbol_table1,
54  const symbol_table_baset &_symbol_table2,
55  const std::string &_module,
57 
58  ~cpp_typecheckt() override
59  {
60  }
61 
62  void typecheck() override;
63 
64  // overload to use C++ syntax
65  std::string to_string(const typet &) override;
66  std::string to_string(const exprt &) override;
67 
68  friend class cpp_typecheck_resolvet;
70 
72  const cpp_namet &cpp_name,
74  const cpp_typecheck_fargst &fargs,
75  bool fail_with_exception=true)
76  {
77  cpp_typecheck_resolvet cpp_typecheck_resolve(*this);
78  return cpp_typecheck_resolve.resolve(
79  cpp_name, want, fargs, fail_with_exception);
80  }
81 
82  void typecheck_expr(exprt &) override;
83 
84  bool cpp_is_pod(const typet &type) const;
85 
86  std::optional<codet> cpp_constructor(
87  const source_locationt &source_location,
88  const exprt &object,
89  const exprt::operandst &operands);
90 
91 protected:
93 
96 
97  void convert(cpp_linkage_spect &);
99  void convert(cpp_usingt &);
100  void convert(cpp_itemt &);
101  void convert(cpp_declarationt &);
103  void convert(cpp_static_assertt &);
104 
105  void convert_initializer(symbolt &symbol);
106  void convert_function(symbolt &symbol);
107 
108  void convert_pmop(exprt &expr);
109 
111 
113  const cpp_declarationt &declaration,
114  const irep_idt &access,
115  struct_typet::componentst &components);
116 
117  //
118  // Templates
119  //
121  const template_typet &old_type,
122  template_typet &new_type);
123 
125 
127 
129  cpp_declarationt &declaration);
130 
132  cpp_declarationt &declaration);
133 
134  void typecheck_class_template(cpp_declarationt &declaration);
135 
137 
139 
140  std::string class_template_identifier(
141  const irep_idt &base_name,
142  const template_typet &template_type,
143  const cpp_template_args_non_tct &partial_specialization_args);
144 
145  std::string function_template_identifier(
146  const irep_idt &base_name,
147  const template_typet &template_type,
148  const typet &function_type);
149 
151  const source_locationt &source_location,
152  const symbolt &template_symbol,
153  const cpp_template_args_non_tct &template_args);
154 
155  // template instantiations
157  {
158  public:
162  };
163 
164  typedef std::list<instantiationt> instantiation_stackt;
166 
167  void show_instantiation_stack(std::ostream &);
168 
170  {
171  public:
173  instantiation_stackt &_instantiation_stack):
174  instantiation_stack(_instantiation_stack)
175  {
176  instantiation_stack.push_back(instantiationt());
177  }
178 
180  {
181  instantiation_stack.pop_back();
182  }
183 
184  private:
186  };
187 
189  const source_locationt &source_location,
190  const symbolt &template_symbol,
191  const cpp_template_args_tct &specialization_template_args,
192  const cpp_template_args_tct &full_template_args);
193 
195  const typet &type);
196 
198  const source_locationt &source_location,
199  const symbolt &symbol,
200  const cpp_template_args_tct &specialization_template_args,
201  const cpp_template_args_tct &full_template_args,
202  const typet &specialization = uninitialized_typet{});
203 
205  const source_locationt &source_location,
206  const struct_tag_typet &type);
207 
209  unsigned anon_counter;
210 
212 
213  std::string template_suffix(
214  const cpp_template_args_tct &template_args);
215 
217  cpp_scopet &template_scope,
218  const std::string &suffix);
219 
220  void
221  convert_parameters(const irep_idt &current_mode, code_typet &function_type);
222 
223  void convert_parameter(
224  const irep_idt &current_mode,
225  code_typet::parametert &parameter);
226 
227  //
228  // Misc
229  //
230 
231  void default_ctor(
232  const source_locationt &source_location,
233  const irep_idt &base_name,
234  cpp_declarationt &ctor) const;
235 
236  void default_cpctor(
237  const symbolt&, cpp_declarationt &cpctor) const;
238 
239  void default_assignop(
240  const symbolt &symbol, cpp_declarationt &cpctor);
241 
243  const symbolt &symbol, cpp_declaratort &declarator);
244 
245  void default_dtor(const symbolt &symb, cpp_declarationt &dtor);
246 
247  codet dtor(const symbolt &symb, const symbol_exprt &this_expr);
248 
250  const struct_typet::basest &bases,
251  const struct_typet::componentst &components,
252  const irept &initializers);
253 
256  const struct_union_typet &struct_union_type);
257 
259  const struct_union_typet &struct_union_type,
260  irept &initializers);
261 
262  bool find_cpctor(const symbolt &symbol)const;
263  bool find_assignop(const symbolt &symbol)const;
264  bool find_dtor(const symbolt &symbol)const;
265 
266  bool find_parent(
267  const symbolt &symb,
268  const irep_idt &base_name,
269  irep_idt &identifier);
270 
271  bool get_component(
272  const source_locationt &source_location,
273  const exprt &object,
274  const irep_idt &component_name,
275  exprt &member);
276 
277  void new_temporary(const source_locationt &source_location,
278  const typet &,
279  const exprt::operandst &ops,
280  exprt &temporary);
281 
282  void new_temporary(const source_locationt &source_location,
283  const typet &,
284  const exprt &op,
285  exprt &temporary);
286 
288  void do_not_typechecked();
289  void clean_up();
290 
291  void add_base_components(
292  const struct_typet &from,
293  const irep_idt &access,
294  struct_typet &to,
295  std::set<irep_idt> &bases,
296  std::set<irep_idt> &vbases,
297  bool is_virtual);
298 
299  bool cast_away_constness(const typet &t1,
300  const typet &t2) const;
301 
302  void do_virtual_table(const symbolt &symbol);
303 
304  // we need to be able to delay the typechecking
305  // of method bodies to handle methods with
306  // bodies in the class definition
308  {
309  public:
311  symbolt *_method_symbol,
312  const template_mapt &_template_map,
313  const instantiation_stackt &_instantiation_stack):
314  method_symbol(_method_symbol),
315  template_map(_template_map),
316  instantiation_stack(_instantiation_stack)
317  {
318  }
319 
323  };
324 
325  typedef std::list<method_bodyt> method_bodiest;
326  std::set<irep_idt> methods_seen;
328 
329  void add_method_body(symbolt *_method_symbol);
330 
331  bool builtin_factory(const irep_idt &) override;
332 
333  // types
334 
335  void typecheck_type(typet &) override;
336 
338  template_typet &type);
339 
341  void check_fixed_size_array(typet &type);
342  void typecheck_enum_type(typet &type);
343 
344  // determine the scope into which a tag goes
345  // (enums, structs, union, classes)
347  const irep_idt &_base_name,
348  bool has_body,
349  bool tag_only_declaration);
350 
352  const symbolt &symbol,
353  const cpp_declarationt &declaration,
354  cpp_declaratort &declarator,
355  struct_typet::componentst &components,
356  const irep_idt &access,
357  bool is_static,
358  bool is_typedef,
359  bool is_mutable);
360 
362  symbolt &symbol,
363  cpp_declarationt &cpp_declaration);
364 
366  void typecheck_compound_body(symbolt &symbol);
368  {
369  UNREACHABLE;
370  }
371  void typecheck_enum_body(symbolt &symbol);
374  void add_anonymous_members_to_scope(const symbolt &struct_union_symbol);
375 
377  irept &initializers,
378  const code_typet &type,
379  exprt &value);
380 
381  static bool has_const(const typet &type);
382  static bool has_volatile(const typet &type);
383  static bool has_auto(const typet &type);
384 
386  const symbolt &compound_symbol,
388  irept &initializers,
389  const typet &method_qualifier,
390  exprt &value);
391 
393  const symbolt &compound_symbol,
394  code_typet &method_type,
395  const typet &method_qualifier);
396 
397  // for function overloading
398  irep_idt function_identifier(const typet &type);
399 
400  void zero_initializer(
401  const exprt &object,
402  const typet &type,
403  const source_locationt &source_location,
404  exprt::operandst &ops);
405 
406  // code conversion
407  void typecheck_code(codet &) override;
408  void typecheck_try_catch(codet &);
410  void typecheck_decl(codet &) override;
411  void typecheck_block(code_blockt &) override;
412  void typecheck_ifthenelse(code_ifthenelset &) override;
413  void typecheck_while(code_whilet &) override;
414  void typecheck_switch(codet &) override;
415 
417 
418  std::optional<codet>
419  cpp_destructor(const source_locationt &source_location, const exprt &object);
420 
421  // expressions
423  void typecheck_expr_main(exprt &) override;
424  void typecheck_expr_member(exprt &) override;
425  void typecheck_expr_ptrmember(exprt &) override;
426  void typecheck_expr_throw(exprt &);
431  void typecheck_cast_expr(exprt &);
432  void typecheck_expr_trinary(if_exprt &) override;
433  void typecheck_expr_binary_arithmetic(exprt &) override;
436  void typecheck_expr_address_of(exprt &) override;
437  void typecheck_expr_dereference(exprt &) override;
438  void typecheck_expr_function_identifier(exprt &) override;
440  void typecheck_expr_this(exprt &);
441  void typecheck_expr_new(exprt &);
442  void typecheck_expr_sizeof(exprt &) override;
447  void typecheck_expr_typecast(exprt &) override;
448  void typecheck_expr_index(exprt &) override;
449  void typecheck_expr_rel(binary_relation_exprt &) override;
450  void typecheck_expr_comma(exprt &) override;
451 
452  void
454 
456  bool overloadable(const exprt &);
457 
459 
462 
464 
465 public:
466  //
467  // Type Conversions
468  //
469 
471  const exprt &expr, exprt &new_expr) const;
472 
474  const exprt &expr, exprt &new_expr) const;
475 
477  const exprt &expr, exprt &new_expr) const;
478 
480  const exprt &expr, const typet&, exprt &new_expr) const;
481 
483  const exprt &expr, exprt &new_expr) const;
484 
486  const exprt &expr, exprt &new_expr) const;
487 
489  const exprt &expr, const typet &type, exprt &new_expr) const;
490 
492  const exprt &expr, const typet &type, exprt &new_expr) const;
493 
495  const exprt &expr, const typet &type, exprt &new_expr) const;
496 
498  const exprt &expr, const typet &type, exprt &new_expr);
499 
501  const exprt &expr, const typet &type, exprt &new_expr);
502 
504  const exprt &expr, exprt &new_expr) const;
505 
507  const exprt &expr, const typet &type, exprt &new_expr, unsigned &rank);
508 
510  const exprt &expr, const typet &type, exprt &new_expr, unsigned &rank);
511 
512  bool reference_related(const exprt &expr, const reference_typet &type) const;
513 
515  const exprt &expr,
516  const reference_typet &type,
517  unsigned &rank) const;
518 
519  bool reference_binding(
520  exprt expr,
521  const reference_typet &type,
522  exprt &new_expr,
523  unsigned &rank);
524 
526  const exprt &expr, const typet &type, exprt &new_expr, unsigned &rank);
527 
529  const exprt &expr, const typet &type, unsigned &rank);
530 
532  const exprt &expr, const typet &type, exprt &new_expr);
533 
534  void reference_initializer(exprt &expr, const reference_typet &type);
535 
536  void implicit_typecast(exprt &expr, const typet &type) override;
537 
538  void get_bases(const struct_typet &type,
539  std::set<irep_idt> &set_bases) const;
540 
541  void get_virtual_bases(const struct_typet &type,
542  std::list<irep_idt> &vbases) const;
543 
544  bool subtype_typecast(
545  const struct_typet &from,
546  const struct_typet &to) const;
547 
548  void make_ptr_typecast(exprt &expr, const pointer_typet &dest_type);
549 
550  // the C++ typecasts
551 
552  bool const_typecast(
553  const exprt &expr,
554  const typet &type,
555  exprt &new_expr);
556 
557  bool dynamic_typecast(
558  const exprt &expr,
559  const typet &type,
560  exprt &new_expr);
561 
563  const exprt &expr,
564  const typet &type,
565  exprt &new_expr,
566  bool check_constantness=true);
567 
568  bool static_typecast(
569  const exprt &expr,
570  const typet &type,
571  exprt &new_expr,
572  bool check_constantness=true);
573 
574  bool contains_cpp_name(const exprt &);
575 
576 private:
577  typedef std::list<irep_idt> dynamic_initializationst;
579  bool disable_access_control; // Disable protect and private
580  std::unordered_set<irep_idt> deferred_typechecking;
582 };
583 
584 #endif // CPROVER_CPP_CPP_TYPECHECK_H
ANSI-C Language Type Checking.
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:762
A codet representing sequential composition of program statements.
Definition: std_code.h:130
codet representation of an if-then-else statement.
Definition: std_code.h:460
Base type of functions.
Definition: std_types.h:583
codet representing a while statement.
Definition: std_code.h:610
Data structure for representing an arbitrary statement in a program.
Definition: std_code_base.h:29
exprt resolve(const cpp_namet &cpp_name, const wantt want, const cpp_typecheck_fargst &fargs, bool fail_with_exception=true)
instantiation_stackt & instantiation_stack
instantiation_levelt(instantiation_stackt &_instantiation_stack)
cpp_template_args_tct full_template_args
source_locationt source_location
bool find_parent(const symbolt &symb, const irep_idt &base_name, irep_idt &identifier)
void default_assignop(const symbolt &symbol, cpp_declarationt &cpctor)
Generate declaration of the implicit default assignment operator.
bool reference_compatible(const exprt &expr, const reference_typet &type, unsigned &rank) const
Reference-compatible.
void typecheck_expr_typecast(exprt &) override
void typecheck_compound_body(symbolt &symbol)
void do_virtual_table(const symbolt &symbol)
void static_and_dynamic_initialization()
Initialization of static objects:
std::string template_suffix(const cpp_template_args_tct &template_args)
std::set< irep_idt > methods_seen
void typecheck_side_effect_assignment(side_effect_exprt &) override
bool implicit_conversion_sequence(const exprt &expr, const typet &type, exprt &new_expr, unsigned &rank)
implicit conversion sequence
bool standard_conversion_floating_point_conversion(const exprt &expr, const typet &type, exprt &new_expr) const
Floating-point conversion.
void put_compound_into_scope(const struct_union_typet::componentt &component)
std::string class_template_identifier(const irep_idt &base_name, const template_typet &template_type, const cpp_template_args_non_tct &partial_specialization_args)
void typecheck_type(typet &) override
void convert_anon_struct_union_member(const cpp_declarationt &declaration, const irep_idt &access, struct_typet::componentst &components)
void typecheck_switch(codet &) override
void explicit_typecast_ambiguity(exprt &)
void typecheck_compound_body(struct_union_typet &) override
instantiation_stackt instantiation_stack
void full_member_initialization(const struct_union_typet &struct_union_type, irept &initializers)
Build the full initialization list of the constructor.
bool contains_cpp_name(const exprt &)
void typecheck_decl(codet &) override
template_mapt template_map
bool reinterpret_typecast(const exprt &expr, const typet &type, exprt &new_expr, bool check_constantness=true)
std::string function_template_identifier(const irep_idt &base_name, const template_typet &template_type, const typet &function_type)
void do_not_typechecked()
void typecheck_enum_type(typet &type)
void convert_pmop(exprt &expr)
void typecheck_expr_sizeof(exprt &) override
void add_base_components(const struct_typet &from, const irep_idt &access, struct_typet &to, std::set< irep_idt > &bases, std::set< irep_idt > &vbases, bool is_virtual)
static bool has_const(const typet &type)
dynamic_initializationst dynamic_initializations
bool standard_conversion_boolean(const exprt &expr, exprt &new_expr) const
Boolean conversion.
void typecheck_code(codet &) override
std::list< method_bodyt > method_bodiest
void convert_template_declaration(cpp_declarationt &declaration)
bool standard_conversion_pointer(const exprt &expr, const typet &type, exprt &new_expr)
Pointer conversion.
void convert_function(symbolt &symbol)
void typecheck_expr_explicit_typecast(exprt &)
void typecheck_compound_declarator(const symbolt &symbol, const cpp_declarationt &declaration, cpp_declaratort &declarator, struct_typet::componentst &components, const irep_idt &access, bool is_static, bool is_typedef, bool is_mutable)
void implicit_typecast(exprt &expr, const typet &type) override
void typecheck_cast_expr(exprt &)
void salvage_default_arguments(const template_typet &old_type, template_typet &new_type)
bool reference_related(const exprt &expr, const reference_typet &type) const
Reference-related.
void default_dtor(const symbolt &symb, cpp_declarationt &dtor)
Note:
bool standard_conversion_integral_conversion(const exprt &expr, const typet &type, exprt &new_expr) const
Integral conversion.
bool standard_conversion_sequence(const exprt &expr, const typet &type, exprt &new_expr, unsigned &rank)
Standard Conversion Sequence.
void typecheck_expr_dereference(exprt &) override
void convert_non_template_declaration(cpp_declarationt &declaration)
irep_idt current_linkage_spec
Definition: cpp_typecheck.h:95
bool standard_conversion_qualification(const exprt &expr, const typet &, exprt &new_expr) const
Qualification conversion.
unsigned anon_counter
void typecheck_function_template(cpp_declarationt &declaration)
typecheck function templates
unsigned template_counter
void typecheck_member_initializer(codet &)
bool check_component_access(const struct_union_typet::componentt &component, const struct_union_typet &struct_union_type)
void typecheck_side_effect_function_call(side_effect_expr_function_callt &) override
std::list< instantiationt > instantiation_stackt
void typecheck_member_function(const symbolt &compound_symbol, struct_typet::componentt &component, irept &initializers, const typet &method_qualifier, exprt &value)
bool cpp_is_pod(const typet &type) const
Definition: cpp_is_pod.cpp:16
void convert_initializer(symbolt &symbol)
Initialize an object with a value.
void check_fixed_size_array(typet &type)
check that an array has fixed size
void default_cpctor(const symbolt &, cpp_declarationt &cpctor) const
Generate code for implicit default copy constructor.
bool standard_conversion_floating_point_promotion(const exprt &expr, exprt &new_expr) const
Floating-point-promotion conversion.
bool find_assignop(const symbolt &symbol) const
bool get_component(const source_locationt &source_location, const exprt &object, const irep_idt &component_name, exprt &member)
bool standard_conversion_floating_integral_conversion(const exprt &expr, const typet &type, exprt &new_expr) const
Floating-integral conversion.
bool const_typecast(const exprt &expr, const typet &type, exprt &new_expr)
void new_temporary(const source_locationt &source_location, const typet &, const exprt::operandst &ops, exprt &temporary)
void typecheck_compound_type(struct_union_typet &) override
void add_anonymous_members_to_scope(const symbolt &struct_union_symbol)
std::optional< codet > cpp_constructor(const source_locationt &source_location, const exprt &object, const exprt::operandst &operands)
void typecheck_expr_trinary(if_exprt &) override
void typecheck_class_template_member(cpp_declarationt &declaration)
typecheck class template members; these can be methods or static members
codet dtor(const symbolt &symb, const symbol_exprt &this_expr)
produces destructor code for a class object
void typecheck_try_catch(codet &)
void get_virtual_bases(const struct_typet &type, std::list< irep_idt > &vbases) const
void typecheck_expr_rel(binary_relation_exprt &) override
void typecheck_expr_reference_to(exprt &)
void show_instantiation_stack(std::ostream &)
bool standard_conversion_function_to_pointer(const exprt &expr, exprt &new_expr) const
Function-to-pointer conversion.
cpp_template_args_tct typecheck_template_args(const source_locationt &source_location, const symbolt &template_symbol, const cpp_template_args_non_tct &template_args)
void convert(cpp_linkage_spect &)
bool standard_conversion_array_to_pointer(const exprt &expr, exprt &new_expr) const
Array-to-pointer conversion.
std::unordered_set< irep_idt > deferred_typechecking
bool dynamic_typecast(const exprt &expr, const typet &type, exprt &new_expr)
void add_method_body(symbolt *_method_symbol)
void check_member_initializers(const struct_typet::basest &bases, const struct_typet::componentst &components, const irept &initializers)
Check a constructor initialization-list.
void typecheck_expr_binary_arithmetic(exprt &) override
void typecheck_expr_delete(exprt &)
method_bodiest method_bodies
void default_assignop_value(const symbolt &symbol, cpp_declaratort &declarator)
Generate code for the implicit default assignment operator.
bool support_float16_type
cpp_scopet & sub_scope_for_instantiation(cpp_scopet &template_scope, const std::string &suffix)
Set up a scope as subscope of the template scope.
cpp_typecheckt(cpp_parse_treet &_cpp_parse_tree, symbol_table_baset &_symbol_table, const std::string &_module, message_handlert &message_handler)
void typecheck_ifthenelse(code_ifthenelset &) override
cpp_scopet & tag_scope(const irep_idt &_base_name, bool has_body, bool tag_only_declaration)
void typecheck_compound_bases(struct_typet &type)
void typecheck_expr_main(exprt &) override
Called after the operands are done.
void elaborate_class_template(const typet &type)
elaborate class template instances
static bool has_auto(const typet &type)
bool builtin_factory(const irep_idt &) override
static bool has_volatile(const typet &type)
bool operator_is_overloaded(exprt &)
bool user_defined_conversion_sequence(const exprt &expr, const typet &type, exprt &new_expr, unsigned &rank)
User-defined conversion sequence.
~cpp_typecheckt() override
Definition: cpp_typecheck.h:58
bool standard_conversion_lvalue_to_rvalue(const exprt &expr, exprt &new_expr) const
Lvalue-to-rvalue conversion.
irep_idt function_identifier(const typet &type)
for function overloading
bool cast_away_constness(const typet &t1, const typet &t2) const
void typecheck() override
typechecking main method
void typecheck_expr_new(exprt &)
codet convert_anonymous_union(cpp_declarationt &declaration)
void add_implicit_dereference(exprt &)
void typecheck_expr_cpp_name(exprt &, const cpp_typecheck_fargst &)
void typecheck_expr(exprt &) override
void typecheck_friend_declaration(symbolt &symbol, cpp_declarationt &cpp_declaration)
void add_this_to_method_type(const symbolt &compound_symbol, code_typet &method_type, const typet &method_qualifier)
void typecheck_expr_side_effect(side_effect_exprt &) override
void typecheck_expr_comma(exprt &) override
bool static_typecast(const exprt &expr, const typet &type, exprt &new_expr, bool check_constantness=true)
bool subtype_typecast(const struct_typet &from, const struct_typet &to) const
void make_ptr_typecast(exprt &expr, const pointer_typet &dest_type)
void convert_parameter(const irep_idt &current_mode, code_typet::parametert &parameter)
std::optional< codet > cpp_destructor(const source_locationt &source_location, const exprt &object)
void typecheck_enum_body(symbolt &symbol)
void typecheck_expr_explicit_constructor_call(exprt &)
bool standard_conversion_integral_promotion(const exprt &expr, exprt &new_expr) const
Integral-promotion conversion.
bool find_cpctor(const symbolt &symbol) const
void typecheck_function_expr(exprt &, const cpp_typecheck_fargst &)
cpp_scopet & typecheck_template_parameters(template_typet &type)
void move_member_initializers(irept &initializers, const code_typet &type, exprt &value)
void convert(cpp_declaratort &)
void typecheck_method_application(side_effect_expr_function_callt &)
std::string to_string(const typet &) override
bool disable_access_control
void elaborate_class_template(const source_locationt &source_location, const struct_tag_typet &type)
void typecheck_expr_this(exprt &)
void typecheck_expr_throw(exprt &)
bool overloadable(const exprt &)
void typecheck_block(code_blockt &) override
std::list< irep_idt > dynamic_initializationst
void convert_parameters(const irep_idt &current_mode, code_typet &function_type)
void typecheck_while(code_whilet &) override
const struct_typet & this_struct_type()
void typecheck_expr_index(exprt &) override
void typecheck_side_effect_inc_dec(side_effect_exprt &)
void zero_initializer(const exprt &object, const typet &type, const source_locationt &source_location, exprt::operandst &ops)
bool standard_conversion_pointer_to_member(const exprt &expr, const typet &type, exprt &new_expr)
Pointer-to-member conversion.
void typecheck_class_template(cpp_declarationt &declaration)
cpp_parse_treet & cpp_parse_tree
Definition: cpp_typecheck.h:94
void typecheck_function_call_arguments(side_effect_expr_function_callt &) override
const symbolt & instantiate_template(const source_locationt &source_location, const symbolt &symbol, const cpp_template_args_tct &specialization_template_args, const cpp_template_args_tct &full_template_args, const typet &specialization=uninitialized_typet{})
void typecheck_expr_ptrmember(exprt &) override
const symbolt & class_template_symbol(const source_locationt &source_location, const symbolt &template_symbol, const cpp_template_args_tct &specialization_template_args, const cpp_template_args_tct &full_template_args)
void default_ctor(const source_locationt &source_location, const irep_idt &base_name, cpp_declarationt &ctor) const
Generate code for implicit default constructors.
exprt resolve(const cpp_namet &cpp_name, const cpp_typecheck_resolvet::wantt want, const cpp_typecheck_fargst &fargs, bool fail_with_exception=true)
Definition: cpp_typecheck.h:71
cpp_scopest cpp_scopes
Definition: cpp_typecheck.h:92
void get_bases(const struct_typet &type, std::set< irep_idt > &set_bases) const
void convert_template_function_or_member_specialization(cpp_declarationt &declaration)
void convert_class_template_specialization(cpp_declarationt &declaration)
void typecheck_expr_address_of(exprt &) override
void reference_initializer(exprt &expr, const reference_typet &type)
A reference to type "cv1 T1" is initialized by an expression of type "cv2 T2" as follows:
bool find_dtor(const symbolt &symbol) const
bool reference_binding(exprt expr, const reference_typet &type, exprt &new_expr, unsigned &rank)
Reference binding.
void typecheck_expr_function_identifier(exprt &) override
void typecheck_expr_member(exprt &) override
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
Base class for all expressions.
Definition: expr.h:56
std::vector< exprt > operandst
Definition: expr.h:58
The trinary if-then-else operator.
Definition: std_expr.h:2370
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:360
message_handlert * message_handler
Definition: message.h:439
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: pointer_expr.h:24
The reference type.
Definition: pointer_expr.h:121
A side_effect_exprt representation of a function call side effect.
Definition: std_code.h:1692
An expression containing a side effect.
Definition: std_code.h:1450
A struct tag type, i.e., struct_typet with an identifier.
Definition: std_types.h:493
Structure type, corresponds to C style structs.
Definition: std_types.h:231
std::vector< baset > basest
Definition: std_types.h:259
Base type for structs and unions.
Definition: std_types.h:62
std::vector< componentt > componentst
Definition: std_types.h:140
Expression to hold a symbol (variable)
Definition: std_expr.h:131
The symbol table base class interface.
Symbol table entry.
Definition: symbol.h:28
The type of an expression, extends irept.
Definition: type.h:29
C++ Parser.
C++ Language Type Checking.
bool cpp_typecheck(cpp_parse_treet &cpp_parse_tree, symbol_table_baset &symbol_table, const std::string &module, message_handlert &message_handler)
C++ Language Type Checking.
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:525
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:80
instantiation_stackt instantiation_stack
method_bodyt(symbolt *_method_symbol, const template_mapt &_template_map, const instantiation_stackt &_instantiation_stack)
C++ Language Type Checking.