From 1b1b6651cd60fcaded8043dc00e61df075fe2e4a Mon Sep 17 00:00:00 2001 From: chriseth Date: Fri, 15 Jan 2016 16:26:12 +0100 Subject: Fix sequence number bug. This bug resulted in incorrect storage access in some situations. The reason was that when intersecting states, the sequence numbers were not handled and thus some operations with too low sequence numbers were used during code generation. --- KnownState.h | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) (limited to 'KnownState.h') diff --git a/KnownState.h b/KnownState.h index 6dff74a5..c1c602dc 100644 --- a/KnownState.h +++ b/KnownState.h @@ -100,13 +100,12 @@ public: void reset() { resetStorage(); resetMemory(); resetStack(); } unsigned sequenceNumber() const { return m_sequenceNumber; } - /// Manually increments the storage and memory sequence number. - void incrementSequenceNumber() { m_sequenceNumber += 2; } /// Replaces the state by the intersection with _other, i.e. only equal knowledge is retained. /// If the stack heighht is different, the smaller one is used and the stack is compared /// relatively. - void reduceToCommonKnowledge(KnownState const& _other); + /// @param _combineSequenceNumbers if true, sets the sequence number to the maximum of both + void reduceToCommonKnowledge(KnownState const& _other, bool _combineSequenceNumbers); /// @returns a shared pointer to a copy of this state. std::shared_ptr copy() const { return std::make_shared(*this); } -- cgit