cprover
cpp_typecheck_type.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 <util/source_location.h>
15 #include <util/simplify_expr.h>
16 #include <util/c_types.h>
17 
18 #include <ansi-c/c_qualifiers.h>
19 
20 #include "cpp_convert_type.h"
21 #include "expr2cpp.h"
22 
24 {
25  assert(!type.id().empty());
26  assert(type.is_not_nil());
27 
28  try
29  {
31  }
32 
33  catch(const char *err)
34  {
36  error() << err << eom;
37  throw 0;
38  }
39 
40  catch(const std::string &err)
41  {
43  error() << err << eom;
44  throw 0;
45  }
46 
47  if(type.id()==ID_cpp_name)
48  {
49  c_qualifierst qualifiers(type);
50 
51  cpp_namet cpp_name;
52  cpp_name.swap(type);
53 
54  exprt symbol_expr=resolve(
55  cpp_name,
58 
59  if(symbol_expr.id()!=ID_type)
60  {
62  error() << "error: expected type" << eom;
63  throw 0;
64  }
65 
66  type=symbol_expr.type();
67  assert(type.is_not_nil());
68 
69  if(type.get_bool(ID_C_constant))
70  qualifiers.is_constant = true;
71 
72  qualifiers.write(type);
73  }
74  else if(type.id()==ID_struct ||
75  type.id()==ID_union)
76  {
78  }
79  else if(type.id()==ID_pointer)
80  {
81  // the pointer might have a qualifier, but do subtype first
82  typecheck_type(type.subtype());
83 
84  // Check if it is a pointer-to-member
85  if(type.find("to-member").is_not_nil())
86  {
87  // these can point either to data members or member functions
88  // of a class
89 
90  typet &class_object=static_cast<typet &>(type.add("to-member"));
91 
92  if(class_object.id()==ID_cpp_name)
93  {
94  assert(class_object.get_sub().back().id()=="::");
95  class_object.get_sub().pop_back();
96  }
97 
98  typecheck_type(class_object);
99 
100  // there may be parameters if this is a pointer to member function
101  if(type.subtype().id()==ID_code)
102  {
103  irept::subt &parameters=type.subtype().add(ID_parameters).get_sub();
104 
105  if(parameters.empty() ||
106  parameters.front().get(ID_C_base_name)!=ID_this)
107  {
108  // Add 'this' to the parameters
109  exprt a0(ID_parameter);
110  a0.set(ID_C_base_name, ID_this);
111  a0.type()=pointer_type(class_object);
112  parameters.insert(parameters.begin(), a0);
113  }
114  }
115  }
116  }
117  else if(type.id()==ID_array)
118  {
119  exprt &size_expr=to_array_type(type).size();
120 
121  if(size_expr.is_not_nil())
122  {
123  typecheck_expr(size_expr);
124  simplify(size_expr, *this);
125  }
126 
127  typecheck_type(type.subtype());
128 
129  if(type.subtype().get_bool(ID_C_constant))
130  type.set(ID_C_constant, true);
131 
132  if(type.subtype().get_bool(ID_C_volatile))
133  type.set(ID_C_volatile, true);
134  }
135  else if(type.id()==ID_code)
136  {
137  code_typet &code_type=to_code_type(type);
138  typecheck_type(code_type.return_type());
139 
140  code_typet::parameterst &parameters=code_type.parameters();
141 
142  for(auto &param : parameters)
143  {
144  typecheck_type(param.type());
145 
146  // see if there is a default value
147  if(param.has_default_value())
148  {
149  typecheck_expr(param.default_value());
150  implicit_typecast(param.default_value(), param.type());
151  }
152  }
153  }
154  else if(type.id()==ID_template)
155  {
156  typecheck_type(type.subtype());
157  }
158  else if(type.id()==ID_c_enum)
159  {
160  typecheck_enum_type(type);
161  }
162  else if(type.id()==ID_c_enum_tag)
163  {
164  }
165  else if(type.id()==ID_c_bit_field)
166  {
168  }
169  else if(type.id()==ID_unsignedbv ||
170  type.id()==ID_signedbv ||
171  type.id()==ID_bool ||
172  type.id()==ID_floatbv ||
173  type.id()==ID_fixedbv ||
174  type.id()==ID_empty)
175  {
176  }
177  else if(type.id()==ID_symbol)
178  {
179  }
180  else if(type.id()==ID_constructor ||
181  type.id()==ID_destructor)
182  {
183  }
184  else if(type.id()=="cpp-cast-operator")
185  {
186  }
187  else if(type.id()=="cpp-template-type")
188  {
189  }
190  else if(type.id()==ID_typeof)
191  {
192  exprt e=static_cast<const exprt &>(type.find(ID_expr_arg));
193 
194  if(e.is_nil())
195  {
196  typet tmp_type=
197  static_cast<const typet &>(type.find(ID_type_arg));
198 
199  if(tmp_type.id()==ID_cpp_name)
200  {
201  // this may be ambiguous -- it can be either a type or
202  // an expression
203 
204  cpp_typecheck_fargst fargs;
205 
206  exprt symbol_expr=resolve(
207  to_cpp_name(static_cast<const irept &>(tmp_type)),
209  fargs);
210 
211  type=symbol_expr.type();
212  }
213  else
214  {
215  typecheck_type(tmp_type);
216  type=tmp_type;
217  }
218  }
219  else
220  {
221  typecheck_expr(e);
222  type=e.type();
223  }
224  }
225  else if(type.id()==ID_decltype)
226  {
227  exprt e=static_cast<const exprt &>(type.find(ID_expr_arg));
228  typecheck_expr(e);
229  type=e.type();
230  }
231  else if(type.id()==ID_unassigned)
232  {
233  // ignore, for template parameter guessing
234  }
235  else if(type.id()==ID_template_class_instance)
236  {
237  // ok (internally generated)
238  }
239  else if(type.id()==ID_block_pointer)
240  {
241  // This is an Apple extension for lambda-like constructs.
242  // http://thirdcog.eu/pwcblocks/
243  }
244  else if(type.id()==ID_nullptr)
245  {
246  }
247  else
248  {
250  error() << "unexpected cpp type: " << type.pretty() << eom;
251  throw 0;
252  }
253 
254  assert(type.is_not_nil());
255 }
The type of an expression.
Definition: type.h:20
void typecheck_type(typet &type)
Base type of functions.
Definition: std_types.h:734
bool is_nil() const
Definition: irep.h:103
bool is_not_nil() const
Definition: irep.h:104
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:296
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:641
std::vector< irept > subt
Definition: irep.h:91
cpp_namet & to_cpp_name(irept &cpp_name)
Definition: cpp_name.h:143
std::vector< parametert > parameterst
Definition: std_types.h:829
typet & type()
Definition: expr.h:60
virtual void implicit_typecast(exprt &expr, const typet &type)
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:240
virtual void typecheck_expr(exprt &expr)
subt & get_sub()
Definition: irep.h:245
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a generic typet to a struct_union_typet.
Definition: std_types.h:277
void typecheck_enum_type(typet &type)
const irep_idt & id() const
Definition: irep.h:189
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Definition: std_types.h:946
source_locationt source_location
Definition: message.h:175
C++ Language Conversion.
void write(typet &src) const
const exprt & size() const
Definition: std_types.h:915
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a generic typet to a c_bit_field_typet.
Definition: std_types.h:1319
C++ Language Type Checking.
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:87
const source_locationt & source_location() const
Definition: type.h:95
Base class for all expressions.
Definition: expr.h:46
const parameterst & parameters() const
Definition: std_types.h:841
irept & add(const irep_namet &name)
Definition: irep.cpp:306
void cpp_convert_plain_type(typet &type)
void typecheck_compound_type(struct_union_typet &type)
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
Definition: std_types.h:884
void swap(irept &irep)
Definition: irep.h:231
mstreamt & error()
Definition: message.h:223
const typet & subtype() const
Definition: type.h:31
virtual void typecheck_c_bit_field_type(c_bit_field_typet &type)
bool empty() const
Definition: dstring.h:61
const irept & find(const irep_namet &name) const
Definition: irep.cpp:285
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 simplify(exprt &expr, const namespacet &ns)