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
forallin the following way:
if_updatedannotation like so:
adminsstate 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
forallchecks). 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.
setAdminsthat makes sure that each assigned address is not 0. You can express this like so:
assert()would inserted in this case.
#assertcan only be inserted directly before another statement, and in the instrumented code they would also be inserted before this statement.
old()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).