From fc945880d11ee85e1a06340c386efec119f6eddf Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Tue, 5 Nov 2019 17:55:05 +0100 Subject: [PATCH] [SMTChecker] Fix override tests --- libsolidity/formal/SMTEncoder.cpp | 1 + .../smtCheckerTests/inheritance/fallback.sol | 27 ++++++++++++++++++ .../inheritance/fallback_receive.sol | 28 +++++++++++++++++++ .../inheritance/functions_1.sol | 4 +-- .../inheritance/functions_2.sol | 4 +-- .../inheritance/functions_3.sol | 14 +++++----- .../smtCheckerTests/inheritance/receive.sol | 27 ++++++++++++++++++ .../inheritance/receive_fallback.sol | 28 +++++++++++++++++++ 8 files changed, 122 insertions(+), 11 deletions(-) create mode 100644 test/libsolidity/smtCheckerTests/inheritance/fallback.sol create mode 100644 test/libsolidity/smtCheckerTests/inheritance/fallback_receive.sol create mode 100644 test/libsolidity/smtCheckerTests/inheritance/receive.sol create mode 100644 test/libsolidity/smtCheckerTests/inheritance/receive_fallback.sol diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index 19240fe11..53902624b 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -52,6 +52,7 @@ bool SMTEncoder::visit(ContractDefinition const& _contract) for (auto const& function: resolvedFunctions) if ( function->name() == baseFunction->name() && + function->kind() == baseFunction->kind() && FunctionType(*function).asCallableFunction(false)-> hasEqualParameterTypes(*FunctionType(*baseFunction).asCallableFunction(false)) ) diff --git a/test/libsolidity/smtCheckerTests/inheritance/fallback.sol b/test/libsolidity/smtCheckerTests/inheritance/fallback.sol new file mode 100644 index 000000000..5e8b36e12 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/inheritance/fallback.sol @@ -0,0 +1,27 @@ +pragma experimental SMTChecker; + +// 2 warnings, fallback and A.g +contract A { + uint x; + + fallback () external { + assert(x == 1); + } + function g() public view { + assert(x == 1); + } +} + +// 2 warnings, fallback and A.g +contract B is A { + uint y; + + fallback () external override { + assert(x == 0); + } +} +// ---- +// Warning: (114-128): Assertion violation happens here +// Warning: (163-177): Assertion violation happens here +// Warning: (280-294): Assertion violation happens here +// Warning: (163-177): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/inheritance/fallback_receive.sol b/test/libsolidity/smtCheckerTests/inheritance/fallback_receive.sol new file mode 100644 index 000000000..5b66c1cb1 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/inheritance/fallback_receive.sol @@ -0,0 +1,28 @@ +pragma experimental SMTChecker; + +// 2 warnings, fallback and A.g +contract A { + uint x; + + fallback () external { + assert(x == 1); + } + function g() public view { + assert(x == 1); + } +} + +// 3 warnings, receive, A.fallback and A.g +contract B is A { + uint y; + + receive () external payable { + assert(x == 0); + } +} +// ---- +// Warning: (114-128): Assertion violation happens here +// Warning: (163-177): Assertion violation happens here +// Warning: (289-303): Assertion violation happens here +// Warning: (114-128): Assertion violation happens here +// Warning: (163-177): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/inheritance/functions_1.sol b/test/libsolidity/smtCheckerTests/inheritance/functions_1.sol index d43e90955..3ee46782d 100644 --- a/test/libsolidity/smtCheckerTests/inheritance/functions_1.sol +++ b/test/libsolidity/smtCheckerTests/inheritance/functions_1.sol @@ -14,12 +14,12 @@ contract A { // 2 warnings, B.f and A.g contract B is A { - function f() public view { + function f() public view override { assert(x == 0); } } // ---- // Warning: (113-127): Assertion violation happens here // Warning: (162-176): Assertion violation happens here -// Warning: (259-273): Assertion violation happens here +// Warning: (268-282): Assertion violation happens here // Warning: (162-176): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/inheritance/functions_2.sol b/test/libsolidity/smtCheckerTests/inheritance/functions_2.sol index c23eb0037..0ff8337fa 100644 --- a/test/libsolidity/smtCheckerTests/inheritance/functions_2.sol +++ b/test/libsolidity/smtCheckerTests/inheritance/functions_2.sol @@ -16,12 +16,12 @@ contract A { contract B is A { uint y; - function f() public view { + function f() public view override { assert(x == 0); } } // ---- // Warning: (113-127): Assertion violation happens here // Warning: (162-176): Assertion violation happens here -// Warning: (269-283): Assertion violation happens here +// Warning: (278-292): Assertion violation happens here // Warning: (162-176): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/inheritance/functions_3.sol b/test/libsolidity/smtCheckerTests/inheritance/functions_3.sol index d8fbdabfc..febaa83b4 100644 --- a/test/libsolidity/smtCheckerTests/inheritance/functions_3.sol +++ b/test/libsolidity/smtCheckerTests/inheritance/functions_3.sol @@ -16,7 +16,7 @@ contract A { contract B is A { uint y; - function f() public view { + function f() public view override { assert(x == 0); } function h() public view { @@ -28,7 +28,7 @@ contract B is A { contract C is B { uint z; - function f() public view { + function f() public view override { assert(x == 0); } function i() public view { @@ -38,10 +38,10 @@ contract C is B { // ---- // Warning: (113-127): Assertion violation happens here // Warning: (162-176): Assertion violation happens here -// Warning: (271-285): Assertion violation happens here -// Warning: (320-334): Assertion violation happens here +// Warning: (280-294): Assertion violation happens here +// Warning: (329-343): Assertion violation happens here // Warning: (162-176): Assertion violation happens here -// Warning: (434-448): Assertion violation happens here -// Warning: (483-497): Assertion violation happens here -// Warning: (320-334): Assertion violation happens here +// Warning: (452-466): Assertion violation happens here +// Warning: (501-515): Assertion violation happens here +// Warning: (329-343): Assertion violation happens here // Warning: (162-176): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/inheritance/receive.sol b/test/libsolidity/smtCheckerTests/inheritance/receive.sol new file mode 100644 index 000000000..f9d92ab52 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/inheritance/receive.sol @@ -0,0 +1,27 @@ +pragma experimental SMTChecker; + +// 2 warnings, receive and A.g +contract A { + uint x; + + receive () external payable { + assert(x == 1); + } + function g() public view { + assert(x == 1); + } +} + +// 2 warnings, receive and A.g +contract B is A { + uint y; + + receive () external payable override { + assert(x == 0); + } +} +// ---- +// Warning: (120-134): Assertion violation happens here +// Warning: (169-183): Assertion violation happens here +// Warning: (292-306): Assertion violation happens here +// Warning: (169-183): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/inheritance/receive_fallback.sol b/test/libsolidity/smtCheckerTests/inheritance/receive_fallback.sol new file mode 100644 index 000000000..ff6c19e77 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/inheritance/receive_fallback.sol @@ -0,0 +1,28 @@ +pragma experimental SMTChecker; + +// 2 warnings, receive and A.g +contract A { + uint x; + + receive () external payable { + assert(x == 1); + } + function g() public view { + assert(x == 1); + } +} + +// 3 warnings, fallback, A.receive and A.g +contract B is A { + uint y; + + fallback () external { + assert(x == 0); + } +} +// ---- +// Warning: (120-134): Assertion violation happens here +// Warning: (169-183): Assertion violation happens here +// Warning: (288-302): Assertion violation happens here +// Warning: (120-134): Assertion violation happens here +// Warning: (169-183): Assertion violation happens here