cprover
does_remove_const.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3  Module: Analyses
4 
5  Author: DiffBlue Limited. All rights reserved.
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 #include <ansi-c/c_qualifiers.h>
20 
26  const goto_programt &goto_program,
27  const namespacet &ns):
28  goto_program(goto_program),
29  ns(ns)
30 {}
31 
35 {
36  for(const goto_programt::instructiont &instruction :
38  {
39  if(!instruction.is_assign())
40  {
41  continue;
42  }
43 
44  const code_assignt &assign=to_code_assign(instruction.code);
45  const typet &rhs_type=assign.rhs().type();
46  const typet &lhs_type=assign.lhs().type();
47 
48  // Compare the types recursively for a point where the rhs is more
49  // const that the lhs
50  if(!does_type_preserve_const_correctness(&lhs_type, &rhs_type))
51  {
52  return true;
53  }
54 
55  if(does_expr_lose_const(assign.rhs()))
56  {
57  return true;
58  }
59  }
60 
61  return false;
62 }
63 
71 {
72  const typet &root_type=expr.type();
73 
74  // Look in each child that has the same base type as the root
75  for(const exprt &op : expr.operands())
76  {
77  const typet &op_type=op.type();
78  if(base_type_eq(op_type, root_type, ns))
79  {
80  // Is this child more const-qualified than the root
81  if(!does_type_preserve_const_correctness(&root_type, &op_type))
82  {
83  return true;
84  }
85  }
86 
87  // Recursively check the children of this child
88  if(does_expr_lose_const(op))
89  {
90  return true;
91  }
92  }
93  return false;
94 }
95 
124  const typet *target_type, const typet *source_type) const
125 {
126  while(target_type->id()==ID_pointer)
127  {
128  bool direct_subtypes_at_least_as_const=
130  target_type->subtype(), source_type->subtype());
131  // We have a pointer to something, but the thing it is pointing to can't be
132  // modified normally, but can through this pointer
133  if(!direct_subtypes_at_least_as_const)
134  return false;
135  // Check the subtypes if they are pointers
136  target_type=&target_type->subtype();
137  source_type=&source_type->subtype();
138  }
139  return true;
140 }
141 
164  const typet &type_more_const, const typet &type_compare) const
165 {
166  const c_qualifierst type_compare_qualifiers(type_compare);
167  const c_qualifierst more_constant_qualifiers(type_more_const);
168  return !type_compare_qualifiers.is_constant ||
169  more_constant_qualifiers.is_constant;
170 }
The type of an expression.
Definition: type.h:20
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Definition: base_type.cpp:270
instructionst instructions
The list of instructions in the goto program.
const namespacet & ns
typet & type()
Definition: expr.h:60
const goto_programt & goto_program
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:178
const irep_idt & id() const
Definition: irep.h:189
exprt & lhs()
Definition: std_code.h:157
exprt & rhs()
Definition: std_code.h:162
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:62
bool operator()() const
A naive analysis to look for casts that remove const-ness from pointers.
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 specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
Base class for all expressions.
Definition: expr.h:46
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:31
operandst & operands()
Definition: expr.h:70
Concrete Goto Program.
Assignment.
Definition: std_code.h:144