From 8677206223ba11f0e1e31928aad41ecfde6d8ba0 Mon Sep 17 00:00:00 2001 From: franck44 Date: Mon, 16 Oct 2023 11:19:19 +1100 Subject: [PATCH] Documentation. --- .../yul-bytecode-verif/overflowChecker/overflowChecker.dfy | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/dafny/yul-bytecode-verif/overflowChecker/overflowChecker.dfy b/src/dafny/yul-bytecode-verif/overflowChecker/overflowChecker.dfy index 7ce9558..9f72a61 100644 --- a/src/dafny/yul-bytecode-verif/overflowChecker/overflowChecker.dfy +++ b/src/dafny/yul-bytecode-verif/overflowChecker/overflowChecker.dfy @@ -32,7 +32,10 @@ module OverflowChecker { { // thanks Dafny } - + /** + * Overfloe checker as generated bh the Solidity compiler. + * `clean-up` calls have been removed. + */ method checked_add_t_uint256(x: u256, y: u256, s: Executing) returns (sum: u256, s': State) /** if no overflow we get normal state s'. */