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'. */