@@ -11,6 +11,7 @@ Author: Diffblue Ltd
11
11
12
12
#include " local_safe_pointers.h"
13
13
14
+ #include < util/base_type.h>
14
15
#include < util/expr_iterator.h>
15
16
#include < util/expr_util.h>
16
17
#include < util/format_expr.h>
@@ -81,7 +82,8 @@ static optionalt<goto_null_checkt> get_null_checked_expr(const exprt &expr)
81
82
// / \param goto_program: program to analyse
82
83
void local_safe_pointerst::operator ()(const goto_programt &goto_program)
83
84
{
84
- std::set<exprt, type_comparet> checked_expressions (type_comparet{});
85
+ std::set<exprt, base_type_comparet> checked_expressions (
86
+ base_type_comparet{ns});
85
87
86
88
for (const auto &instruction : goto_program.instructions )
87
89
{
@@ -96,7 +98,8 @@ void local_safe_pointerst::operator()(const goto_programt &goto_program)
96
98
checked_expressions = findit->second ;
97
99
else
98
100
{
99
- checked_expressions = std::set<exprt, type_comparet>(type_comparet{});
101
+ checked_expressions =
102
+ std::set<exprt, base_type_comparet>(base_type_comparet{ns});
100
103
}
101
104
}
102
105
@@ -176,11 +179,8 @@ void local_safe_pointerst::operator()(const goto_programt &goto_program)
176
179
// / \param out: stream to write output to
177
180
// / \param goto_program: GOTO program analysed (the same one passed to
178
181
// / operator())
179
- // / \param ns: namespace
180
182
void local_safe_pointerst::output (
181
- std::ostream &out,
182
- const goto_programt &goto_program,
183
- const namespacet &ns)
183
+ std::ostream &out, const goto_programt &goto_program)
184
184
{
185
185
forall_goto_program_instructions (i_it, goto_program)
186
186
{
@@ -220,11 +220,8 @@ void local_safe_pointerst::output(
220
220
// / \param out: stream to write output to
221
221
// / \param goto_program: GOTO program analysed (the same one passed to
222
222
// / operator())
223
- // / \param ns: namespace
224
223
void local_safe_pointerst::output_safe_dereferences (
225
- std::ostream &out,
226
- const goto_programt &goto_program,
227
- const namespacet &ns)
224
+ std::ostream &out, const goto_programt &goto_program)
228
225
{
229
226
forall_goto_program_instructions (i_it, goto_program)
230
227
{
@@ -241,17 +238,12 @@ void local_safe_pointerst::output_safe_dereferences(
241
238
out << " {" ;
242
239
bool first = true ;
243
240
i_it->apply ([&first, &out](const exprt &e) {
244
- for (auto subexpr_it = e.depth_begin (), subexpr_end = e.depth_end ();
245
- subexpr_it != subexpr_end;
246
- ++subexpr_it)
241
+ if (e.id () == ID_dereference)
247
242
{
248
- if (subexpr_it->id () == ID_dereference)
249
- {
250
- if (!first)
251
- out << " , " ;
252
- first = true ;
253
- format_rec (out, to_dereference_expr (*subexpr_it).pointer ());
254
- }
243
+ if (!first)
244
+ out << " , " ;
245
+ first = true ;
246
+ format_rec (out, to_dereference_expr (e).pointer ());
255
247
}
256
248
});
257
249
out << " }" ;
@@ -272,6 +264,17 @@ bool local_safe_pointerst::is_non_null_at_program_point(
272
264
auto findit = non_null_expressions.find (program_point->location_number );
273
265
if (findit == non_null_expressions.end ())
274
266
return false ;
267
+ const exprt *tocheck = &expr;
268
+ while (tocheck->id () == ID_typecast)
269
+ tocheck = &tocheck->op0 ();
270
+ return findit->second .count (*tocheck) != 0 ;
271
+ }
275
272
276
- return findit->second .count (skip_typecast (expr)) != 0 ;
273
+ bool local_safe_pointerst::base_type_comparet::operator ()(
274
+ const exprt &e1 , const exprt &e2 ) const
275
+ {
276
+ if (base_type_eq (e1 , e2 , ns))
277
+ return false ;
278
+ else
279
+ return e1 < e2 ;
277
280
}
0 commit comments