Skip to content

Commit

Permalink
refactor: remove insertedAfter initialization
Browse files Browse the repository at this point in the history
  • Loading branch information
QGarchery committed Jul 11, 2024
1 parent 76a0d1d commit dfba522
Show file tree
Hide file tree
Showing 2 changed files with 9 additions and 13 deletions.
11 changes: 4 additions & 7 deletions certora/applyHarnessFifo.patch
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
diff -ruN DoubleLinkedList.sol DoubleLinkedList.sol
--- DoubleLinkedList.sol 2024-07-10 12:25:51.055549876 +0200
+++ DoubleLinkedList.sol 2024-07-10 12:38:54.711124189 +0200
+++ DoubleLinkedList.sol 2024-07-11 13:17:25.523919166 +0200
@@ -16,6 +16,8 @@

struct List {
Expand All @@ -10,18 +10,15 @@ diff -ruN DoubleLinkedList.sol DoubleLinkedList.sol
}

/* ERRORS */
@@ -98,8 +100,10 @@

uint256 numberOfIterations;
@@ -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`.
+ list.insertedAfter = address(0); // HARNESS

while (numberOfIterations < maxIterations && next != address(0) && list.accounts[next].value >= value) {
+ list.insertedAfter = next; // HARNESS
next = list.accounts[next].next;
unchecked {
++numberOfIterations;
@@ -107,6 +111,7 @@
@@ -107,6 +110,7 @@
}

if (numberOfIterations == maxIterations) next = address(0);
Expand All @@ -31,7 +28,7 @@ diff -ruN DoubleLinkedList.sol DoubleLinkedList.sol
list.accounts[id] = Account(prev, next, value);
diff -ruN MockDLL.sol MockDLL.sol
--- MockDLL.sol 1970-01-01 01:00:00.000000000 +0100
+++ MockDLL.sol 2024-07-10 12:36:30.235182781 +0200
+++ MockDLL.sol 2024-07-11 10:58:47.037997151 +0200
@@ -0,0 +1,111 @@
+// SPDX-License-Identifier: AGPL-3.0-only
+pragma solidity ^0.8.0;
Expand Down
11 changes: 5 additions & 6 deletions certora/applyHarnessSimple.patch
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
diff -ruN DoubleLinkedList.sol DoubleLinkedList.sol
--- DoubleLinkedList.sol 2024-07-10 12:25:51.055549876 +0200
+++ DoubleLinkedList.sol 2024-07-10 12:34:45.178218509 +0200
+++ DoubleLinkedList.sol 2024-07-11 13:19:00.201544572 +0200
@@ -16,6 +16,8 @@

struct List {
Expand All @@ -10,7 +10,7 @@ diff -ruN DoubleLinkedList.sol DoubleLinkedList.sol
}

/* ERRORS */
@@ -90,23 +92,20 @@
@@ -90,23 +92,19 @@
/// @param list The list to search in.
/// @param id The address of the account.
/// @param value The value of the account.
Expand All @@ -23,26 +23,25 @@ diff -ruN DoubleLinkedList.sol DoubleLinkedList.sol

- uint256 numberOfIterations;
- address next = list.accounts[address(0)].next; // If not added at the end of the list `id` will be inserted before `next`.
+ list.insertedAfter = address(0);
+ 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) {
+ list.insertedAfter = next;
+ list.insertedAfter = next; // HARNESS
next = list.accounts[next].next;
- unchecked {
- ++numberOfIterations;
- }
}

- if (numberOfIterations == maxIterations) next = address(0);
+ list.insertedBefore = next;
+ list.insertedBefore = next; // HARNESS

address prev = list.accounts[next].prev;
list.accounts[id] = Account(prev, next, value);
diff -ruN MockDLL.sol MockDLL.sol
--- MockDLL.sol 1970-01-01 01:00:00.000000000 +0100
+++ MockDLL.sol 2024-07-10 12:26:25.130305388 +0200
+++ MockDLL.sol 2024-07-11 12:42:15.108949766 +0200
@@ -0,0 +1,91 @@
+// SPDX-License-Identifier: AGPL-3.0-only
+pragma solidity ^0.8.0;
Expand Down

0 comments on commit dfba522

Please sign in to comment.