cprover
cpp_typecheck_code.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/arith_tools.h>
15 #include <util/source_location.h>
16 
17 #include "cpp_convert_type.h"
19 #include "cpp_template_type.h"
20 #include "cpp_util.h"
21 #include "cpp_exception_id.h"
22 
24 {
25  const irep_idt &statement=code.get_statement();
26 
27  if(statement==ID_try_catch)
28  {
29  code.type() = empty_typet();
30  typecheck_try_catch(code);
31  }
32  else if(statement==ID_member_initializer)
33  {
34  code.type() = empty_typet();
36  }
37  else if(statement==ID_msc_if_exists ||
38  statement==ID_msc_if_not_exists)
39  {
40  }
41  else if(statement==ID_decl_block)
42  {
43  // type checked already
44  }
45  else if(statement == ID_expression)
46  {
47  if(
48  !code.has_operands() || code.op0().id() != ID_side_effect ||
49  to_side_effect_expr(code.op0()).get_statement() != ID_assign)
50  {
52  return;
53  }
54 
55  // as an extension, we support indexed access into signed/unsigned
56  // bitvectors, typically used with __CPROVER::(un)signedbv<N>
57  exprt &expr = code.op0();
58 
59  if(expr.operands().size() == 2)
60  {
61  auto &binary_expr = to_binary_expr(expr);
62 
63  if(binary_expr.op0().id() == ID_index)
64  {
65  exprt array = to_index_expr(binary_expr.op0()).array();
66  typecheck_expr(array);
67 
68  if(
69  array.type().id() == ID_signedbv ||
70  array.type().id() == ID_unsignedbv)
71  {
72  shl_exprt shl{from_integer(1, array.type()),
73  to_index_expr(binary_expr.op0()).index()};
74  exprt rhs = if_exprt{
75  equal_exprt{binary_expr.op1(), from_integer(0, array.type())},
76  bitand_exprt{array, bitnot_exprt{shl}},
77  bitor_exprt{array, shl}};
78  binary_expr.op0() = to_index_expr(binary_expr.op0()).array();
79  binary_expr.op1() = rhs;
80  }
81  }
82  }
83 
85  }
86  else
88 }
89 
91 {
92  bool first = true;
93 
94  for(auto &op : code.operands())
95  {
96  if(first)
97  {
98  // this is the 'try'
100  first = false;
101  }
102  else
103  {
104  // This is (one of) the catch clauses.
105  code_blockt &catch_block = to_code_block(to_code(op));
106 
107  // look at the catch operand
108  auto &statements = catch_block.statements();
109  PRECONDITION(!statements.empty());
110 
111  if(statements.front().get_statement() == ID_ellipsis)
112  {
113  statements.erase(statements.begin());
114 
115  // do body
116  typecheck_code(catch_block);
117  }
118  else
119  {
120  // turn references into non-references
121  {
122  code_declt &decl = to_code_decl(statements.front());
123  cpp_declarationt &cpp_declaration = to_cpp_declaration(decl.symbol());
124 
125  assert(cpp_declaration.declarators().size()==1);
126  cpp_declaratort &declarator=cpp_declaration.declarators().front();
127 
128  if(is_reference(declarator.type()))
129  declarator.type()=declarator.type().subtype();
130  }
131 
132  // typecheck the body
133  typecheck_code(catch_block);
134 
135  // the declaration is now in a decl_block
136  CHECK_RETURN(!catch_block.statements().empty());
137  CHECK_RETURN(
138  catch_block.statements().front().get_statement() == ID_decl_block);
139 
140  // get the declaration
141  const code_declt &code_decl =
142  to_code_decl(to_code(catch_block.statements().front().op0()));
143 
144  // get the type
145  const typet &type = code_decl.symbol().type();
146 
147  // annotate exception ID
148  op.set(ID_exception_id, cpp_exception_id(type, *this));
149  }
150  }
151  }
152 }
153 
155 {
156  // In addition to the C syntax, C++ also allows a declaration
157  // as condition. E.g.,
158  // if(void *p=...) ...
159 
160  if(code.cond().id()==ID_code)
161  {
162  typecheck_code(to_code(code.cond()));
163  }
164  else
166 }
167 
169 {
170  // In addition to the C syntax, C++ also allows a declaration
171  // as condition. E.g.,
172  // while(void *p=...) ...
173 
174  if(code.cond().id()==ID_code)
175  {
176  typecheck_code(to_code(code.cond()));
177  }
178  else
180 }
181 
183 {
184  // In addition to the C syntax, C++ also allows a declaration
185  // as condition. E.g.,
186  // switch(int i=...) ...
187 
188  exprt &value = to_code_switch(code).value();
189  if(value.id() == ID_code)
190  {
191  // we shall rewrite that into
192  // { int i=....; switch(i) .... }
193 
194  codet decl = to_code(value);
195  typecheck_decl(decl);
196 
197  assert(decl.get_statement()==ID_decl_block);
198  assert(decl.operands().size()==1);
199 
200  // replace declaration by its symbol
201  value = to_code_decl(to_code(to_unary_expr(decl).op())).symbol();
202 
204 
205  code_blockt code_block({to_code(decl.op0()), code});
206  code.swap(code_block);
207  }
208  else
210 }
211 
213 {
214  const cpp_namet &member=
215  to_cpp_name(code.find(ID_member));
216 
217  // Let's first typecheck the operands.
218  Forall_operands(it, code)
219  {
220  const bool has_array_ini = it->get_bool(ID_C_array_ini);
221  typecheck_expr(*it);
222  if(has_array_ini)
223  it->set(ID_C_array_ini, true);
224  }
225 
226  // The initializer may be a data member (non-type)
227  // or a parent class (type).
228  // We ask for VAR only, as we get the parent classes via their
229  // constructor!
230  cpp_typecheck_fargst fargs;
231  fargs.in_use=true;
232  fargs.operands=code.operands();
233 
234  // We should only really resolve in qualified mode,
235  // no need to look into the parent.
236  // Plus, this should happen in class scope, not the scope of
237  // the constructor because of the constructor arguments.
238  exprt symbol_expr=
240 
241  if(symbol_expr.type().id()==ID_code)
242  {
243  const code_typet &code_type=to_code_type(symbol_expr.type());
244 
245  assert(code_type.parameters().size()>=1);
246 
247  // It's a parent. Call the constructor that we got.
248  side_effect_expr_function_callt function_call(
249  symbol_expr, {}, uninitialized_typet{}, code.source_location());
250  function_call.arguments().reserve(code.operands().size()+1);
251 
252  // we have to add 'this'
253  exprt this_expr = cpp_scopes.current_scope().this_expr;
254  assert(this_expr.is_not_nil());
255 
257  this_expr,
258  code_type.parameters().front().type());
259 
260  function_call.arguments().push_back(this_expr);
261 
262  forall_operands(it, code)
263  function_call.arguments().push_back(*it);
264 
265  // done building the expression, check the argument types
266  typecheck_function_call_arguments(function_call);
267 
268  if(symbol_expr.get_bool(ID_C_not_accessible))
269  {
270  const irep_idt &access = symbol_expr.get(ID_C_access);
271  CHECK_RETURN(
272  access == ID_private || access == ID_protected ||
273  access == ID_noaccess);
274 
275  if(access == ID_private || access == ID_noaccess)
276  {
277  #if 0
279  str << "error: constructor of '"
280  << to_string(symbol_expr)
281  << "' is not accessible";
282  throw 0;
283  #endif
284  }
285  }
286 
287  code_expressiont code_expression(function_call);
288 
289  code.swap(code_expression);
290  }
291  else
292  {
293  // a reference member
294  if(
295  symbol_expr.id() == ID_dereference &&
296  to_dereference_expr(symbol_expr).pointer().id() == ID_member &&
297  symbol_expr.get_bool(ID_C_implicit))
298  {
299  // treat references as normal pointers
300  exprt tmp = to_dereference_expr(symbol_expr).pointer();
301  symbol_expr.swap(tmp);
302  }
303 
304  if(symbol_expr.id() == ID_symbol &&
305  symbol_expr.type().id()!=ID_code)
306  {
307  // maybe the name of the member collides with a parameter of the
308  // constructor
310  ID_dereference, cpp_scopes.current_scope().this_expr.type().subtype());
311  dereference.copy_to_operands(cpp_scopes.current_scope().this_expr);
312  cpp_typecheck_fargst deref_fargs;
313  deref_fargs.add_object(dereference);
314 
315  {
316  cpp_save_scopet cpp_saved_scope(cpp_scopes);
319  symbol_expr =
320  resolve(member, cpp_typecheck_resolvet::wantt::VAR, deref_fargs);
321  }
322 
323  if(
324  symbol_expr.id() == ID_dereference &&
325  to_dereference_expr(symbol_expr).pointer().id() == ID_member &&
326  symbol_expr.get_bool(ID_C_implicit))
327  {
328  // treat references as normal pointers
329  exprt tmp = to_dereference_expr(symbol_expr).pointer();
330  symbol_expr.swap(tmp);
331  }
332  }
333 
334  if(
335  symbol_expr.id() == ID_member &&
336  to_member_expr(symbol_expr).op().id() == ID_dereference &&
337  to_dereference_expr(to_member_expr(symbol_expr).op()).pointer() ==
339  {
340  if(is_reference(symbol_expr.type()))
341  {
342  // it's a reference member
343  if(code.operands().size()!= 1)
344  {
346  error() << " reference '" << to_string(symbol_expr)
347  << "' expects one initializer" << eom;
348  throw 0;
349  }
350 
351  reference_initializer(code.op0(), symbol_expr.type());
352 
353  // assign the pointers
354  symbol_expr.type().remove(ID_C_reference);
355  symbol_expr.set(ID_C_lvalue, true);
356  code.op0().type().remove(ID_C_reference);
357 
358  side_effect_exprt assign(
359  ID_assign,
360  {symbol_expr, code.op0()},
361  typet(),
362  code.source_location());
364  code_expressiont new_code(assign);
365  code.swap(new_code);
366  }
367  else
368  {
369  // it's a data member
371 
372  auto call =
373  cpp_constructor(code.source_location(), symbol_expr, code.operands());
374 
375  if(call.has_value())
376  code.swap(call.value());
377  else
378  {
379  auto source_location = code.source_location();
380  code = code_skipt();
381  code.add_source_location() = source_location;
382  }
383  }
384  }
385  else
386  {
388  error() << "invalid member initializer '" << to_string(symbol_expr) << "'"
389  << eom;
390  throw 0;
391  }
392  }
393 }
394 
396 {
397  if(code.operands().size()!=1)
398  {
400  error() << "declaration expected to have one operand" << eom;
401  throw 0;
402  }
403 
404  assert(code.op0().id()==ID_cpp_declaration);
405 
406  cpp_declarationt &declaration=
407  to_cpp_declaration(code.op0());
408 
409  typet &type=declaration.type();
410 
411  bool is_typedef=declaration.is_typedef();
412 
413  if(declaration.declarators().empty() || !has_auto(type))
414  typecheck_type(type);
415 
416  assert(type.is_not_nil());
417 
418  if(declaration.declarators().empty() &&
419  follow(type).get_bool(ID_C_is_anonymous))
420  {
421  if(type.id() != ID_union_tag)
422  {
424  error() << "declaration statement does not declare anything"
425  << eom;
426  throw 0;
427  }
428 
429  code = convert_anonymous_union(declaration);
430  return;
431  }
432 
433  // mark as 'already typechecked'
435 
436  codet new_code(ID_decl_block);
437  new_code.reserve_operands(declaration.declarators().size());
438 
439  // Do the declarators (if any)
440  for(auto &declarator : declaration.declarators())
441  {
442  cpp_declarator_convertert cpp_declarator_converter(*this);
443  cpp_declarator_converter.is_typedef=is_typedef;
444 
445  const symbolt &symbol=
446  cpp_declarator_converter.convert(declaration, declarator);
447 
448  if(is_typedef)
449  continue;
450 
451  code_declt decl_statement(cpp_symbol_expr(symbol));
452  decl_statement.add_source_location()=symbol.location;
453 
454  // Do we have an initializer that's not code?
455  if(symbol.value.is_not_nil() &&
456  symbol.value.id()!=ID_code)
457  {
458  decl_statement.copy_to_operands(symbol.value);
460  has_auto(symbol.type) ||
461  follow(decl_statement.op1().type()) == follow(symbol.type),
462  "declarator type should match symbol type");
463  }
464 
465  new_code.add_to_operands(std::move(decl_statement));
466 
467  // is there a constructor to be called?
468  if(symbol.value.is_not_nil())
469  {
471  declarator.find(ID_init_args).is_nil(),
472  "declarator should not have init_args");
473  if(symbol.value.id()==ID_code)
474  new_code.copy_to_operands(symbol.value);
475  }
476  else
477  {
478  exprt object_expr=cpp_symbol_expr(symbol);
479 
481 
482  auto constructor_call = cpp_constructor(
483  symbol.location, object_expr, declarator.init_args().operands());
484 
485  if(constructor_call.has_value())
486  new_code.add_to_operands(std::move(constructor_call.value()));
487  }
488  }
489 
490  code.swap(new_code);
491 }
492 
494 {
495  cpp_save_scopet saved_scope(cpp_scopes);
497 
499 }
exprt::copy_to_operands
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
Definition: expr.h:150
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
cpp_idt::class_identifier
irep_idt class_identifier
Definition: cpp_id.h:81
code_blockt
A codet representing sequential composition of program statements.
Definition: std_code.h:170
to_unary_expr
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:316
typet::subtype
const typet & subtype() const
Definition: type.h:47
cpp_declarationt::is_typedef
bool is_typedef() const
Definition: cpp_declaration.h:135
cpp_typecheckt::typecheck_switch
void typecheck_switch(codet &) override
Definition: cpp_typecheck_code.cpp:182
Forall_operands
#define Forall_operands(it, expr)
Definition: expr.h:24
arith_tools.h
code_whilet
codet representing a while statement.
Definition: std_code.h:896
cpp_typecheck_fargst
Definition: cpp_typecheck_fargs.h:23
codet::op0
exprt & op0()
Definition: expr.h:102
to_code_decl
const code_declt & to_code_decl(const codet &code)
Definition: std_code.h:450
cpp_save_scopet
Definition: cpp_scopes.h:129
c_typecheck_baset::typecheck_while
virtual void typecheck_while(code_whilet &code)
Definition: c_typecheck_code.cpp:731
cpp_scopest::id_map
id_mapt id_map
Definition: cpp_scopes.h:69
cpp_typecheckt::cpp_scopes
cpp_scopest cpp_scopes
Definition: cpp_typecheck.h:109
cpp_idt::this_expr
exprt this_expr
Definition: cpp_id.h:82
cpp_exception_id
irep_idt cpp_exception_id(const typet &src, const namespacet &ns)
turns a type into an exception ID
Definition: cpp_exception_id.cpp:90
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
typet
The type of an expression, extends irept.
Definition: type.h:29
cpp_typecheckt::typecheck_while
void typecheck_while(code_whilet &) override
Definition: cpp_typecheck_code.cpp:168
to_cpp_declaration
cpp_declarationt & to_cpp_declaration(irept &irep)
Definition: cpp_declaration.h:148
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1347
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
cpp_typecheckt::typecheck_side_effect_assignment
void typecheck_side_effect_assignment(side_effect_exprt &) override
Definition: cpp_typecheck_expr.cpp:1997
side_effect_expr_function_callt
A side_effect_exprt representation of a function call side effect.
Definition: std_code.h:2117
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:2964
cpp_typecheckt::typecheck_block
void typecheck_block(code_blockt &) override
Definition: cpp_typecheck_code.cpp:493
cpp_typecheck_fargst::operands
exprt::operandst operands
Definition: cpp_typecheck_fargs.h:26
irept::find
const irept & find(const irep_namet &name) const
Definition: irep.cpp:103
code_declt
A codet representing the declaration of a local variable.
Definition: std_code.h:402
cpp_declarator_convertert::convert
symbolt & convert(const typet &type, const cpp_storage_spect &storage_spec, const cpp_member_spect &member_spec, cpp_declaratort &declarator)
Definition: cpp_declarator_converter.cpp:34
exprt
Base class for all expressions.
Definition: expr.h:53
cpp_typecheckt::cpp_constructor
optionalt< codet > cpp_constructor(const source_locationt &source_location, const exprt &object, const exprt::operandst &operands)
Definition: cpp_constructor.cpp:25
exprt::op0
exprt & op0()
Definition: expr.h:102
cpp_typecheckt::typecheck_decl
void typecheck_decl(codet &) override
Definition: cpp_typecheck_code.cpp:395
code_ifthenelset::cond
const exprt & cond() const
Definition: std_code.h:764
messaget::eom
static eomt eom
Definition: message.h:297
cpp_typecheckt::typecheck_try_catch
void typecheck_try_catch(codet &)
Definition: cpp_typecheck_code.cpp:90
to_side_effect_expr
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition: std_code.h:1931
equal_exprt
Equality.
Definition: std_expr.h:1190
code_ifthenelset
codet representation of an if-then-else statement.
Definition: std_code.h:746
cpp_declarationt::declarators
const declaratorst & declarators() const
Definition: cpp_declaration.h:64
cpp_exception_id.h
C++ Language Type Checking.
to_code
const codet & to_code(const exprt &expr)
Definition: std_code.h:155
to_binary_expr
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:678
code_blockt::statements
code_operandst & statements()
Definition: std_code.h:178
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
cpp_typecheckt::typecheck_type
void typecheck_type(typet &) override
Definition: cpp_typecheck_type.cpp:23
irept::get_bool
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:64
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:402
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:946
bitor_exprt
Bit-wise OR.
Definition: std_expr.h:2388
messaget::error
mstreamt & error() const
Definition: message.h:399
empty_typet
The empty type.
Definition: std_types.h:46
already_typechecked_exprt::make_already_typechecked
static void make_already_typechecked(exprt &expr)
Definition: c_typecheck_base.h:289
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
exprt::has_operands
bool has_operands() const
Return true if there is at least one operand.
Definition: expr.h:92
cpp_util.h
cpp_scopest::current_scope
cpp_scopet & current_scope()
Definition: cpp_scopes.h:33
messaget::mstreamt::source_location
source_locationt source_location
Definition: message.h:247
cpp_typecheckt::reference_initializer
void reference_initializer(exprt &expr, const typet &type)
A reference to type "cv1 T1" is initialized by an expression of type "cv2 T2" as follows:
Definition: cpp_typecheck_conversions.cpp:1547
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:18
cpp_declarator_convertert
Definition: cpp_declarator_converter.h:26
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
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:231
cpp_declarator_convertert::is_typedef
bool is_typedef
Definition: cpp_declarator_converter.h:31
cpp_symbol_expr
symbol_exprt cpp_symbol_expr(const symbolt &symbol)
Definition: cpp_util.cpp:14
dereference_exprt::pointer
exprt & pointer()
Definition: std_expr.h:2901
cpp_typecheckt::typecheck_function_call_arguments
void typecheck_function_call_arguments(side_effect_expr_function_callt &) override
Definition: cpp_typecheck_expr.cpp:1832
exprt::op1
exprt & op1()
Definition: expr.h:105
cpp_typecheckt::make_ptr_typecast
void make_ptr_typecast(exprt &expr, const typet &dest_type)
Definition: cpp_typecheck_compound_type.cpp:1680
source_location.h
index_exprt::index
exprt & index()
Definition: std_expr.h:1319
cpp_typecheckt::typecheck_ifthenelse
void typecheck_ifthenelse(code_ifthenelset &) override
Definition: cpp_typecheck_code.cpp:154
index_exprt::array
exprt & array()
Definition: std_expr.h:1309
c_typecheck_baset::typecheck_code
virtual void typecheck_code(codet &code)
Definition: c_typecheck_code.cpp:26
irept::swap
void swap(irept &irep)
Definition: irep.h:463
cpp_typecheck_fargst::in_use
bool in_use
Definition: cpp_typecheck_fargs.h:25
code_typet
Base type of functions.
Definition: std_types.h:736
cpp_convert_type.h
C++ Language Conversion.
code_whilet::cond
const exprt & cond() const
Definition: std_code.h:903
cpp_declarationt
Definition: cpp_declaration.h:24
irept::id
const irep_idt & id() const
Definition: irep.h:418
irept::remove
void remove(const irep_namet &name)
Definition: irep.cpp:93
cpp_typecheck_fargst::add_object
void add_object(const exprt &expr)
Definition: cpp_typecheck_fargs.h:51
bitand_exprt
Bit-wise AND.
Definition: std_expr.h:2460
cpp_scopest::go_to
void go_to(cpp_idt &id)
Definition: cpp_scopes.h:104
c_typecheck_baset::typecheck_switch
virtual void typecheck_switch(codet &code)
Definition: c_typecheck_code.cpp:668
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:857
cpp_typecheck.h
C++ Language Type Checking.
code_declt::symbol
symbol_exprt & symbol()
Definition: std_code.h:408
side_effect_exprt::get_statement
const irep_idt & get_statement() const
Definition: std_code.h:1897
bitnot_exprt
Bit-wise negation of bit-vectors.
Definition: std_expr.h:2344
cpp_scopest::new_block_scope
cpp_scopet & new_block_scope()
Definition: cpp_scopes.cpp:16
code_switcht::value
const exprt & value() const
Definition: std_code.h:841
to_dereference_expr
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: std_expr.h:2944
cpp_typecheckt::typecheck_expr
void typecheck_expr(exprt &) override
Definition: cpp_typecheck_expr.cpp:2251
symbolt::value
exprt value
Initial value of symbol.
Definition: symbol.h:34
code_skipt
A codet representing a skip statement.
Definition: std_code.h:270
cpp_typecheckt::typecheck_code
void typecheck_code(codet &) override
Definition: cpp_typecheck_code.cpp:23
cpp_typecheckt::typecheck_member_initializer
void typecheck_member_initializer(codet &)
Definition: cpp_typecheck_code.cpp:212
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:51
is_reference
bool is_reference(const typet &type)
Returns true if the type is a reference.
Definition: std_types.cpp:133
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
symbolt
Symbol table entry.
Definition: symbol.h:28
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:442
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
side_effect_expr_function_callt::arguments
exprt::operandst & arguments()
Definition: std_code.h:2161
cpp_typecheckt::has_auto
static bool has_auto(const typet &type)
Definition: cpp_typecheck_compound_type.cpp:64
to_code_switch
const code_switcht & to_code_switch(const codet &code)
Definition: std_code.h:878
cpp_typecheckt::convert_anonymous_union
codet convert_anonymous_union(cpp_declarationt &declaration)
Definition: cpp_typecheck_declaration.cpp:33
exprt::add_to_operands
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition: expr.h:157
cpp_typecheck_resolvet::wantt::VAR
@ VAR
already_typechecked_typet::make_already_typechecked
static void make_already_typechecked(typet &type)
Definition: c_typecheck_base.h:309
c_typecheck_baset::typecheck_ifthenelse
virtual void typecheck_ifthenelse(code_ifthenelset &code)
Definition: c_typecheck_code.cpp:574
to_code_block
const code_blockt & to_code_block(const codet &code)
Definition: std_code.h:256
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:3489
cpp_typecheckt::to_string
std::string to_string(const typet &) override
Definition: cpp_typecheck.cpp:84
exprt::operands
operandst & operands()
Definition: expr.h:95
codet::op1
exprt & op1()
Definition: expr.h:105
dereference
void dereference(const irep_idt &function_id, goto_programt::const_targett target, exprt &expr, const namespacet &ns, value_setst &value_sets)
Remove dereferences in expr using value_sets to determine to what objects the pointers may be pointin...
Definition: goto_program_dereference.cpp:303
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:259
uninitialized_typet
Definition: cpp_parse_tree.h:32
codet::get_statement
const irep_idt & get_statement() const
Definition: std_code.h:71
cpp_typecheckt::resolve
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:88
exprt::reserve_operands
void reserve_operands(operandst::size_type n)
Definition: expr.h:127
binary_exprt::op1
exprt & op1()
Definition: expr.h:105
cpp_namet
Definition: cpp_name.h:17
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:254
cpp_declaratort
Definition: cpp_declarator.h:20
side_effect_exprt
An expression containing a side effect.
Definition: std_code.h:1866
to_cpp_name
cpp_namet & to_cpp_name(irept &cpp_name)
Definition: cpp_name.h:144
c_typecheck_baset::typecheck_block
virtual void typecheck_block(code_blockt &code)
Definition: c_typecheck_code.cpp:187
code_expressiont
codet representation of an expression statement.
Definition: std_code.h:1810
cpp_template_type.h
shl_exprt
Left shift.
Definition: std_expr.h:2561
cpp_declarator_converter.h
C++ Language Type Checking.
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:35