solidity/test/libsolidity/smtCheckerTests/inheritance/functions_2.sol
2022-04-01 23:41:18 -05:00

27 lines
825 B
Solidity

// 2 warnings, A.f and A.g
contract A {
uint x;
function f() public virtual view {
assert(x == 1);
}
function g() public view {
assert(x == 1);
}
}
// 2 warnings, B.f and A.g
contract B is A {
uint y;
function f() public view override {
assert(x == 1);
}
}
// ====
// SMTEngine: all
// ----
// Warning 6328: (88-102='assert(x == 1)'): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nA.constructor()\nState: x = 0\nA.f()
// Warning 6328: (137-151='assert(x == 1)'): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nA.constructor()\nState: x = 0\nA.g()
// Warning 6328: (253-267='assert(x == 1)'): CHC: Assertion violation happens here.\nCounterexample:\ny = 0, x = 0\n\nTransaction trace:\nB.constructor()\nState: y = 0, x = 0\nB.f()