Fix SMTChecker tests in 060

This commit is contained in:
Leonardo Alt 2019-12-03 21:44:06 +01:00
parent f2790cc5e0
commit d6e8ca4c54
14 changed files with 43 additions and 43 deletions

View File

@ -6,7 +6,7 @@ contract C {
}
}
contract B is C {
abstract contract B is C {
constructor(uint x) public {
a = x;
}
@ -19,4 +19,4 @@ contract A is B {
}
}
// ----
// Warning: (244-262): Assertion violation happens here
// Warning: (253-271): Assertion violation happens here

View File

@ -6,7 +6,7 @@ contract C {
}
}
contract B is C {
abstract contract B is C {
constructor(uint x) public {
a = x;
}
@ -18,6 +18,6 @@ contract A is B {
}
}
// ----
// Warning: (221-226): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning: (212-217): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning: (203-208): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning: (242-247): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning: (251-256): Overflow (resulting value larger than 2**256 - 1) happens here

View File

@ -6,7 +6,7 @@ contract C {
}
}
contract B1 is C {
abstract contract B1 is C {
constructor(uint x) public {
a = x;
}
@ -25,5 +25,5 @@ contract A is B2, B1 {
}
}
// ----
// Warning: (205-210): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning: (321-339): Assertion violation happens here
// Warning: (214-219): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning: (330-348): Assertion violation happens here

View File

@ -6,7 +6,7 @@ contract C {
}
}
contract B1 is C {
abstract contract B1 is C {
constructor(uint x) public {
a = x;
}
@ -25,5 +25,5 @@ contract A is B2, B1 {
}
}
// ----
// Warning: (205-210): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning: (321-339): Assertion violation happens here
// Warning: (214-219): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning: (330-348): Assertion violation happens here

View File

@ -6,7 +6,7 @@ contract C {
}
}
contract B1 is C {
abstract contract B1 is C {
uint b1;
constructor(uint x) public {
b1 = x + a;
@ -27,8 +27,8 @@ contract A is B2, B1 {
}
}
// ----
// Warning: (165-170): Underflow (resulting value less than 0) happens here
// Warning: (165-170): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning: (230-235): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning: (253-258): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning: (353-369): Assertion violation happens here
// Warning: (174-179): Underflow (resulting value less than 0) happens here
// Warning: (174-179): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning: (239-244): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning: (262-267): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning: (362-378): Assertion violation happens here

View File

@ -6,13 +6,13 @@ contract F {
}
}
contract E is F {}
contract D is E {
abstract contract E is F {}
abstract contract D is E {
constructor() public {
a = 3;
}
}
contract C is D {}
abstract contract C is D {}
contract B is C {
constructor(uint x) F(x + 1) public {
}
@ -25,5 +25,5 @@ contract A is B {
}
}
// ----
// Warning: (234-239): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning: (329-343): Assertion violation happens here
// Warning: (261-266): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning: (356-370): Assertion violation happens here

View File

@ -6,13 +6,13 @@ contract F {
}
}
contract E is F {}
contract D is E {
abstract contract E is F {}
abstract contract D is E {
constructor() public {
a = 3;
}
}
contract C is D {}
abstract contract C is D {}
contract B is C {
constructor() F(1) public {
assert(a == 3);
@ -23,5 +23,5 @@ contract B is C {
contract A is B {
}
// ----
// Warning: (260-274): Assertion violation happens here
// Warning: (260-274): Assertion violation happens here
// Warning: (287-301): Assertion violation happens here
// Warning: (287-301): Assertion violation happens here

View File

@ -6,13 +6,13 @@ contract F {
}
}
contract E is F {}
contract D is E {
abstract contract E is F {}
abstract contract D is E {
constructor() public {
a = 3;
}
}
contract C is D {}
abstract contract C is D {}
contract B is C {
constructor(uint x) F(x + 1) public {
}
@ -25,5 +25,5 @@ contract A is B {
}
}
// ----
// Warning: (234-239): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning: (329-343): Assertion violation happens here
// Warning: (261-266): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning: (356-370): Assertion violation happens here

View File

@ -6,7 +6,7 @@ contract C {
}
}
contract B is C {
abstract contract B is C {
uint b;
constructor(uint x) public {
b = a + x;
@ -22,6 +22,6 @@ contract A is B {
}
// ----
// Warning: (162-167): Underflow (resulting value less than 0) happens here
// Warning: (162-167): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning: (287-305): Assertion violation happens here
// Warning: (171-176): Underflow (resulting value less than 0) happens here
// Warning: (171-176): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning: (296-314): Assertion violation happens here

View File

@ -6,7 +6,7 @@ contract C {
}
}
contract B is C {
abstract contract B is C {
uint b;
constructor(uint x) public {
b = x + 10;
@ -22,5 +22,5 @@ contract A is B {
}
// ----
// Warning: (162-168): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning: (285-303): Assertion violation happens here
// Warning: (171-177): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning: (294-312): Assertion violation happens here

View File

@ -17,7 +17,7 @@ contract B is A {
uint y;
fallback () external override {
assert(x == 0);
assert(x == 1);
}
}
// ----

View File

@ -17,7 +17,7 @@ contract B is A {
uint y;
receive () external payable {
assert(x == 0);
assert(x == 1);
}
}
// ----

View File

@ -17,7 +17,7 @@ contract B is A {
uint y;
receive () external payable override {
assert(x == 0);
assert(x == 1);
}
}
// ----

View File

@ -17,7 +17,7 @@ contract B is A {
uint y;
fallback () external {
assert(x == 0);
assert(x == 1);
}
}
// ----