Skip to content

Commit af6bd9c

Browse files
Replace guardt in dereference_failure by exprt
This was immediately converted to an exprt anyway, so doesn't need to be a guardt specifically.
1 parent 85a901b commit af6bd9c

File tree

2 files changed

+2
-6
lines changed

2 files changed

+2
-6
lines changed

src/pointer-analysis/goto_program_dereference.cpp

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -68,10 +68,8 @@ bool goto_program_dereferencet::is_valid_object(
6868
void goto_program_dereferencet::dereference_failure(
6969
const std::string &property,
7070
const std::string &msg,
71-
const guardt &guard)
71+
exprt guard_expr)
7272
{
73-
exprt guard_expr=guard.as_expr();
74-
7573
if(assertions.insert(guard_expr).second)
7674
{
7775
guard_expr = boolean_negate(guard_expr);

src/pointer-analysis/goto_program_dereference.h

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -19,8 +19,6 @@ Author: Daniel Kroening, [email protected]
1919
#include "value_sets.h"
2020
#include "value_set_dereference.h"
2121

22-
class guardt;
23-
2422
/// Wrapper for functions removing dereferences in expressions contained in
2523
/// a goto program.
2624
class goto_program_dereferencet:protected dereference_callbackt
@@ -77,7 +75,7 @@ class goto_program_dereferencet:protected dereference_callbackt
7775
virtual void dereference_failure(
7876
const std::string &property,
7977
const std::string &msg,
80-
const guardt &guard);
78+
exprt guard_expr);
8179

8280
void
8381
get_value_set(const exprt &expr, value_setst::valuest &dest) const override;

0 commit comments

Comments
 (0)