cprover
Loading...
Searching...
No Matches
casting_replace_symbol.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: ANSI-C Linking
4
5Author: Michael Tautschnig
6
7\*******************************************************************/
8
11
13
14#include <util/pointer_expr.h>
15#include <util/std_code.h>
16#include <util/std_expr.h>
17
19{
20 bool result = true; // unchanged
21
22 // first look at type
23
24 const exprt &const_dest(dest);
25 if(have_to_replace(const_dest.type()))
27 result = false;
28
29 // now do expression itself
30
31 if(!have_to_replace(dest))
32 return result;
33
34 if(dest.id() == ID_side_effect)
35 {
37 {
38 if(!have_to_replace(call->function()))
39 return replace_symbolt::replace(dest);
40
41 exprt before = dest;
42 code_typet type = to_code_type(call->function().type());
43
44 result &= replace_symbolt::replace(call->function());
45
46 // maybe add type casts here?
47 for(auto &arg : call->arguments())
48 result &= replace_symbolt::replace(arg);
49
50 if(
51 type.return_type() !=
52 to_code_type(call->function().type()).return_type())
53 {
54 call->type() = to_code_type(call->function().type()).return_type();
55 dest = typecast_exprt(*call, type.return_type());
56 result = true;
57 }
58
59 return result;
60 }
61 }
62 else if(dest.id() == ID_address_of)
63 {
64 pointer_typet ptr_type = to_pointer_type(dest.type());
65
66 result &= replace_symbolt::replace(dest);
67
68 address_of_exprt address_of = to_address_of_expr(dest);
69 if(address_of.object().type() != ptr_type.base_type())
70 {
71 to_pointer_type(address_of.type()).base_type() =
72 address_of.object().type();
73 dest = typecast_exprt{address_of, std::move(ptr_type)};
74 result = true;
75 }
76
77 return result;
78 }
79
80 return replace_symbolt::replace(dest);
81}
82
84{
85 expr_mapt::const_iterator it = expr_map.find(s.get_identifier());
86
87 if(it == expr_map.end())
88 return true;
89
90 const exprt &e = it->second;
91
92 source_locationt previous_source_location{s.source_location()};
94 previous_source_location.is_not_nil(),
95 "front-ends should construct symbol expressions with source locations",
96 s.pretty());
97 if(e.type().id() != ID_array && e.type().id() != ID_code)
98 {
99 typet type = s.type();
100 static_cast<exprt &>(s) = typecast_exprt::conditional_cast(e, type);
101 }
102 else
103 static_cast<exprt &>(s) = e;
104 s.add_source_location() = std::move(previous_source_location);
105
106 return false;
107}
Operator to return the address of an object.
bool replace_symbol_expr(symbol_exprt &dest) const override
bool replace(exprt &dest) const override
Base type of functions.
Definition std_types.h:583
const typet & return_type() const
Definition std_types.h:689
Base class for all expressions.
Definition expr.h:56
typet & type()
Return the type of the expression.
Definition expr.h:84
const source_locationt & source_location() const
Definition expr.h:231
source_locationt & add_source_location()
Definition expr.h:236
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition irep.cpp:482
const irep_idt & id() const
Definition irep.h:388
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
const typet & base_type() const
The type of the data what we point to.
virtual bool replace(exprt &dest) const
bool have_to_replace(const exprt &dest) const
Expression to hold a symbol (variable)
Definition std_expr.h:131
const irep_idt & get_identifier() const
Definition std_expr.h:160
Semantic type conversion.
Definition std_expr.h:2068
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:2076
The type of an expression, extends irept.
Definition type.h:29
auto expr_try_dynamic_cast(TExpr &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TExpr >::type
Try to cast a reference to a generic exprt to a specific derived class.
Definition expr_cast.h:81
API to expression classes for Pointers.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
#define DATA_INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
Definition invariant.h:535
API to expression classes.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition std_types.h:788