Skip to content

Commit dbff82c

Browse files
Petr BauchPetr Bauch
Petr Bauch
authored and
Petr Bauch
committed
Fix getting a fresh variable for memory harness tmps
Do not introduce symbols for types and do not disregard local temporaries.
1 parent 3675873 commit dbff82c

File tree

1 file changed

+17
-10
lines changed

1 file changed

+17
-10
lines changed

src/goto-harness/memory_snapshot_harness_generator.cpp

Lines changed: 17 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -228,22 +228,29 @@ code_blockt memory_snapshot_harness_generatort::add_assignments_to_globals(
228228
for(const auto &pair : snapshot)
229229
{
230230
const symbolt &snapshot_symbol = pair.second;
231-
if(!snapshot_symbol.is_static_lifetime)
232-
continue;
233-
234231
symbol_tablet &symbol_table = goto_model.symbol_table;
235-
const symbolt &symbol =
236-
(symbol_table.lookup(snapshot_symbol.base_name) != nullptr)
237-
? snapshot_symbol
238-
: fresh_symbol_copy(snapshot_symbol, symbol_table);
239232

240-
if(variables_to_havoc.count(symbol.base_name) == 0)
233+
auto should_get_fresh = [&symbol_table](const symbolt &symbol) {
234+
return symbol_table.lookup(symbol.base_name) == nullptr &&
235+
!symbol.is_type;
236+
};
237+
const symbolt &fresh_or_snapshot_symbol =
238+
should_get_fresh(snapshot_symbol)
239+
? fresh_symbol_copy(snapshot_symbol, symbol_table)
240+
: snapshot_symbol;
241+
242+
if(!fresh_or_snapshot_symbol.is_static_lifetime)
243+
continue;
244+
245+
if(variables_to_havoc.count(fresh_or_snapshot_symbol.base_name) == 0)
241246
{
242-
code.add(code_assignt{symbol.symbol_expr(), symbol.value});
247+
code.add(code_assignt{fresh_or_snapshot_symbol.symbol_expr(),
248+
fresh_or_snapshot_symbol.value});
243249
}
244250
else
245251
{
246-
recursive_initialization.initialize(symbol.symbol_expr(), 0, {}, code);
252+
recursive_initialization.initialize(
253+
fresh_or_snapshot_symbol.symbol_expr(), 0, {}, code);
247254
}
248255
}
249256
return code;

0 commit comments

Comments
 (0)