cprover
replace_symbol_ext.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Modified expression replacement for constant propagator
4 
5 Author: Peter Schrammel
6 
7 \*******************************************************************/
8 
11 
12 #include "replace_symbol_ext.h"
13 
14 #include <util/std_types.h>
15 #include <util/std_expr.h>
16 
19 {
20  bool result=true;
21 
22  // first look at type
23 
24  if(have_to_replace(dest.type()))
25  if(!replace_symbolt::replace(dest.type()))
26  result=false;
27 
28  // now do expression itself
29 
30  if(!have_to_replace(dest))
31  return result;
32 
33  // do not replace object in address_of expressions
34  if(dest.id()==ID_address_of)
35  {
36  const exprt &object = to_address_of_expr(dest).object();
37  if(object.id()==ID_symbol)
38  {
39  expr_mapt::const_iterator it=
40  expr_map.find(object.get(ID_identifier));
41 
42  if(it!=expr_map.end())
43  return false;
44  }
45  }
46  else if(dest.id()==ID_symbol)
47  {
48  expr_mapt::const_iterator it=
49  expr_map.find(dest.get(ID_identifier));
50 
51  if(it!=expr_map.end())
52  {
53  dest=it->second;
54  return false;
55  }
56  }
57 
58  Forall_operands(it, dest)
59  if(!replace(*it))
60  result=false;
61 
62  const irept &c_sizeof_type=dest.find(ID_C_c_sizeof_type);
63 
64  if(c_sizeof_type.is_not_nil() &&
66  static_cast<typet&>(dest.add(ID_C_c_sizeof_type))))
67  result=false;
68 
69  const irept &va_arg_type=dest.find(ID_C_va_arg_type);
70 
71  if(va_arg_type.is_not_nil() &&
72  !replace_symbolt::replace(static_cast<typet&>(dest.add(ID_C_va_arg_type))))
73  result=false;
74 
75  return result;
76 }
bool is_not_nil() const
Definition: irep.h:104
exprt & object()
Definition: std_expr.h:2608
virtual bool replace(exprt &dest) const
does not replace object in address_of expressions
virtual bool replace(exprt &dest) const
typet & type()
Definition: expr.h:60
const irep_idt & id() const
Definition: irep.h:189
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast a generic exprt to an address_of_exprt.
Definition: std_expr.h:2629
API to expression classes.
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
bool have_to_replace(const exprt &dest) const
Base class for tree-like data structures with sharing.
Definition: irep.h:87
API to type classes.
Modified expression replacement for constant propagator.
Base class for all expressions.
Definition: expr.h:46
irept & add(const irep_namet &name)
Definition: irep.cpp:306
#define Forall_operands(it, expr)
Definition: expr.h:23
expr_mapt expr_map
const irept & find(const irep_namet &name) const
Definition: irep.cpp:285