Add support to internal function calls

This commit is contained in:
Leonardo Alt
2020-03-11 16:29:07 +01:00
parent 1167af1dfe
commit 07368c2e1e
67 changed files with 506 additions and 189 deletions
@@ -2,40 +2,22 @@ pragma experimental SMTChecker;
contract C
{
uint x;
uint y;
uint z;
function f() public {
if (x == 1)
x = 2;
else
x = 1;
g();
if (y != 1)
g();
assert(y == 1);
}
function g() public {
function g() internal {
y = 1;
h();
assert(z == 1);
}
function h() public {
z = 1;
x = 1;
function h() internal {
f();
// This fails for the following calls to the contract:
// h()
// g() h()
// It does not fail for f() g() h() because in that case
// h() will not inline f() since it already is in the callstack.
assert(x == 1);
assert(y == 1);
}
}
// ----
// Warning: (271-274): Assertion checker does not support recursive function calls.
// Warning: (140-143): Assertion checker does not support recursive function calls.
// Warning: (483-497): Assertion violation happens here
// Warning: (201-204): Assertion checker does not support recursive function calls.
// Warning: (483-497): Assertion violation happens here