Skip to content

Commit 1e25c00

Browse files
committed
Fix variable initialization order in snapshot-harness aliasing pointers
The root cause was in the topological sort implementation. The `dfs()` method enforced that seen and inserted sets must be empty on entry (via `PRECONDITION`) and would clear them on exit. However, `topological_sort()` calls `dfs()` multiple times in a loop for each item in the input collection. This meant only the first item was sorted correctly; subsequent items would fail the precondition or produce incorrect results. The fix moves the set clearing logic to the beginning of `topological_sort()`, ensuring a fresh DFS traversal for the entire collection while allowing the DFS to maintain state across recursive calls within a single item's dependency graph. Co-authored-by: Kiro autonomous agent Fixes: #4978
1 parent 76dd20f commit 1e25c00

File tree

3 files changed

+3
-5
lines changed

3 files changed

+3
-5
lines changed

regression/snapshot-harness/dynamic-array-int-ordering/test.desc

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,3 @@
1-
KNOWNBUG
21
main.c
32
a,a1,iterator1,a2,a3,iterator2,a4,a5,iterator3,a6,a7,array2,a8 --harness-type initialize-with-memory-snapshot --initial-goto-location main:4
43
^EXIT=10$

regression/snapshot-harness/dynamic-array-int/test.desc

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,3 @@
1-
KNOWNBUG
21
main.c
32
array,iterator1,iterator2,iterator3 --harness-type initialize-with-memory-snapshot --initial-goto-location main:4
43
^EXIT=10$

src/goto-harness/memory_snapshot_harness_generator.h

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -324,6 +324,9 @@ class memory_snapshot_harness_generatort : public goto_harness_generatort
324324
auto push_to_output = [&output](const valuet &value) {
325325
output.push_back(value);
326326
};
327+
// Clear the sets before starting the sort to ensure a fresh traversal
328+
seen.clear();
329+
inserted.clear();
327330
for(const auto &item : input)
328331
{
329332
dfs(item, associate_key_with_t, push_to_output);
@@ -339,10 +342,7 @@ class memory_snapshot_harness_generatort : public goto_harness_generatort
339342
template <typename Value, typename Map, typename Handler>
340343
void dfs(Value &&node, Map &&key_to_t, Handler &&handle)
341344
{
342-
PRECONDITION(seen.empty() && inserted.empty());
343345
dfs_inner(node, key_to_t, handle);
344-
seen.clear();
345-
inserted.clear();
346346
}
347347

348348
template <typename Value, typename Map, typename Handler>

0 commit comments

Comments
 (0)