Browse Source

made the spec run

Michael George 3 years ago
parent
commit
aafb14461b

+ 17 - 1
certora/harnesses/ERC1155/ERC1155PausableHarness.sol

@@ -1,6 +1,22 @@
-import "../../munged/token/ERC1155/extensions/ERC1155Pausable.sol"
+import "../../munged/token/ERC1155/extensions/ERC1155Pausable.sol";
 
 contract ERC1155PausableHarness is ERC1155Pausable {
+    constructor(string memory uri_)
+        ERC1155(uri_)
+    {}
 
+    function pause() public {
+        _pause();
+    }
+
+    function unpause() public {
+        _unpause();
+    }
+
+    function onlyWhenPausedMethod() public whenPaused {
+    }
+
+    function onlyWhenNotPausedMethod() public whenNotPaused {
+    }
 }
 

+ 1 - 1
certora/scripts/verifyERC1155Pausable.sh

@@ -1,5 +1,5 @@
 certoraRun \
-    certora/harness/ERC1155/ERC1155PausableHarness.sol \
+    certora/harnesses/ERC1155/ERC1155PausableHarness.sol \
     --verify ERC1155PausableHarness:certora/specs/ERC1155Pausable.spec \
     --solc solc8.2 \
     --optimistic_loop \

+ 9 - 0
certora/specs/ERC1155Pausable.spec

@@ -0,0 +1,9 @@
+
+rule sanity {
+    method f; env e; calldataarg args;
+
+    f(e, args);
+
+    assert false;
+}
+