Skip to content

Commit 3ab2c1f

Browse files
committed
Replace redundant pointer-and-boolean with just a pointer
It's already implicit in a bare pointer (rather than a reference) that it could be null, so let's just use that to express whether we have an answer or not.
1 parent 7ff4fbd commit 3ab2c1f

6 files changed

+23
-24
lines changed

src/goto-symex/symex_dereference_state.cpp

Lines changed: 8 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -28,9 +28,8 @@ Author: Daniel Kroening, [email protected]
2828
/// \param expr: expression to get or create a failed symbol for
2929
/// \param [out] symbol: failed symbol result
3030
/// \return true if we populated \p symbol
31-
bool symex_dereference_statet::get_or_create_failed_symbol(
32-
const exprt &expr,
33-
const symbolt *&symbol)
31+
const symbolt *symex_dereference_statet::get_or_create_failed_symbol(
32+
const exprt &expr)
3433
{
3534
const namespacet &ns=goto_symex.ns;
3635

@@ -39,13 +38,14 @@ bool symex_dereference_statet::get_or_create_failed_symbol(
3938
{
4039
const ssa_exprt &ssa_expr=to_ssa_expr(expr);
4140
if(ssa_expr.get_original_expr().id()!=ID_symbol)
42-
return false;
41+
return nullptr;
4342

4443
const symbolt &ptr_symbol=
4544
ns.lookup(to_ssa_expr(expr).get_object_name());
4645

4746
const irep_idt &failed_symbol = ptr_symbol.type.get(ID_C_failed_symbol);
4847

48+
const symbolt *symbol;
4949
if(failed_symbol!="" &&
5050
!ns.lookup(failed_symbol, symbol))
5151
{
@@ -55,8 +55,7 @@ bool symex_dereference_statet::get_or_create_failed_symbol(
5555
state.rename(sym_expr, ns, goto_symex_statet::L1);
5656
sym.name=to_ssa_expr(sym_expr).get_identifier();
5757
state.symbol_table.move(sym, sym_ptr);
58-
symbol=sym_ptr;
59-
return true;
58+
return sym_ptr;
6059
}
6160
}
6261
else if(expr.id()==ID_symbol)
@@ -66,6 +65,7 @@ bool symex_dereference_statet::get_or_create_failed_symbol(
6665

6766
const irep_idt &failed_symbol = ptr_symbol.type.get(ID_C_failed_symbol);
6867

68+
const symbolt *symbol;
6969
if(failed_symbol!="" &&
7070
!ns.lookup(failed_symbol, symbol))
7171
{
@@ -75,12 +75,11 @@ bool symex_dereference_statet::get_or_create_failed_symbol(
7575
state.rename(sym_expr, ns, goto_symex_statet::L1);
7676
sym.name=to_ssa_expr(sym_expr).get_identifier();
7777
state.symbol_table.move(sym, sym_ptr);
78-
symbol=sym_ptr;
79-
return true;
78+
return sym_ptr;
8079
}
8180
}
8281

83-
return false;
82+
return nullptr;
8483
}
8584

8685
/// Just forwards a value-set query to `state.value_set`

src/goto-symex/symex_dereference_state.h

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -39,8 +39,7 @@ class symex_dereference_statet:
3939
void get_value_set(const exprt &expr, value_setst::valuest &value_set)
4040
const override;
4141

42-
bool get_or_create_failed_symbol(const exprt &expr, const symbolt *&symbol)
43-
override;
42+
const symbolt *get_or_create_failed_symbol(const exprt &expr) override;
4443
};
4544

4645
#endif // CPROVER_GOTO_SYMEX_SYMEX_DEREFERENCE_STATE_H

src/pointer-analysis/dereference_callback.h

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -32,8 +32,7 @@ class dereference_callbackt
3232
virtual void
3333
get_value_set(const exprt &expr, value_setst::valuest &value_set) const = 0;
3434

35-
virtual bool
36-
get_or_create_failed_symbol(const exprt &expr, const symbolt *&symbol) = 0;
35+
virtual const symbolt *get_or_create_failed_symbol(const exprt &expr) = 0;
3736
};
3837

3938
#endif // CPROVER_POINTER_ANALYSIS_DEREFERENCE_CALLBACK_H

src/pointer-analysis/goto_program_dereference.cpp

Lines changed: 8 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -24,26 +24,27 @@ Author: Daniel Kroening, [email protected]
2424
/// `failed_symbol` comment
2525
/// \return true when `expr` is a symbol, whose type contains a `failed_symbol`
2626
/// comment which exists in the namespace.
27-
bool goto_program_dereferencet::get_or_create_failed_symbol(
28-
const exprt &expr,
29-
const symbolt *&symbol)
27+
const symbolt *goto_program_dereferencet::get_or_create_failed_symbol(
28+
const exprt &expr)
3029
{
3130
if(expr.id()==ID_symbol)
3231
{
3332
if(expr.get_bool(ID_C_invalid_object))
34-
return false;
33+
return nullptr;
3534

3635
const symbolt &ptr_symbol = ns.lookup(to_symbol_expr(expr));
3736

3837
const irep_idt &failed_symbol = ptr_symbol.type.get(ID_C_failed_symbol);
3938

4039
if(failed_symbol.empty())
41-
return false;
40+
return nullptr;
4241

43-
return !ns.lookup(failed_symbol, symbol);
42+
const symbolt *symbol = nullptr;
43+
ns.lookup(failed_symbol, symbol);
44+
return symbol;
4445
}
4546

46-
return false;
47+
return nullptr;
4748
}
4849

4950
/// \deprecated

src/pointer-analysis/goto_program_dereference.h

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -69,8 +69,7 @@ class goto_program_dereferencet:protected dereference_callbackt
6969
DEPRECATED("Unused")
7070
virtual bool is_valid_object(const irep_idt &identifier);
7171

72-
bool get_or_create_failed_symbol(const exprt &expr, const symbolt *&symbol)
73-
override;
72+
const symbolt *get_or_create_failed_symbol(const exprt &expr) override;
7473

7574
DEPRECATED("Unused")
7675
virtual void dereference_failure(

src/pointer-analysis/value_set_dereference.cpp

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -122,10 +122,12 @@ exprt value_set_dereferencet::dereference(
122122
{
123123
// first see if we have a "failed object" for this pointer
124124

125-
const symbolt *failed_symbol;
125+
126126
exprt failure_value;
127127

128-
if(dereference_callback.get_or_create_failed_symbol(pointer, failed_symbol))
128+
if(
129+
const symbolt *failed_symbol =
130+
dereference_callback.get_or_create_failed_symbol(pointer))
129131
{
130132
// yes!
131133
failure_value=failed_symbol->symbol_expr();

0 commit comments

Comments
 (0)