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/expr.h>
17 #include <util/std_code.h>
18 #include <util/base_type.h>
19 
26  const namespacet &ns):
28  ns(ns)
29 {}
30 
33 std::pair<bool, source_locationt> does_remove_constt::operator()() const
34 {
35  for(const goto_programt::instructiont &instruction :
37  {
38  if(!instruction.is_assign())
39  {
40  continue;
41  }
42 
43  const code_assignt &assign=to_code_assign(instruction.code);
44  const typet &rhs_type=assign.rhs().type();
45  const typet &lhs_type=assign.lhs().type();
46 
47  // Compare the types recursively for a point where the rhs is more
48  // const that the lhs
49  if(!does_type_preserve_const_correctness(&lhs_type, &rhs_type))
50  {
51  return {true, assign.find_source_location()};
52  }
53 
54  if(does_expr_lose_const(assign.rhs()))
55  {
56  return {true, assign.rhs().find_source_location()};
57  }
58  }
59 
60  return {false, source_locationt()};
61 }
62 
70 {
71  const typet &root_type=expr.type();
72 
73  // Look in each child that has the same base type as the root
74  for(const exprt &op : expr.operands())
75  {
76  const typet &op_type=op.type();
77  if(base_type_eq(op_type, root_type, ns))
78  {
79  // Is this child more const-qualified than the root
80  if(!does_type_preserve_const_correctness(&root_type, &op_type))
81  {
82  return true;
83  }
84  }
85 
86  // Recursively check the children of this child
87  if(does_expr_lose_const(op))
88  {
89  return true;
90  }
91  }
92  return false;
93 }
94 
123  const typet *target_type, const typet *source_type) const
124 {
125  while(target_type->id()==ID_pointer)
126  {
127  bool direct_subtypes_at_least_as_const=
129  target_type->subtype(), source_type->subtype());
130  // We have a pointer to something, but the thing it is pointing to can't be
131  // modified normally, but can through this pointer
132  if(!direct_subtypes_at_least_as_const)
133  return false;
134  // Check the subtypes if they are pointers
135  target_type=&target_type->subtype();
136  source_type=&source_type->subtype();
137  }
138  return true;
139 }
140 
163  const typet &type_more_const, const typet &type_compare) const
164 {
165  return !type_compare.get_bool(ID_C_constant) ||
166  type_more_const.get_bool(ID_C_constant);
167 }
The type of an expression.
Definition: type.h:22
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Definition: base_type.cpp:326
const namespacet & ns
typet & type()
Definition: expr.h:56
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:240
const goto_programt & goto_program
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:173
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:240
const irep_idt & id() const
Definition: irep.h:259
exprt & lhs()
Definition: std_code.h:209
exprt & rhs()
Definition: std_code.h:214
const source_locationt & find_source_location() const
Definition: expr.cpp:246
std::pair< bool, source_locationt > operator()() const
A naive analysis to look for casts that remove const-ness from pointers.
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:403
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...
TO_BE_DOCUMENTED.
Definition: namespace.h:74
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...
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:70
Base class for all expressions.
Definition: expr.h:42
goto_programt & goto_program
Definition: cover.cpp:63
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. ...
does_remove_constt(const goto_programt &goto_program, const namespacet &ns)
A naive analysis to look for casts that remove const-ness from pointers.
Base Type Computation.
const typet & subtype() const
Definition: type.h:33
operandst & operands()
Definition: expr.h:66
Concrete Goto Program.
Assignment.
Definition: std_code.h:196