Skip to content

Commit d7776db

Browse files
committed
Replace maybe_symbol with specific tighter scoped variables
This ensures that the variable is only in scope when it is non-null.
1 parent 26b5184 commit d7776db

File tree

1 file changed

+6
-8
lines changed

1 file changed

+6
-8
lines changed

src/goto-programs/mm_io.cpp

Lines changed: 6 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -118,25 +118,23 @@ void mm_io(symbol_tablet &symbol_table, goto_functionst &goto_functions)
118118
const irep_idt id_r = CPROVER_PREFIX "mm_io_r";
119119
const irep_idt id_w = CPROVER_PREFIX "mm_io_w";
120120

121-
auto maybe_symbol=symbol_table.lookup(id_r);
122-
if(maybe_symbol)
121+
if(const auto mm_io_r_symbol = symbol_table.lookup(id_r))
123122
{
124-
mm_io_r=maybe_symbol->symbol_expr();
123+
mm_io_r = mm_io_r_symbol->symbol_expr();
125124

126125
const auto &value_symbol = get_fresh_aux_symbol(
127126
to_code_type(mm_io_r.type()).return_type(),
128127
id2string(id_r) + "$value",
129128
id2string(id_r) + "$value",
130-
maybe_symbol->location,
131-
maybe_symbol->mode,
129+
mm_io_r_symbol->location,
130+
mm_io_r_symbol->mode,
132131
symbol_table);
133132

134133
mm_io_r_value = value_symbol.symbol_expr();
135134
}
136135

137-
maybe_symbol=symbol_table.lookup(id_w);
138-
if(maybe_symbol)
139-
mm_io_w=maybe_symbol->symbol_expr();
136+
if(const auto mm_io_w_symbol = symbol_table.lookup(id_w))
137+
mm_io_w = mm_io_w_symbol->symbol_expr();
140138

141139
for(auto & f : goto_functions.function_map)
142140
mm_io(mm_io_r, mm_io_r_value, mm_io_w, f.second, ns);

0 commit comments

Comments
 (0)