diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/RemoveUnusedMemory.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/RemoveUnusedMemory.java index df52a77350..5dd865d961 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/RemoveUnusedMemory.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/RemoveUnusedMemory.java @@ -26,6 +26,14 @@ public void run(Program program) { final Memory memory = program.getMemory(); final MemoryObjectCollector collector = new MemoryObjectCollector(); program.getThreadEvents(RegReader.class).forEach(r -> r.transformExpressions(collector)); + // Also add MemoryObjects referenced by initial values (this does happen in Litmus code) + for (MemoryObject obj : memory.getObjects()) { + for (int field : obj.getStaticallyInitializedFields()) { + if (obj.getInitialValue(field) instanceof MemoryObject memObj) { + collector.memoryObjects.add(memObj); + } + } + } Sets.difference(memory.getObjects(), collector.memoryObjects).forEach(memory::deleteMemoryObject); }