scribble
scribble copied to clipboard
Warn users when annotations may add inifinte loops
Instrumentation turns the following terminating code into non-terminating code:
contract Foo {
function double1(uint x) public view returns (uint) {
return double2(x);
}
/// if_succeeds $result == double1(x);
function double2(uint x) public view returns (uint) {
return x + x;
}
}
We can use the callgraph of the original code to detect when function calls in the annotations may create cycles and issue warnings for users that the annotations may introduce infinite recursion. For example this check shouldn't flag anything in the following sample:
contract Foo {
/// if_succeeds $result == double2(x);
function double1(uint x) public view returns (uint) {
return x * 2;
}
/// if_succeeds $result == double1(x);
function double2(uint x) public view returns (uint) {
return x + x;
}
}
This is not straightforward, as sometimes we can encounder conditional constructs in annotations and in functions. Therefore, in case of naive implementation some produced warnings might be misleading.