invariant
and if_updated
) or the contract's state variables and the arguments/returns of a specific function (if_succeeds
). While this is already powerful, sometimes you really want to check a property in the middle of an existing function (e.g. inside a loop?) and wish to talk about the values of local variables in the function. For this purpose we have added the #assert
annotation.forall
in the following way:if_updated
annotation like so:
admins
state variable into a custom type that tracks the set of keys. This adds multiple arrays and maps, and also adds extra loops in the instrumentation code (implementing the actual forall
checks). This instrumentation can sometimes cause trouble for backend tools (such as fuzzers and symbolic execution engines) because of all of the extra paths its adding to the code.setAdmins
that makes sure that each assigned address is not 0. You can express this like so:assert()
would inserted in this case.#assert
:#assert
can only be inserted directly before another statement, and in the instrumented code they would also be inserted before this statement.#assert
annotation at the end of a code block! If you do, it will be silently ignored! This limitation is due to the way the solidity compiler reports docstrings on statements to us. We are working on resolving this. Until then, if you need to insert an annotation at the end of a code block, insert a dummy no-op statement. For example:
...
/// #assert false;
0; // Dummy no-op statement insertedold()
inside of an assert()
- it can only talk about the state of the program at the point of the #assert
. If you want to talk about changes in state across some statements, check out the articles on the new experimental let feature(TODO).