#requireannotation can be inserted before a function or before any statement inside of a function. When inserted before a function, it can talk about the arguments/returns of the function and is instrumented as a
require()statement at the beginning of the function.
require()inserted before the target statement.
IInterestRateModeland can be upgraded by calling
Pool.upgradeInterestRateModel. In our experience our fuzzer can often trigger the upgrade path with a random address, thus breaking the contract (the fuzzer is allowed to try things as the owner as well). Once this invalid upgrade is performed, and the contract is in an invalid state a lot of followup false positives are triggered. We'd like to limit the fuzzer from triggering an invalid upgrade. We can do so with the following
require(), if the fuzzer tries to use an invalid address here, the transaction reverting will not be treated as a property violation.
#trycan be inserted before a function or before a given statement. It allows the user to write a boolean expression over the inputs, that aims to help the backend tool. For example consider the following contrived
MultiTokenPoolcontract, that holds funds on behalf of a user for multiple different tokens. The pool provides a function for withdrawing funds from just one token -
withdrawSingleToken, without realizing that a valid token address is needed, then its unlikely that it will be able to cover this function. In such cases a user can suggest specific inputs for the tool to try with the following
ifs are designed to have no actual effect on the exectuion of the program, but still to not be optimized away by the compiler. The idea behind them is that if the underlying tool is trying to maximize coverage by exploring more paths, then it will attempt to reach the bodies of the
ifstatemets. Reaching those bodies requires solving the relatively easy constraints
token == <Token1 addr>and
token == <Token2 addr>. Solving these constraints allows the tool to try exactly the inputs that we wanted it to try. Note that unlike the
#trydoes not limit the backend tool to only use the inputs we suggested - the annotation allows any other possible input as well.