cprover
Toggle main menu visibility
Loading...
Searching...
No Matches
does_remove_const.cpp
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module: Analyses
4
5
Author: Diffblue Ltd.
6
7
\*******************************************************************/
8
11
12
#include "
does_remove_const.h
"
13
14
#include <
goto-programs/goto_program.h
>
15
16
#include <
util/pointer_expr.h
>
17
20
does_remove_constt::does_remove_constt
(
const
goto_programt
&
goto_program
)
21
:
goto_program
(
goto_program
)
22
{}
23
26
std::pair<bool, source_locationt>
does_remove_constt::operator()
()
const
27
{
28
for
(
const
goto_programt::instructiont
&instruction :
29
goto_program
.instructions)
30
{
31
if
(!instruction.
is_assign
())
32
{
33
continue
;
34
}
35
36
const
typet
&rhs_type = instruction.
assign_rhs
().
type
();
37
const
typet
&lhs_type = instruction.
assign_lhs
().
type
();
38
39
// Compare the types recursively for a point where the rhs is more
40
// const that the lhs
41
if
(!
does_type_preserve_const_correctness
(&lhs_type, &rhs_type))
42
{
43
return
{
true
, instruction.
source_location
()};
44
}
45
46
if
(
does_expr_lose_const
(instruction.
assign_rhs
()))
47
{
48
return
{
true
, instruction.
assign_rhs
().
find_source_location
()};
49
}
50
}
51
52
return
{
false
,
source_locationt
()};
53
}
54
61
bool
does_remove_constt::does_expr_lose_const
(
const
exprt
&expr)
const
62
{
63
const
typet
&root_type=expr.
type
();
64
65
// Look in each child that has the same type as the root
66
for
(
const
exprt
&op : expr.
operands
())
67
{
68
const
typet
&op_type=op.type();
69
if
(op_type == root_type)
70
{
71
// Is this child more const-qualified than the root
72
if
(!
does_type_preserve_const_correctness
(&root_type, &op_type))
73
{
74
return
true
;
75
}
76
}
77
78
// Recursively check the children of this child
79
if
(
does_expr_lose_const
(op))
80
{
81
return
true
;
82
}
83
}
84
return
false
;
85
}
86
114
bool
does_remove_constt::does_type_preserve_const_correctness
(
115
const
typet
*target_type,
const
typet
*source_type)
const
116
{
117
while
(target_type->
id
()==ID_pointer)
118
{
119
PRECONDITION
(source_type->
id
() == ID_pointer);
120
121
const
auto
&target_pointer_type =
to_pointer_type
(*target_type);
122
const
auto
&source_pointer_type =
to_pointer_type
(*source_type);
123
124
bool
direct_subtypes_at_least_as_const =
is_type_at_least_as_const_as
(
125
target_pointer_type.base_type(), source_pointer_type.base_type());
126
// We have a pointer to something, but the thing it is pointing to can't be
127
// modified normally, but can through this pointer
128
if
(!direct_subtypes_at_least_as_const)
129
return
false
;
130
// Check the subtypes if they are pointers
131
target_type = &target_pointer_type.base_type();
132
source_type = &source_pointer_type.base_type();
133
}
134
return
true
;
135
}
136
158
bool
does_remove_constt::is_type_at_least_as_const_as
(
159
const
typet
&type_more_const,
const
typet
&type_compare)
const
160
{
161
return
!type_compare.
get_bool
(ID_C_constant) ||
162
type_more_const.
get_bool
(ID_C_constant);
163
}
does_remove_constt::is_type_at_least_as_const_as
bool is_type_at_least_as_const_as(const typet &type_more_const, const typet &type_compare) const
A simple check to check the type_more_const is at least as const as type compare.
Definition
does_remove_const.cpp:158
does_remove_constt::does_type_preserve_const_correctness
bool does_type_preserve_const_correctness(const typet *target_type, const typet *source_type) const
A recursive check that handles when assigning a source value to a target, is the assignment a loss of...
Definition
does_remove_const.cpp:114
does_remove_constt::does_remove_constt
does_remove_constt(const goto_programt &)
A naive analysis to look for casts that remove const-ness from pointers.
Definition
does_remove_const.cpp:20
does_remove_constt::operator()
std::pair< bool, source_locationt > operator()() const
A naive analysis to look for casts that remove const-ness from pointers.
Definition
does_remove_const.cpp:26
does_remove_constt::goto_program
const goto_programt & goto_program
Definition
does_remove_const.h:36
does_remove_constt::does_expr_lose_const
bool does_expr_lose_const(const exprt &expr) const
Search the expression tree to look for any children that have the same base type, but a less strict c...
Definition
does_remove_const.cpp:61
exprt
Base class for all expressions.
Definition
expr.h:57
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:68
exprt::type
typet & type()
Return the type of the expression.
Definition
expr.h:85
exprt::operands
operandst & operands()
Definition
expr.h:95
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition
goto_program.h:180
goto_programt::instructiont::assign_lhs
const exprt & assign_lhs() const
Get the lhs of the assignment for ASSIGN.
Definition
goto_program.h:199
goto_programt::instructiont::assign_rhs
const exprt & assign_rhs() const
Get the rhs of the assignment for ASSIGN.
Definition
goto_program.h:213
goto_programt::instructiont::is_assign
bool is_assign() const
Definition
goto_program.h:492
goto_programt::instructiont::source_location
const source_locationt & source_location() const
Definition
goto_program.h:332
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition
goto_program.h:72
irept::get_bool
bool get_bool(const irep_idt &name) const
Definition
irep.cpp:57
irept::id
const irep_idt & id() const
Definition
irep.h:388
source_locationt
Definition
source_location.h:20
typet
The type of an expression, extends irept.
Definition
type.h:29
does_remove_const.h
Analyses.
goto_program.h
Concrete Goto Program.
pointer_expr.h
API to expression classes for Pointers.
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition
pointer_expr.h:93
PRECONDITION
#define PRECONDITION(CONDITION)
Definition
invariant.h:463
analyses
does_remove_const.cpp
Generated by
1.17.0