cprover
Toggle main menu visibility
Loading...
Searching...
No Matches
casting_replace_symbol.cpp
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module: ANSI-C Linking
4
5
Author: Michael Tautschnig
6
7
\*******************************************************************/
8
11
12
#include "
casting_replace_symbol.h
"
13
14
#include <
util/pointer_expr.h
>
15
#include <
util/std_code.h
>
16
#include <
util/std_expr.h
>
17
18
bool
casting_replace_symbolt::replace
(
exprt
&dest)
const
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
()))
26
if
(!
replace_symbolt::replace
(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
{
36
if
(
auto
call =
expr_try_dynamic_cast<side_effect_expr_function_callt>
(dest))
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
83
bool
casting_replace_symbolt::replace_symbol_expr
(
symbol_exprt
&s)
const
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
()};
93
DATA_INVARIANT_WITH_DIAGNOSTICS
(
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
}
casting_replace_symbol.h
ANSI-C Linking.
address_of_exprt
Operator to return the address of an object.
Definition
pointer_expr.h:540
address_of_exprt::object
exprt & object()
Definition
pointer_expr.h:549
casting_replace_symbolt::replace_symbol_expr
bool replace_symbol_expr(symbol_exprt &dest) const override
Definition
casting_replace_symbol.cpp:83
casting_replace_symbolt::replace
bool replace(exprt &dest) const override
Definition
casting_replace_symbol.cpp:18
code_typet
Base type of functions.
Definition
std_types.h:583
code_typet::return_type
const typet & return_type() const
Definition
std_types.h:689
exprt
Base class for all expressions.
Definition
expr.h:57
exprt::type
typet & type()
Return the type of the expression.
Definition
expr.h:85
exprt::source_location
const source_locationt & source_location() const
Definition
expr.h:236
exprt::add_source_location
source_locationt & add_source_location()
Definition
expr.h:241
irept::pretty
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition
irep.cpp:482
irept::is_not_nil
bool is_not_nil() const
Definition
irep.h:372
irept::id
const irep_idt & id() const
Definition
irep.h:388
pointer_typet
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition
pointer_expr.h:24
pointer_typet::base_type
const typet & base_type() const
The type of the data what we point to.
Definition
pointer_expr.h:35
replace_symbolt::replace
virtual bool replace(exprt &dest) const
Definition
replace_symbol.cpp:64
replace_symbolt::have_to_replace
bool have_to_replace(const exprt &dest) const
Definition
replace_symbol.cpp:164
replace_symbolt::expr_map
expr_mapt expr_map
Definition
replace_symbol.h:93
source_locationt
Definition
source_location.h:20
symbol_exprt
Expression to hold a symbol (variable).
Definition
std_expr.h:132
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition
std_expr.h:161
typecast_exprt
Semantic type conversion.
Definition
std_expr.h:1985
typecast_exprt::conditional_cast
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition
std_expr.h:1993
typet
The type of an expression, extends irept.
Definition
type.h:29
expr_try_dynamic_cast
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
pointer_expr.h
API to expression classes for Pointers.
to_address_of_expr
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition
pointer_expr.h:577
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition
pointer_expr.h:93
DATA_INVARIANT_WITH_DIAGNOSTICS
#define DATA_INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
Definition
invariant.h:535
std_code.h
std_expr.h
API to expression classes.
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition
std_types.h:788
linking
casting_replace_symbol.cpp
Generated by
1.17.0