cprover
cpp_typecheck_function.cpp
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 #include "cpp_typecheck.h"
13 
14 #include <ansi-c/c_qualifiers.h>
15 
16 #include "cpp_template_type.h"
17 #include "cpp_type2name.h"
18 #include "cpp_util.h"
19 
21  const irep_idt &mode,
22  code_typet::parametert &parameter)
23 {
24  irep_idt base_name=id2string(parameter.get_base_name());
25 
26  if(base_name.empty())
27  {
28  base_name="#anon_arg"+std::to_string(anon_counter++);
29  parameter.set_base_name(base_name);
30  }
31 
33  id2string(base_name);
34 
35  parameter.set_identifier(identifier);
36 
37  symbolt symbol;
38 
39  symbol.name=identifier;
40  symbol.base_name=parameter.get_base_name();
41  symbol.location=parameter.source_location();
42  symbol.mode=mode;
43  symbol.module=module;
44  symbol.type=parameter.type();
45  symbol.is_state_var=true;
46  symbol.is_lvalue=!is_reference(symbol.type);
47 
48  assert(!symbol.base_name.empty());
49 
50  symbolt *new_symbol;
51 
52  if(symbol_table.move(symbol, new_symbol))
53  {
55  error() << "cpp_typecheckt::convert_parameter: symbol_table.move(\""
56  << symbol.name << "\") failed" << eom;
57  throw 0;
58  }
59 
60  // put into scope
61  cpp_scopes.put_into_scope(*new_symbol);
62 }
63 
65  const irep_idt &mode,
66  code_typet &function_type)
67 {
68  code_typet::parameterst &parameters=
69  function_type.parameters();
70 
71  for(code_typet::parameterst::iterator
72  it=parameters.begin();
73  it!=parameters.end();
74  it++)
75  convert_parameter(mode, *it);
76 }
77 
79 {
80  code_typet &function_type=
82 
83  // only a prototype?
84  if(symbol.value.is_nil())
85  return;
86 
87  // if it is a destructor, add the implicit code
88  if(symbol.type.get(ID_return_type)==ID_destructor)
89  {
90  const symbolt &msymb=lookup(symbol.type.get(ID_C_member_name));
91 
92  assert(symbol.value.id()==ID_code);
93  assert(symbol.value.get(ID_statement)==ID_block);
94 
95  symbol.value.copy_to_operands(dtor(msymb));
96  }
97 
98  // enter appropriate scope
99  cpp_save_scopet saved_scope(cpp_scopes);
100  cpp_scopet &function_scope=cpp_scopes.set_scope(symbol.name);
101 
102  // fix the scope's prefix
103  function_scope.prefix=id2string(symbol.name)+"::";
104 
105  // genuine function definition -- do the parameter declarations
106  convert_parameters(symbol.mode, function_type);
107 
108  // create "this" if it's a non-static method
109  if(function_scope.is_method &&
110  !function_scope.is_static_member)
111  {
112  code_typet::parameterst &parameters=function_type.parameters();
113  assert(parameters.size()>=1);
114  code_typet::parametert &this_parameter_expr=parameters.front();
115  function_scope.this_expr=exprt(ID_symbol, this_parameter_expr.type());
116  function_scope.this_expr.set(
117  ID_identifier, this_parameter_expr.get(ID_C_identifier));
118  }
119  else
120  function_scope.this_expr.make_nil();
121 
122  // do the function body
124 
125  // save current return type
126  typet old_return_type=return_type;
127 
128  return_type=function_type.return_type();
129 
130  // constructor, destructor?
131  if(return_type.id()==ID_constructor ||
132  return_type.id()==ID_destructor)
134 
135  typecheck_code(to_code(symbol.value));
136 
137  symbol.value.type()=symbol.type;
138 
139  return_type = old_return_type;
140 }
141 
144 {
145  const code_typet &function_type=
147 
148  const code_typet::parameterst &parameters=
149  function_type.parameters();
150 
151  std::string result;
152  bool first=true;
153 
154  result+='(';
155 
156  // the name of the function should not depend on
157  // the class name that is encoded in the type of this,
158  // but we must distinguish "const" and "non-const" member
159  // functions
160 
161  code_typet::parameterst::const_iterator it=
162  parameters.begin();
163 
164  if(it!=parameters.end() &&
165  it->get_identifier()==ID_this)
166  {
167  const typet &pointer=it->type();
168  const typet &symbol =pointer.subtype();
169  if(symbol.get_bool(ID_C_constant))
170  result+="const$";
171  if(symbol.get_bool(ID_C_volatile))
172  result+="volatile$";
173  result+="this";
174  first=false;
175  it++;
176  }
177 
178  // we skipped the "this", on purpose!
179 
180  for(; it!=parameters.end(); it++)
181  {
182  if(first)
183  first=false;
184  else
185  result+=',';
186  typet tmp_type=it->type();
187  result+=cpp_type2name(it->type());
188  }
189 
190  result+=')';
191 
192  return result;
193 }
The type of an expression.
Definition: type.h:20
irep_idt name
The unique identifier.
Definition: symbol.h:46
void convert_function(symbolt &symbol)
mstreamt & result()
Definition: message.h:233
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
Definition: namespace.cpp:139
codet dtor(const symbolt &symb)
produces destructor code for a class object
Base type of functions.
Definition: std_types.h:734
bool is_nil() const
Definition: irep.h:103
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
irep_idt mode
Language mode.
Definition: symbol.h:55
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:61
std::vector< parametert > parameterst
Definition: std_types.h:829
virtual void typecheck_code(codet &code)
exprt value
Initial value of symbol.
Definition: symbol.h:40
bool is_static_member
Definition: cpp_id.h:48
cpp_idt & put_into_scope(const symbolt &symbol, cpp_scopet &scope, bool is_friend=false)
Definition: cpp_scopes.cpp:22
void convert_parameter(const irep_idt &mode, code_typet::parametert &parameter)
irep_idt module
Name of module the symbol belongs to.
Definition: symbol.h:49
typet & type()
Definition: expr.h:60
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:240
const typet & template_subtype(const typet &type)
void set_base_name(const irep_idt &name)
Definition: std_types.h:777
symbol_tablet & symbol_table
std::string prefix
Definition: cpp_id.h:80
const irep_idt & id() const
Definition: irep.h:189
const irep_idt & get_base_name() const
Definition: std_types.h:787
const irep_idt mode
C++ Language Module.
source_locationt source_location
Definition: message.h:175
The empty type.
Definition: std_types.h:53
void convert_parameters(const irep_idt &mode, code_typet &function_type)
bool is_reference(const typet &type)
TO_BE_DOCUMENTED.
Definition: std_types.cpp:105
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
std::string cpp_type2name(const typet &type)
C++ Language Type Checking.
unsigned anon_counter
bool move(symbolt &symbol, symbolt *&new_symbol)
Move a symbol into the symbol table.
virtual void start_typecheck_code()
exprt this_expr
Definition: cpp_id.h:77
cpp_scopet & set_scope(const irep_idt &identifier)
Definition: cpp_scopes.h:88
irep_idt function_identifier(const typet &type)
for function overloading
typet type
Type of symbol.
Definition: symbol.h:37
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:43
void set_identifier(const irep_idt &identifier)
Definition: std_types.h:772
Base class for all expressions.
Definition: expr.h:46
bool is_state_var
Definition: symbol.h:66
const parameterst & parameters() const
Definition: std_types.h:841
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:52
cpp_scopet & current_scope()
Definition: cpp_scopes.h:33
const source_locationt & source_location() const
Definition: expr.h:142
bool is_method
Definition: cpp_id.h:48
const irep_idt module
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
Definition: std_types.h:884
void make_nil()
Definition: irep.h:243
mstreamt & error()
Definition: message.h:223
const codet & to_code(const exprt &expr)
Definition: std_code.h:49
const typet & subtype() const
Definition: type.h:31
bool empty() const
Definition: dstring.h:61
const typet & return_type() const
Definition: std_types.h:831
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:214
bool is_lvalue
Definition: symbol.h:71
cpp_scopest cpp_scopes