915ca181ba
Co-authored-by: Shelly Grossman <shelly@certora.com> Co-authored-by: Aleksander Kryukov <58052996+RedLikeRosesss@users.noreply.github.com> Co-authored-by: Michael M <91594326+MichaelMorami@users.noreply.github.com> Co-authored-by: Aleksander Kryukov <firealexkryukov@gmail.com>
14 lines
518 B
Ruby
14 lines
518 B
Ruby
/*
|
|
This rule looks for a non-reverting execution path to each method, including those overridden in the harness.
|
|
A method has such an execution path if it violates this rule.
|
|
How it works:
|
|
- If there is a non-reverting execution path, we reach the false assertion, and the sanity fails.
|
|
- If all execution paths are reverting, we never call the assertion, and the method will pass this rule vacuously.
|
|
*/
|
|
|
|
rule sanity(method f) {
|
|
env e;
|
|
calldataarg arg;
|
|
f(e, arg);
|
|
assert false;
|
|
} |