CBMC
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 
15 
16 #include <util/pointer_expr.h>
17 #include <util/std_code.h>
18 
22  : goto_program(goto_program)
23 {}
24 
27 std::pair<bool, source_locationt> does_remove_constt::operator()() const
28 {
29  for(const goto_programt::instructiont &instruction :
31  {
32  if(!instruction.is_assign())
33  {
34  continue;
35  }
36 
37  const typet &rhs_type = instruction.assign_rhs().type();
38  const typet &lhs_type = instruction.assign_lhs().type();
39 
40  // Compare the types recursively for a point where the rhs is more
41  // const that the lhs
42  if(!does_type_preserve_const_correctness(&lhs_type, &rhs_type))
43  {
44  return {true, instruction.source_location()};
45  }
46 
47  if(does_expr_lose_const(instruction.assign_rhs()))
48  {
49  return {true, instruction.assign_rhs().find_source_location()};
50  }
51  }
52 
53  return {false, source_locationt()};
54 }
55 
63 {
64  const typet &root_type=expr.type();
65 
66  // Look in each child that has the same type as the root
67  for(const exprt &op : expr.operands())
68  {
69  const typet &op_type=op.type();
70  if(op_type == root_type)
71  {
72  // Is this child more const-qualified than the root
73  if(!does_type_preserve_const_correctness(&root_type, &op_type))
74  {
75  return true;
76  }
77  }
78 
79  // Recursively check the children of this child
80  if(does_expr_lose_const(op))
81  {
82  return true;
83  }
84  }
85  return false;
86 }
87 
116  const typet *target_type, const typet *source_type) const
117 {
118  while(target_type->id()==ID_pointer)
119  {
120  PRECONDITION(source_type->id() == ID_pointer);
121 
122  const auto &target_pointer_type = to_pointer_type(*target_type);
123  const auto &source_pointer_type = to_pointer_type(*source_type);
124 
125  bool direct_subtypes_at_least_as_const = is_type_at_least_as_const_as(
126  target_pointer_type.base_type(), source_pointer_type.base_type());
127  // We have a pointer to something, but the thing it is pointing to can't be
128  // modified normally, but can through this pointer
129  if(!direct_subtypes_at_least_as_const)
130  return false;
131  // Check the subtypes if they are pointers
132  target_type = &target_pointer_type.base_type();
133  source_type = &source_pointer_type.base_type();
134  }
135  return true;
136 }
137 
160  const typet &type_more_const, const typet &type_compare) const
161 {
162  return !type_compare.get_bool(ID_C_constant) ||
163  type_more_const.get_bool(ID_C_constant);
164 }
typet
The type of an expression, extends irept.
Definition: type.h:28
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:27
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:62
exprt
Base class for all expressions.
Definition: expr.h:55
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:115
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:159
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:84
goto_programt::instructiont::source_location
const source_locationt & source_location() const
Definition: goto_program.h:340
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
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:165
pointer_expr.h
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:79
irept::id
const irep_idt & id() const
Definition: irep.h:396
goto_programt::instructiont::assign_rhs
const exprt & assign_rhs() const
Get the rhs of the assignment for ASSIGN.
Definition: goto_program.h:221
std_code.h
goto_program.h
source_locationt
Definition: source_location.h:18
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:592
does_remove_const.h
goto_programt::instructiont::assign_lhs
const exprt & assign_lhs() const
Get the lhs of the assignment for ASSIGN.
Definition: goto_program.h:207
goto_programt::instructiont::is_assign
bool is_assign() const
Definition: goto_program.h:465
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
exprt::operands
operandst & operands()
Definition: expr.h:94
does_remove_constt::goto_program
const goto_programt & goto_program
Definition: does_remove_const.h:36
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:180
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:21
irept::get_bool
bool get_bool(const irep_idt &name) const
Definition: irep.cpp:58