cprover
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 #include <util/type.h>
16 #include <util/std_code.h>
17 #include <util/base_type.h>
18 
24  const goto_programt &goto_program,
25  const namespacet &ns):
26  goto_program(goto_program),
27  ns(ns)
28 {}
29 
32 std::pair<bool, source_locationt> does_remove_constt::operator()() const
33 {
34  for(const goto_programt::instructiont &instruction :
36  {
37  if(!instruction.is_assign())
38  {
39  continue;
40  }
41 
42  const code_assignt &assign = instruction.get_assign();
43  const typet &rhs_type=assign.rhs().type();
44  const typet &lhs_type=assign.lhs().type();
45 
46  // Compare the types recursively for a point where the rhs is more
47  // const that the lhs
48  if(!does_type_preserve_const_correctness(&lhs_type, &rhs_type))
49  {
50  return {true, assign.find_source_location()};
51  }
52 
53  if(does_expr_lose_const(assign.rhs()))
54  {
55  return {true, assign.rhs().find_source_location()};
56  }
57  }
58 
59  return {false, source_locationt()};
60 }
61 
69 {
70  const typet &root_type=expr.type();
71 
72  // Look in each child that has the same base type as the root
73  for(const exprt &op : expr.operands())
74  {
75  const typet &op_type=op.type();
76  if(base_type_eq(op_type, root_type, ns))
77  {
78  // Is this child more const-qualified than the root
79  if(!does_type_preserve_const_correctness(&root_type, &op_type))
80  {
81  return true;
82  }
83  }
84 
85  // Recursively check the children of this child
86  if(does_expr_lose_const(op))
87  {
88  return true;
89  }
90  }
91  return false;
92 }
93 
122  const typet *target_type, const typet *source_type) const
123 {
124  while(target_type->id()==ID_pointer)
125  {
126  bool direct_subtypes_at_least_as_const=
128  target_type->subtype(), source_type->subtype());
129  // We have a pointer to something, but the thing it is pointing to can't be
130  // modified normally, but can through this pointer
131  if(!direct_subtypes_at_least_as_const)
132  return false;
133  // Check the subtypes if they are pointers
134  target_type=&target_type->subtype();
135  source_type=&source_type->subtype();
136  }
137  return true;
138 }
139 
162  const typet &type_more_const, const typet &type_compare) const
163 {
164  return !type_compare.get_bool(ID_C_constant) ||
165  type_more_const.get_bool(ID_C_constant);
166 }
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Check types for equality across all levels of hierarchy.
Definition: base_type.cpp:290
Base Type Computation.
A codet representing an assignment in the program.
Definition: std_code.h:293
exprt & rhs()
Definition: std_code.h:315
exprt & lhs()
Definition: std_code.h:310
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 &goto_program, const namespacet &ns)
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...
const namespacet & ns
Base class for all expressions.
Definition: expr.h:54
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
Definition: expr.cpp:165
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:92
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:178
const code_assignt & get_assign() const
Get the assignment for ASSIGN.
Definition: goto_program.h:198
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:71
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:652
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:58
const irep_idt & id() const
Definition: irep.h:407
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
The type of an expression, extends irept.
Definition: type.h:28
const typet & subtype() const
Definition: type.h:47
Concrete Goto Program.
Defines typet, type_with_subtypet and type_with_subtypest.