From f154c3ec1a916501e6efb847bd5ff21a793b06f6 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 9 Dec 2025 10:48:32 +0000 Subject: [PATCH] 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 --- .../snapshot-harness/dynamic-array-int-ordering/test.desc | 4 +--- regression/snapshot-harness/dynamic-array-int/test.desc | 5 +---- src/goto-harness/memory_snapshot_harness_generator.h | 6 +++--- 3 files changed, 5 insertions(+), 10 deletions(-) diff --git a/regression/snapshot-harness/dynamic-array-int-ordering/test.desc b/regression/snapshot-harness/dynamic-array-int-ordering/test.desc index cc65ba43d83..7164950c762 100644 --- a/regression/snapshot-harness/dynamic-array-int-ordering/test.desc +++ b/regression/snapshot-harness/dynamic-array-int-ordering/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE main.c a,a1,iterator1,a2,a3,iterator2,a4,a5,iterator3,a6,a7,array2,a8 --harness-type initialize-with-memory-snapshot --initial-goto-location main:4 ^EXIT=10$ @@ -14,5 +14,3 @@ a,a1,iterator1,a2,a3,iterator2,a4,a5,iterator3,a6,a7,array2,a8 --harness-type in VERIFICATION FAILED -- unwinding assertion loop \d+: FAILURE --- -For more information take a look at github#5351 diff --git a/regression/snapshot-harness/dynamic-array-int/test.desc b/regression/snapshot-harness/dynamic-array-int/test.desc index 3178475a0ba..0395cff2ea1 100644 --- a/regression/snapshot-harness/dynamic-array-int/test.desc +++ b/regression/snapshot-harness/dynamic-array-int/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE main.c array,iterator1,iterator2,iterator3 --harness-type initialize-with-memory-snapshot --initial-goto-location main:4 ^EXIT=10$ @@ -14,6 +14,3 @@ array,iterator1,iterator2,iterator3 --harness-type initialize-with-memory-snapsh VERIFICATION FAILED -- unwinding assertion loop \d+: FAILURE --- -Broken by https://github.com/diffblue/cbmc/issues/4978 -For more information take a look at github#5351 diff --git a/src/goto-harness/memory_snapshot_harness_generator.h b/src/goto-harness/memory_snapshot_harness_generator.h index 52a51fc2560..aa60431263f 100644 --- a/src/goto-harness/memory_snapshot_harness_generator.h +++ b/src/goto-harness/memory_snapshot_harness_generator.h @@ -324,6 +324,9 @@ class memory_snapshot_harness_generatort : public goto_harness_generatort auto push_to_output = [&output](const valuet &value) { output.push_back(value); }; + // Clear the sets before starting the sort to ensure a fresh traversal + seen.clear(); + inserted.clear(); for(const auto &item : input) { dfs(item, associate_key_with_t, push_to_output); @@ -339,10 +342,7 @@ class memory_snapshot_harness_generatort : public goto_harness_generatort template void dfs(Value &&node, Map &&key_to_t, Handler &&handle) { - PRECONDITION(seen.empty() && inserted.empty()); dfs_inner(node, key_to_t, handle); - seen.clear(); - inserted.clear(); } template