Skip to content

Commit 90b597b

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 226aee7 commit 90b597b

File tree

6 files changed

+24
-30
lines changed

6 files changed

+24
-30
lines changed

src/goto-symex/symex_dereference_state.cpp

Lines changed: 9 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -26,11 +26,9 @@ Author: Daniel Kroening, [email protected]
2626
/// already exist.
2727
///
2828
/// \param expr: expression to get or create a failed symbol for
29-
/// \param [out] symbol: failed symbol result
30-
/// \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)
29+
/// \return pointer to the failed symbol for \p expr, or nullptr if none
30+
const symbolt *symex_dereference_statet::get_or_create_failed_symbol(
31+
const exprt &expr)
3432
{
3533
const namespacet &ns=goto_symex.ns;
3634

@@ -39,13 +37,14 @@ bool symex_dereference_statet::get_or_create_failed_symbol(
3937
{
4038
const ssa_exprt &ssa_expr=to_ssa_expr(expr);
4139
if(ssa_expr.get_original_expr().id()!=ID_symbol)
42-
return false;
40+
return nullptr;
4341

4442
const symbolt &ptr_symbol=
4543
ns.lookup(to_ssa_expr(expr).get_object_name());
4644

4745
const irep_idt &failed_symbol = ptr_symbol.type.get(ID_C_failed_symbol);
4846

47+
const symbolt *symbol;
4948
if(failed_symbol!="" &&
5049
!ns.lookup(failed_symbol, symbol))
5150
{
@@ -55,8 +54,7 @@ bool symex_dereference_statet::get_or_create_failed_symbol(
5554
state.rename(sym_expr, ns, goto_symex_statet::L1);
5655
sym.name=to_ssa_expr(sym_expr).get_identifier();
5756
state.symbol_table.move(sym, sym_ptr);
58-
symbol=sym_ptr;
59-
return true;
57+
return sym_ptr;
6058
}
6159
}
6260
else if(expr.id()==ID_symbol)
@@ -66,6 +64,7 @@ bool symex_dereference_statet::get_or_create_failed_symbol(
6664

6765
const irep_idt &failed_symbol = ptr_symbol.type.get(ID_C_failed_symbol);
6866

67+
const symbolt *symbol;
6968
if(failed_symbol!="" &&
7069
!ns.lookup(failed_symbol, symbol))
7170
{
@@ -75,12 +74,11 @@ bool symex_dereference_statet::get_or_create_failed_symbol(
7574
state.rename(sym_expr, ns, goto_symex_statet::L1);
7675
sym.name=to_ssa_expr(sym_expr).get_identifier();
7776
state.symbol_table.move(sym, sym_ptr);
78-
symbol=sym_ptr;
79-
return true;
77+
return sym_ptr;
8078
}
8179
}
8280

83-
return false;
81+
return nullptr;
8482
}
8583

8684
/// 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: 9 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -20,30 +20,28 @@ Author: Daniel Kroening, [email protected]
2020
#include <util/options.h>
2121

2222
/// \param expr: expression to check
23-
/// \param [out] symbol: symbol which gets assigned the value from the
24-
/// `failed_symbol` comment
25-
/// \return true when `expr` is a symbol, whose type contains a `failed_symbol`
26-
/// comment which exists in the namespace.
27-
bool goto_program_dereferencet::get_or_create_failed_symbol(
28-
const exprt &expr,
29-
const symbolt *&symbol)
23+
/// \return pointer to appropriate failed symbol for \p expr, or nullptr if none
24+
const symbolt *
25+
goto_program_dereferencet::get_or_create_failed_symbol(const exprt &expr)
3026
{
3127
if(expr.id()==ID_symbol)
3228
{
3329
if(expr.get_bool(ID_C_invalid_object))
34-
return false;
30+
return nullptr;
3531

3632
const symbolt &ptr_symbol = ns.lookup(to_symbol_expr(expr));
3733

3834
const irep_idt &failed_symbol = ptr_symbol.type.get(ID_C_failed_symbol);
3935

4036
if(failed_symbol.empty())
41-
return false;
37+
return nullptr;
4238

43-
return !ns.lookup(failed_symbol, symbol);
39+
const symbolt *symbol = nullptr;
40+
ns.lookup(failed_symbol, symbol);
41+
return symbol;
4442
}
4543

46-
return false;
44+
return nullptr;
4745
}
4846

4947
/// \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: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -122,10 +122,11 @@ exprt value_set_dereferencet::dereference(
122122
{
123123
// first see if we have a "failed object" for this pointer
124124

125-
const symbolt *failed_symbol;
126125
exprt failure_value;
127126

128-
if(dereference_callback.get_or_create_failed_symbol(pointer, failed_symbol))
127+
if(
128+
const symbolt *failed_symbol =
129+
dereference_callback.get_or_create_failed_symbol(pointer))
129130
{
130131
// yes!
131132
failure_value=failed_symbol->symbol_expr();

0 commit comments

Comments
 (0)