diff --git a/certora/applyHarnessFifo.patch b/certora/applyHarnessFifo.patch index 8222e01..4f69001 100644 --- a/certora/applyHarnessFifo.patch +++ b/certora/applyHarnessFifo.patch @@ -1,6 +1,6 @@ diff -ruN DoubleLinkedList.sol DoubleLinkedList.sol ---- DoubleLinkedList.sol 2024-07-10 12:25:51.055549876 +0200 -+++ DoubleLinkedList.sol 2024-07-11 13:17:25.523919166 +0200 +--- DoubleLinkedList.sol 2024-07-11 13:38:21.976522997 +0200 ++++ DoubleLinkedList.sol 2024-07-11 13:40:22.469518264 +0200 @@ -16,6 +16,8 @@ struct List { @@ -11,7 +11,7 @@ diff -ruN DoubleLinkedList.sol DoubleLinkedList.sol /* ERRORS */ @@ -100,6 +102,7 @@ - address next = list.accounts[address(0)].next; // If not added at the end of the list `id` will be inserted before `next`. + address next = list.accounts[address(0)].next; // `id` will be inserted before `next`. while (numberOfIterations < maxIterations && next != address(0) && list.accounts[next].value >= value) { + list.insertedAfter = next; // HARNESS diff --git a/certora/applyHarnessSimple.patch b/certora/applyHarnessSimple.patch index fa8d984..bcbedda 100644 --- a/certora/applyHarnessSimple.patch +++ b/certora/applyHarnessSimple.patch @@ -1,6 +1,6 @@ diff -ruN DoubleLinkedList.sol DoubleLinkedList.sol ---- DoubleLinkedList.sol 2024-07-10 12:25:51.055549876 +0200 -+++ DoubleLinkedList.sol 2024-07-11 13:19:00.201544572 +0200 +--- DoubleLinkedList.sol 2024-07-11 13:38:21.976522997 +0200 ++++ DoubleLinkedList.sol 2024-07-11 13:40:08.765859975 +0200 @@ -16,6 +16,8 @@ struct List { @@ -22,8 +22,7 @@ diff -ruN DoubleLinkedList.sol DoubleLinkedList.sol if (list.accounts[id].value != 0) revert AccountAlreadyInserted(); - uint256 numberOfIterations; -- address next = list.accounts[address(0)].next; // If not added at the end of the list `id` will be inserted before `next`. -+ address next = list.accounts[address(0)].next; // `id` will be inserted before `next`. + address next = list.accounts[address(0)].next; // `id` will be inserted before `next`. - while (numberOfIterations < maxIterations && next != address(0) && list.accounts[next].value >= value) { + while (next != address(0) && list.accounts[next].value >= value) { diff --git a/src/DoubleLinkedList.sol b/src/DoubleLinkedList.sol index 7a988d4..aae953b 100644 --- a/src/DoubleLinkedList.sol +++ b/src/DoubleLinkedList.sol @@ -97,7 +97,7 @@ library DoubleLinkedList { if (list.accounts[id].value != 0) revert AccountAlreadyInserted(); uint256 numberOfIterations; - address next = list.accounts[address(0)].next; // If not added at the end of the list `id` will be inserted before `next`. + address next = list.accounts[address(0)].next; // `id` will be inserted before `next`. while (numberOfIterations < maxIterations && next != address(0) && list.accounts[next].value >= value) { next = list.accounts[next].next;