Prover Version 8.8.0
Announcing new CVL features and improvements for CI/CD
Author:
Shane RunquistA new builtin rule, uncheckedOverflows, is available. It checks whether arithmetic operations can overflow or underflow in unchecked code. The analysis is done for each external method and each unchecked operation that is reachable from the method call.
A new builtin rule, safeCasting, has been added that checks whether any Solidity casting operator can be out of bounds (e.g., whether in uint16(x) , is it possible for x to be larger than 2^16-1). Analysis is done for each external method and each casting operation that is reachable from the method call.
The --method and --exclude_method flags now allow providing only the method name (without any parameter types) for EVM. If there are several overloads for this function name, all of them will be matched.
Jaroslav Bendík, PhD
Yoav Elmalem
Johannes Späth, PhD--assume_no_casting_overflowNewly added flag, --assume_no_casting_overflow, assumes no casting operations in Solidity are out of bounds. For example, if int16(x) is in the Solidity code, then x is assumed to be in the valid range of an int16 when this flag is used. Note that this is an underapproximation, as Solidity does not revert on such out-of-bounds values.
Access these updates by ensuring your software is up-to-date with the latest version. To upgrade to v8.8.0, simply run pip install --upgrade certora-cli.
As always, support is available on our Discord server. We welcome and appreciate your feedback.