CBMC
Loading...
Searching...
No Matches
does_remove_const.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Analyses
4
5Author: Diffblue Ltd.
6
7\*******************************************************************/
8
11
12#include "does_remove_const.h"
13
15
16#include <util/pointer_expr.h>
17
21 : goto_program(goto_program)
22{}
23
26std::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
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
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
73 {
74 return true;
75 }
76 }
77
78 // Recursively check the children of this child
80 {
81 return true;
82 }
83 }
84 return false;
85}
86
115 const typet *target_type, const typet *source_type) const
116{
117 while(target_type->id()==ID_pointer)
118 {
120
121 const auto &target_pointer_type = to_pointer_type(*target_type);
123
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
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
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
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.
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...
does_remove_constt(const goto_programt &)
A naive analysis to look for casts that remove const-ness from pointers.
std::pair< bool, source_locationt > operator()() const
A naive analysis to look for casts that remove const-ness from pointers.
const goto_programt & goto_program
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...
Base class for all expressions.
Definition expr.h:56
typet & type()
Return the type of the expression.
Definition expr.h:84
operandst & operands()
Definition expr.h:94
This class represents an instruction in the GOTO intermediate representation.
A generic container class for the GOTO intermediate representation of one function.
const irep_idt & id() const
Definition irep.h:388
The type of an expression, extends irept.
Definition type.h:29
Concrete Goto Program.
API to expression classes for Pointers.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
#define PRECONDITION(CONDITION)
Definition invariant.h:463