CBMC
cpp_typecheck_fargs.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_FARGS_H
13 #define CPROVER_CPP_CPP_TYPECHECK_FARGS_H
14 
15 #include <util/expr.h>
16 
17 class code_typet;
18 class cpp_typecheckt;
20 
21 class cpp_typecheck_fargst // for function overloading
22 {
23 public:
26 
27  // has_object indicates that the first element of
28  // 'operands' is the 'this' pointer (with the object type,
29  // not pointer to object type)
30 
31  cpp_typecheck_fargst():in_use(false), has_object(false) { }
32 
33  bool has_class_type() const;
34 
35  void build(
36  const side_effect_expr_function_callt &function_call);
37 
39  const side_effect_expr_function_callt &function_call):
40  in_use(false), has_object(false)
41  {
42  build(function_call);
43  }
44 
45  bool match(
46  const code_typet &code_type,
47  unsigned &distance,
49 
50  void add_object(const exprt &expr)
51  {
52  // if(!in_use) return;
53  has_object=true;
54  operands.insert(operands.begin(), expr);
55  }
56 
58  {
60  operands.erase(operands.begin());
61  has_object = false;
62  }
63 };
64 
65 #endif // CPROVER_CPP_CPP_TYPECHECK_FARGS_H
Base type of functions.
Definition: std_types.h:583
exprt::operandst operands
cpp_typecheck_fargst(const side_effect_expr_function_callt &function_call)
bool match(const code_typet &code_type, unsigned &distance, cpp_typecheckt &cpp_typecheck) const
void build(const side_effect_expr_function_callt &function_call)
void add_object(const exprt &expr)
Base class for all expressions.
Definition: expr.h:56
std::vector< exprt > operandst
Definition: expr.h:58
A side_effect_exprt representation of a function call side effect.
Definition: std_code.h:1692
bool cpp_typecheck(cpp_parse_treet &cpp_parse_tree, symbol_table_baset &symbol_table, const std::string &module, message_handlert &message_handler)
#define PRECONDITION(CONDITION)
Definition: invariant.h:463