Skip to content

Commit 34c54a6

Browse files
committed
Fix the ordering in which symbols are initialised
In memory-snapshot-harness: so that pointer to objects are initialised after those objects.
1 parent 9037d49 commit 34c54a6

File tree

2 files changed

+23
-2
lines changed

2 files changed

+23
-2
lines changed

src/goto-harness/memory_snapshot_harness_generator.cpp

Lines changed: 17 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -207,6 +207,18 @@ size_t memory_snapshot_harness_generatort::pointer_depth(const typet &t) const
207207
return pointer_depth(t.subtype()) + 1;
208208
}
209209

210+
bool memory_snapshot_harness_generatort::refers_to(
211+
const exprt &expr,
212+
const irep_idt &name) const
213+
{
214+
if(expr.id() == ID_symbol)
215+
return to_symbol_expr(expr).get_identifier() == name;
216+
return std::any_of(
217+
expr.operands().begin(),
218+
expr.operands().end(),
219+
[this, name](const exprt &subexpr) { return refers_to(subexpr, name); });
220+
}
221+
210222
code_blockt memory_snapshot_harness_generatort::add_assignments_to_globals(
211223
const symbol_tablet &snapshot,
212224
goto_modelt &goto_model) const
@@ -230,8 +242,11 @@ code_blockt memory_snapshot_harness_generatort::add_assignments_to_globals(
230242
ordered_snapshot_symbols.begin(),
231243
ordered_snapshot_symbols.end(),
232244
[this](const snapshot_pairt &left, const snapshot_pairt &right) {
233-
return pointer_depth(left.second.symbol_expr().type()) <
234-
pointer_depth(right.second.symbol_expr().type());
245+
if(refers_to(right.second.value, left.first))
246+
return true;
247+
else
248+
return pointer_depth(left.second.symbol_expr().type()) <
249+
pointer_depth(right.second.symbol_expr().type());
235250
});
236251

237252
code_blockt code;

src/goto-harness/memory_snapshot_harness_generator.h

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -244,6 +244,12 @@ class memory_snapshot_harness_generatort : public goto_harness_generatort
244244
/// \return pointer depth of type \p t
245245
size_t pointer_depth(const typet &t) const;
246246

247+
/// Recursively test pointer reference
248+
/// \param expr: expression to be tested
249+
/// \param name: name to be located
250+
/// \return true if \p expr refers to an object named \p name
251+
bool refers_to(const exprt &expr, const irep_idt &name) const;
252+
247253
/// data to store the command-line options
248254
std::string memory_snapshot_file;
249255
std::string initial_goto_location_line;

0 commit comments

Comments
 (0)