Merge remote-tracking branch 'origin/develop' into HEAD

This commit is contained in:
chriseth
2020-03-11 18:44:06 +01:00
198 changed files with 2907 additions and 761 deletions
+6 -2
View File
@@ -53,12 +53,16 @@ ExecutionFramework::ExecutionFramework(langutil::EVMVersion _evmVersion):
m_optimiserSettings = solidity::frontend::OptimiserSettings::full();
else if (solidity::test::CommonOptions::get().optimize)
m_optimiserSettings = solidity::frontend::OptimiserSettings::standard();
m_evmHost->reset();
reset();
}
void ExecutionFramework::reset()
{
m_evmHost->reset();
for (size_t i = 0; i < 10; i++)
m_evmHost->accounts[EVMHost::convertToEVMC(account(i))].balance =
EVMHost::convertToEVMC(u256(1) << 100);
}
std::pair<bool, string> ExecutionFramework::compareAndCreateMessage(
+2
View File
@@ -251,6 +251,8 @@ private:
}
protected:
void reset();
void sendMessage(bytes const& _data, bool _isCreation, u256 const& _value = 0);
void sendEther(Address const& _to, u256 const& _value);
size_t currentTimestamp();
+22 -13
View File
@@ -15,6 +15,7 @@
along with solidity. If not, see <http://www.gnu.org/licenses/>.
*/
#include <test/Common.h>
#include <test/TestCase.h>
#include <libsolutil/StringUtils.h>
@@ -52,14 +53,18 @@ bool TestCase::isTestFilename(boost::filesystem::path const& _filename)
!boost::starts_with(_filename.string(), ".");
}
bool TestCase::validateSettings(langutil::EVMVersion)
void TestCase::validateSettings()
{
if (!m_settings.empty())
throw runtime_error(
"Unknown setting(s): " +
util::joinHumanReadable(m_settings | boost::adaptors::map_keys)
);
return true;
}
bool TestCase::shouldRun()
{
return m_shouldRun;
}
pair<map<string, string>, size_t> TestCase::parseSourcesAndSettingsWithLineNumbers(istream& _stream)
@@ -157,20 +162,19 @@ void TestCase::expect(string::iterator& _it, string::iterator _end, string::valu
++_it;
}
bool EVMVersionRestrictedTestCase::validateSettings(langutil::EVMVersion _evmVersion)
void EVMVersionRestrictedTestCase::validateSettings()
{
if (!m_settings.count("EVMVersion"))
return true;
return;
string versionString = m_settings["EVMVersion"];
m_validatedSettings["EVMVersion"] = versionString;
m_settings.erase("EVMVersion");
if (!TestCase::validateSettings(_evmVersion))
return false;
TestCase::validateSettings();
if (versionString.empty())
return true;
return;
string comparator;
size_t versionBegin = 0;
@@ -188,18 +192,23 @@ bool EVMVersionRestrictedTestCase::validateSettings(langutil::EVMVersion _evmVer
if (!version)
BOOST_THROW_EXCEPTION(runtime_error{"Invalid EVM version: \"" + versionString + "\""});
langutil::EVMVersion evmVersion = solidity::test::CommonOptions::get().evmVersion();
bool comparisonResult;
if (comparator == ">")
return _evmVersion > version;
comparisonResult = evmVersion > version;
else if (comparator == ">=")
return _evmVersion >= version;
comparisonResult = evmVersion >= version;
else if (comparator == "<")
return _evmVersion < version;
comparisonResult = evmVersion < version;
else if (comparator == "<=")
return _evmVersion <= version;
comparisonResult = evmVersion <= version;
else if (comparator == "=")
return _evmVersion == version;
comparisonResult = evmVersion == version;
else if (comparator == "!")
return !(_evmVersion == version);
comparisonResult = !(evmVersion == version);
else
BOOST_THROW_EXCEPTION(runtime_error{"Invalid EVM comparator: \"" + comparator + "\""});
if (!comparisonResult)
m_shouldRun = false;
}
+6 -3
View File
@@ -70,10 +70,12 @@ public:
/// Validates the settings, i.e. moves them from m_settings to m_validatedSettings.
/// Throws a runtime exception if any setting is left at this class (i.e. unknown setting).
virtual void validateSettings();
/// Returns true, if the test case is supported in the current environment and false
/// otherwise which causes this test to be skipped.
/// This might check e.g. for restrictions on the EVM version.
virtual bool validateSettings(langutil::EVMVersion /*_evmVersion*/);
bool shouldRun();
protected:
std::pair<std::map<std::string, std::string>, std::size_t> parseSourcesAndSettingsWithLineNumbers(std::istream& _file);
@@ -102,13 +104,14 @@ protected:
std::map<std::string, std::string> m_settings;
/// Updated settings after validation.
std::map<std::string, std::string> m_validatedSettings;
bool m_shouldRun = true;
};
class EVMVersionRestrictedTestCase: public TestCase
{
public:
/// Returns true, if the test case is supported for EVM version @arg _evmVersion, false otherwise.
bool validateSettings(langutil::EVMVersion _evmVersion) override;
void validateSettings() override;
};
}
+2 -1
View File
@@ -94,7 +94,8 @@ int registerTests(
{
stringstream errorStream;
auto testCase = _testCaseCreator(config);
if (testCase->validateSettings(solidity::test::CommonOptions::get().evmVersion()))
testCase->validateSettings();
if (testCase->shouldRun())
switch (testCase->run(errorStream))
{
case TestCase::TestResult::Success:
+10 -1
View File
@@ -77,6 +77,11 @@ function compileFull()
expect_output=1
shift;
fi
if [[ $1 = '-o' ]]
then
expect_output=2
shift;
fi
local files="$*"
local output
@@ -93,7 +98,7 @@ function compileFull()
if [[ \
"$exit_code" -ne "$expected_exit_code" || \
( $expect_output -eq 0 && -n "$errors" ) || \
( $expect_output -ne 0 && -z "$errors" ) \
( $expect_output -eq 1 && -z "$errors" ) \
]]
then
printError "Unexpected compilation result:"
@@ -350,6 +355,10 @@ SOLTMPDIR=$(mktemp -d)
then
opts="$opts -w"
fi
if grep "This may report a warning" "$f" >/dev/null
then
opts="$opts -o"
fi
compileFull $opts "$SOLTMPDIR/$f"
done
)
@@ -0,0 +1,95 @@
{
"absolutePath": "a",
"exportedSymbols":
{
"C":
[
6
]
},
"id": 7,
"nodeType": "SourceUnit",
"nodes":
[
{
"abstract": false,
"baseContracts": [],
"contractDependencies": [],
"contractKind": "contract",
"documentation": null,
"fullyImplemented": true,
"id": 6,
"linearizedBaseContracts":
[
6
],
"name": "C",
"nodeType": "ContractDefinition",
"nodes":
[
{
"body":
{
"id": 4,
"nodeType": "Block",
"src": "42:31:1",
"statements":
[
{
"AST":
{
"nodeType": "YulBlock",
"src": "61:6:1",
"statements":
[
{
"nodeType": "YulBlock",
"src": "63:2:1",
"statements": []
}
]
},
"evmVersion": %EVMVERSION%,
"externalReferences": [],
"id": 3,
"nodeType": "InlineAssembly",
"src": "52:15:1"
}
]
},
"documentation": null,
"functionSelector": "e2179b8e",
"id": 5,
"implemented": true,
"kind": "function",
"modifiers": [],
"name": "g",
"nodeType": "FunctionDefinition",
"overrides": null,
"parameters":
{
"id": 1,
"nodeType": "ParameterList",
"parameters": [],
"src": "27:2:1"
},
"returnParameters":
{
"id": 2,
"nodeType": "ParameterList",
"parameters": [],
"src": "42:0:1"
},
"scope": 6,
"src": "17:56:1",
"stateMutability": "view",
"virtual": false,
"visibility": "public"
}
],
"scope": 7,
"src": "0:75:1"
}
],
"src": "0:76:1"
}
@@ -0,0 +1,7 @@
contract C {
function g() view public {
assembly { {} }
}
}
// ----
@@ -0,0 +1,123 @@
{
"attributes":
{
"absolutePath": "a",
"exportedSymbols":
{
"C":
[
6
]
}
},
"children":
[
{
"attributes":
{
"abstract": false,
"baseContracts":
[
null
],
"contractDependencies":
[
null
],
"contractKind": "contract",
"documentation": null,
"fullyImplemented": true,
"linearizedBaseContracts":
[
6
],
"name": "C",
"scope": 7
},
"children":
[
{
"attributes":
{
"documentation": null,
"functionSelector": "e2179b8e",
"implemented": true,
"isConstructor": false,
"kind": "function",
"modifiers":
[
null
],
"name": "g",
"overrides": null,
"scope": 6,
"stateMutability": "view",
"virtual": false,
"visibility": "public"
},
"children":
[
{
"attributes":
{
"parameters":
[
null
]
},
"children": [],
"id": 1,
"name": "ParameterList",
"src": "27:2:1"
},
{
"attributes":
{
"parameters":
[
null
]
},
"children": [],
"id": 2,
"name": "ParameterList",
"src": "42:0:1"
},
{
"children":
[
{
"attributes":
{
"evmVersion": %EVMVERSION%,
"externalReferences":
[
null
],
"operations": "{ { } }"
},
"children": [],
"id": 3,
"name": "InlineAssembly",
"src": "52:15:1"
}
],
"id": 4,
"name": "Block",
"src": "42:31:1"
}
],
"id": 5,
"name": "FunctionDefinition",
"src": "17:56:1"
}
],
"id": 6,
"name": "ContractDefinition",
"src": "0:75:1"
}
],
"id": 7,
"name": "SourceUnit",
"src": "0:76:1"
}
@@ -0,0 +1,116 @@
{
"absolutePath": "a",
"exportedSymbols":
{
"C":
[
6
]
},
"id": 7,
"nodeType": "SourceUnit",
"nodes":
[
{
"abstract": false,
"baseContracts": [],
"contractDependencies": [],
"contractKind": "contract",
"documentation": null,
"fullyImplemented": true,
"id": 6,
"linearizedBaseContracts":
[
6
],
"name": "C",
"nodeType": "ContractDefinition",
"nodes":
[
{
"body":
{
"id": 4,
"nodeType": "Block",
"src": "42:48:1",
"statements":
[
{
"AST":
{
"nodeType": "YulBlock",
"src": "61:23:1",
"statements":
[
{
"cases":
[
{
"body":
{
"nodeType": "YulBlock",
"src": "80:2:1",
"statements": []
},
"nodeType": "YulCase",
"src": "72:10:1",
"value": "default"
}
],
"expression":
{
"kind": "number",
"nodeType": "YulLiteral",
"src": "70:1:1",
"type": "",
"value": "0"
},
"nodeType": "YulSwitch",
"src": "63:19:1"
}
]
},
"evmVersion": %EVMVERSION%,
"externalReferences": [],
"id": 3,
"nodeType": "InlineAssembly",
"src": "52:32:1"
}
]
},
"documentation": null,
"functionSelector": "e2179b8e",
"id": 5,
"implemented": true,
"kind": "function",
"modifiers": [],
"name": "g",
"nodeType": "FunctionDefinition",
"overrides": null,
"parameters":
{
"id": 1,
"nodeType": "ParameterList",
"parameters": [],
"src": "27:2:1"
},
"returnParameters":
{
"id": 2,
"nodeType": "ParameterList",
"parameters": [],
"src": "42:0:1"
},
"scope": 6,
"src": "17:73:1",
"stateMutability": "view",
"virtual": false,
"visibility": "public"
}
],
"scope": 7,
"src": "0:92:1"
}
],
"src": "0:93:1"
}
@@ -0,0 +1,7 @@
contract C {
function g() view public {
assembly { switch 0 default {} }
}
}
// ----
@@ -0,0 +1,123 @@
{
"attributes":
{
"absolutePath": "a",
"exportedSymbols":
{
"C":
[
6
]
}
},
"children":
[
{
"attributes":
{
"abstract": false,
"baseContracts":
[
null
],
"contractDependencies":
[
null
],
"contractKind": "contract",
"documentation": null,
"fullyImplemented": true,
"linearizedBaseContracts":
[
6
],
"name": "C",
"scope": 7
},
"children":
[
{
"attributes":
{
"documentation": null,
"functionSelector": "e2179b8e",
"implemented": true,
"isConstructor": false,
"kind": "function",
"modifiers":
[
null
],
"name": "g",
"overrides": null,
"scope": 6,
"stateMutability": "view",
"virtual": false,
"visibility": "public"
},
"children":
[
{
"attributes":
{
"parameters":
[
null
]
},
"children": [],
"id": 1,
"name": "ParameterList",
"src": "27:2:1"
},
{
"attributes":
{
"parameters":
[
null
]
},
"children": [],
"id": 2,
"name": "ParameterList",
"src": "42:0:1"
},
{
"children":
[
{
"attributes":
{
"evmVersion": %EVMVERSION%,
"externalReferences":
[
null
],
"operations": "{\n switch 0\n default { }\n}"
},
"children": [],
"id": 3,
"name": "InlineAssembly",
"src": "52:32:1"
}
],
"id": 4,
"name": "Block",
"src": "42:48:1"
}
],
"id": 5,
"name": "FunctionDefinition",
"src": "17:73:1"
}
],
"id": 6,
"name": "ContractDefinition",
"src": "0:92:1"
}
],
"id": 7,
"name": "SourceUnit",
"src": "0:93:1"
}
+7
View File
@@ -17,14 +17,18 @@
#include <test/libsolidity/SMTCheckerJSONTest.h>
#include <test/Common.h>
#include <libsolidity/formal/ModelChecker.h>
#include <libsolidity/interface/StandardCompiler.h>
#include <libsolutil/CommonIO.h>
#include <libsolutil/JSON.h>
#include <boost/algorithm/string.hpp>
#include <boost/algorithm/string/join.hpp>
#include <boost/algorithm/string/predicate.hpp>
#include <boost/test/unit_test.hpp>
#include <boost/throw_exception.hpp>
#include <fstream>
#include <memory>
#include <stdexcept>
@@ -50,6 +54,9 @@ SMTCheckerJSONTest::SMTCheckerJSONTest(string const& _filename, langutil::EVMVer
!m_smtResponses.isObject()
)
BOOST_THROW_EXCEPTION(runtime_error("Invalid JSON file."));
if (ModelChecker::availableSolvers().none())
m_shouldRun = false;
}
TestCase::TestResult SMTCheckerJSONTest::run(ostream& _stream, string const& _linePrefix, bool _formatted)
+9 -14
View File
@@ -44,6 +44,15 @@ SMTCheckerTest::SMTCheckerTest(string const& _filename, langutil::EVMVersion _ev
}
else
m_enabledSolvers = smt::SMTSolverChoice::All();
auto available = ModelChecker::availableSolvers();
if (!available.z3)
m_enabledSolvers.z3 = false;
if (!available.cvc4)
m_enabledSolvers.cvc4 = false;
if (m_enabledSolvers.none())
m_shouldRun = false;
}
TestCase::TestResult SMTCheckerTest::run(ostream& _stream, string const& _linePrefix, bool _formatted)
@@ -55,17 +64,3 @@ TestCase::TestResult SMTCheckerTest::run(ostream& _stream, string const& _linePr
return printExpectationAndError(_stream, _linePrefix, _formatted) ? TestResult::Success : TestResult::Failure;
}
bool SMTCheckerTest::validateSettings(langutil::EVMVersion _evmVersion)
{
auto available = ModelChecker::availableSolvers();
if (!available.z3)
m_enabledSolvers.z3 = false;
if (!available.cvc4)
m_enabledSolvers.cvc4 = false;
if (m_enabledSolvers.none())
return false;
return SyntaxTest::validateSettings(_evmVersion);
}
-2
View File
@@ -37,8 +37,6 @@ public:
TestResult run(std::ostream& _stream, std::string const& _linePrefix = "", bool _formatted = false) override;
bool validateSettings(langutil::EVMVersion _evmVersion) override;
protected:
/// This is set via option SMTSolvers in the test.
/// The possible options are `all`, `z3`, `cvc4`, `none`,
+4 -7
View File
@@ -71,6 +71,9 @@ SemanticTest::SemanticTest(string const& _filename, langutil::EVMVersion _evmVer
m_settings.erase("ABIEncoderV1Only");
}
if (m_runWithABIEncoderV1Only && solidity::test::CommonOptions::get().useABIEncoderV2)
m_shouldRun = false;
if (m_settings.count("revertStrings"))
{
auto revertStrings = revertStringsFromString(m_settings["revertStrings"]);
@@ -90,17 +93,11 @@ SemanticTest::SemanticTest(string const& _filename, langutil::EVMVersion _evmVer
soltestAssert(!m_tests.empty(), "No tests specified in " + _filename);
}
bool SemanticTest::validateSettings(langutil::EVMVersion _evmVersion)
{
if (m_runWithABIEncoderV1Only && solidity::test::CommonOptions::get().useABIEncoderV2)
return false;
return EVMVersionRestrictedTestCase::validateSettings(_evmVersion);
}
TestCase::TestResult SemanticTest::run(ostream& _stream, string const& _linePrefix, bool _formatted)
{
for(bool compileViaYul: set<bool>{!m_runWithoutYul, m_runWithYul})
{
reset();
bool success = true;
m_compileViaYul = compileViaYul;
-2
View File
@@ -44,8 +44,6 @@ public:
explicit SemanticTest(std::string const& _filename, langutil::EVMVersion _evmVersion);
bool validateSettings(langutil::EVMVersion _evmVersion) override;
TestResult run(std::ostream& _stream, std::string const& _linePrefix = "", bool _formatted = false) override;
void printSource(std::ostream &_stream, std::string const& _linePrefix = "", bool _formatted = false) const override;
void printUpdatedExpectations(std::ostream& _stream, std::string const& _linePrefix = "") const override;
-1
View File
@@ -540,7 +540,6 @@ BOOST_AUTO_TEST_CASE(keyword_is_reserved)
"default",
"define",
"final",
"immutable",
"implements",
"in",
"inline",
@@ -0,0 +1,9 @@
contract C {
function f(string memory s) public pure returns (bytes memory t) {
t = bytes(s);
}
}
// ====
// compileViaYul: also
// ----
// f(string): 32, 5, "Hello" -> 32, 5, "Hello"
@@ -0,0 +1,14 @@
abstract contract I
{
function a() internal view virtual returns(uint256);
}
abstract contract V is I
{
function b() public view returns(uint256) { return a(); }
}
contract C is V
{
function a() internal view override returns (uint256) { return 42;}
}
// ----
// b() -> 42
@@ -0,0 +1,9 @@
pragma experimental ABIEncoderV2;
contract C {
function f(uint256[][] calldata x) external { x[0]; }
}
// ====
// EVMVersion: >=byzantium
// revertStrings: debug
// ----
// f(uint256[][]): 0x20, 1, 0x20, 2, 0x42 -> FAILURE, hex"08c379a0", 0x20, 23, "Calldata tail too short"
@@ -4,7 +4,7 @@ contract C {
}
function f(bool x) public returns (uint) {
// Set the gas to make this work on pre-byzantium VMs
try this.g.gas(8000)(x) {
try this.g{gas: 8000}(x) {
return 1;
} catch {
return 2;
@@ -4,7 +4,7 @@ contract C {
}
function f(bool x) public returns (uint) {
// Set the gas to make this work on pre-byzantium VMs
try this.g.gas(8000)(x) {
try this.g{gas: 8000}(x) {
return 1;
} catch {
return 2;
@@ -0,0 +1,23 @@
contract C {
function f(uint x) public pure returns (uint) {
return 2 * x;
}
function g() public view returns (function (uint) external returns (uint)) {
return this.f;
}
function h(uint x) public returns (uint) {
return this.g()(x) + 1;
}
function t() external view returns (
function(uint) external returns (uint) a,
function(uint) external view returns (uint) b) {
a = this.f;
b = this.f;
}
}
// ====
// compileViaYul: also
// ----
// f(uint256): 2 -> 4
// h(uint256): 2 -> 5
// t() -> 0xFDD67305928FCAC8D213D1E47BFA6165CD0B87BB3DE648B0000000000000000, 0xFDD67305928FCAC8D213D1E47BFA6165CD0B87BB3DE648B0000000000000000
@@ -0,0 +1,17 @@
contract C {
function f() external returns (address) {
return this.f.address;
}
function g() external returns (bool) {
return this.f.address == address(this);
}
function h(function() external a) public returns (address) {
return a.address;
}
}
// ====
// compileViaYul: also
// ----
// f() -> 0x0fdd67305928fcac8d213d1e47bfa6165cd0b87b
// g() -> true
// h(function): left(0x1122334400112233445566778899AABBCCDDEEFF42424242) -> 0x1122334400112233445566778899AABBCCDDEEFF
@@ -0,0 +1,13 @@
contract C {
function f() external returns (bytes4) {
return this.f.selector;
}
function h(function() external a) public returns (bytes4) {
return a.selector;
}
}
// ====
// compileViaYul: also
// ----
// f() -> left(0x26121ff0)
// h(function): left(0x1122334400112233445566778899AABBCCDDEEFF42424242) -> left(0x42424242)
@@ -6,23 +6,17 @@ contract c {
x = x + 1;
return x;
}
function g(bool a) public returns (bool) {
function g() public returns (bool) {
bool b;
if (a) {
x = 0;
b = (f() == 0) && (f() == 0);
assert(x == 1);
assert(!b);
} else {
x = 100;
b = (f() > 0) && (f() > 0);
b = f() > 0;
assert(x == 102);
// Should fail.
assert(!b);
}
return b;
}
}
// ----
// Warning: (101-106): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning: (362-372): Assertion violation happens here
// Warning: (202-218): Assertion violation happens here
// Warning: (242-252): Assertion violation happens here
@@ -19,4 +19,6 @@ contract A is B {
}
}
// ----
// Warning: (217-222): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning: (265-270): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning: (253-271): Assertion violation happens here
@@ -26,4 +26,6 @@ contract A is B2, B1 {
}
// ----
// Warning: (214-219): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning: (214-219): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning: (342-347): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning: (330-348): Assertion violation happens here
@@ -26,4 +26,6 @@ contract A is B2, B1 {
}
// ----
// Warning: (214-219): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning: (214-219): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning: (342-347): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning: (330-348): Assertion violation happens here
@@ -31,4 +31,7 @@ contract A is B2, B1 {
// 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: (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: (174-179): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning: (362-378): Assertion violation happens here
@@ -26,4 +26,5 @@ contract A is B {
}
// ----
// Warning: (261-266): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning: (261-266): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning: (356-370): Assertion violation happens here
@@ -14,3 +14,4 @@ contract A is C {
}
// ----
// Warning: (148-162): Assertion violation happens here
// Warning: (166-182): Assertion violation happens here
@@ -9,5 +9,3 @@ contract C {
}
}
// ----
// Warning: (99-107): Assertion checker does not support recursive function calls.
// Warning: (141-144): Assertion checker does not support recursive function calls.
@@ -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
@@ -14,4 +14,3 @@ contract C
}
// ----
// Warning: (111-114): Assertion checker does not support recursive function calls.
@@ -22,5 +22,4 @@ contract C
}
}
// ----
// Warning: (206-209): Assertion checker does not support recursive function calls.
// Warning: (111-114): Assertion checker does not support recursive function calls.
// Warning: (130-144): Error trying to invoke SMT solver.
@@ -0,0 +1,25 @@
pragma experimental SMTChecker;
contract C{
uint x;
constructor(uint y) public {
assert(x == 0);
x = 1;
}
function f() public {
assert(x == 1);
++x;
g();
assert(x == 1);
}
function g() internal {
assert(x == 2);
--x;
assert(x == 1);
}
}
// ----
// Warning: (70-76): Unused function parameter. Remove or comment out the variable name to silence this warning.
// Warning: (163-166): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning: (245-248): Underflow (resulting value less than 0) happens here
@@ -0,0 +1,32 @@
pragma experimental SMTChecker;
contract C{
uint x;
constructor(uint y) public {
assert(x == 1);
x = 1;
}
function f() public {
assert(x == 2);
++x;
g();
assert(x == 2);
}
function g() internal {
assert(x == 3);
--x;
assert(x == 2);
}
}
// ----
// Warning: (70-76): Unused function parameter. Remove or comment out the variable name to silence this warning.
// Warning: (145-159): Assertion violation happens here
// Warning: (163-166): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning: (227-241): Assertion violation happens here
// Warning: (252-266): Assertion violation happens here
// Warning: (177-191): Assertion violation happens here
// Warning: (227-241): Assertion violation happens here
// Warning: (245-248): Underflow (resulting value less than 0) happens here
// Warning: (252-266): Assertion violation happens here
// Warning: (89-103): Assertion violation happens here
@@ -0,0 +1,21 @@
pragma experimental SMTChecker;
contract A {
uint x;
function f() internal {
assert(x == 1);
--x;
}
}
contract C is A {
constructor() public {
assert(x == 0);
++x;
f();
assert(x == 0);
}
}
// ----
// Warning: (100-103): Underflow (resulting value less than 0) happens here
// Warning: (100-103): Underflow (resulting value less than 0) happens here
@@ -0,0 +1,26 @@
pragma experimental SMTChecker;
contract A {
uint x;
function f() internal {
assert(x == 2);
--x;
}
}
contract C is A {
constructor() public {
assert(x == 1);
++x;
f();
assert(x == 1);
}
}
// ----
// Warning: (82-96): Assertion violation happens here
// Warning: (100-103): Underflow (resulting value less than 0) happens here
// Warning: (82-96): Assertion violation happens here
// Warning: (100-103): Underflow (resulting value less than 0) happens here
// Warning: (155-169): Assertion violation happens here
// Warning: (82-96): Assertion violation happens here
// Warning: (187-201): Assertion violation happens here
@@ -0,0 +1,27 @@
pragma experimental SMTChecker;
contract C{
uint x;
constructor(uint y) public {
assert(x == 0);
x = 1;
}
function f() public {
assert(x == 1);
++x;
++x;
g();
g();
assert(x == 1);
}
function g() internal {
--x;
}
}
// ----
// Warning: (70-76): Unused function parameter. Remove or comment out the variable name to silence this warning.
// Warning: (163-166): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning: (170-173): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning: (241-244): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning: (241-244): Underflow (resulting value less than 0) happens here
@@ -0,0 +1,30 @@
pragma experimental SMTChecker;
contract C{
uint x;
constructor(uint y) public {
assert(x == 1);
x = 1;
}
function f() public {
assert(x == 2);
++x;
++x;
g();
g();
assert(x == 3);
}
function g() internal {
--x;
}
}
// ----
// Warning: (70-76): Unused function parameter. Remove or comment out the variable name to silence this warning.
// Warning: (145-159): Assertion violation happens here
// Warning: (163-166): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning: (170-173): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning: (241-244): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning: (191-205): Assertion violation happens here
// Warning: (241-244): Underflow (resulting value less than 0) happens here
// Warning: (89-103): Assertion violation happens here
@@ -0,0 +1,18 @@
pragma experimental SMTChecker;
contract C {
function g(uint y) public {
uint z = L.f(y);
assert(z == y);
}
}
library L {
function f(uint x) internal returns (uint) {
return x;
}
}
// ----
// Warning: (131-190): Function state mutability can be restricted to pure
// Warning: (86-87): Assertion checker does not yet implement type type(library L)
@@ -0,0 +1,26 @@
pragma experimental SMTChecker;
library l1 {
uint private constant TON = 1000;
function f1() public pure {
assert(TON == 1000);
assert(TON == 2000);
}
function f2(uint x, uint y) internal pure returns (uint) {
return x + y;
}
}
contract C {
function f(uint x) public pure {
uint z = l1.f2(x, 1);
assert(z == x + 1);
}
}
// ----
// Warning: (136-155): Assertion violation happens here
// Warning: (229-234): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning: (300-302): Assertion checker does not yet implement type type(library l1)
// Warning: (229-234): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning: (327-332): Overflow (resulting value larger than 2**256 - 1) happens here
@@ -0,0 +1,9 @@
pragma experimental SMTChecker;
library l1 {
uint private constant TON = 1000;
function f1() public pure {
assert(TON == 1000);
}
}
@@ -9,4 +9,3 @@ contract C {
}
//
// ----
// Warning: (126-129): Assertion checker does not support recursive function calls.
@@ -25,4 +25,3 @@ a;
// ----
// Warning: (72-90): Statement has no effect.
// Warning: (96-107): Statement has no effect.
// Warning: (304-307): Assertion checker does not support recursive function calls.
@@ -26,4 +26,5 @@ contract A is B {
}
// ----
// Warning: (261-266): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning: (261-266): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning: (356-370): Assertion violation happens here
@@ -24,4 +24,10 @@ contract A is B {
// ----
// 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: (230-235): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning: (171-176): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning: (260-265): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning: (282-287): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning: (282-291): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning: (308-313): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning: (296-314): Assertion violation happens here
@@ -23,4 +23,9 @@ contract A is B {
// ----
// Warning: (171-177): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning: (231-236): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning: (171-177): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning: (261-266): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning: (283-289): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning: (306-311): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning: (294-312): Assertion violation happens here
@@ -13,5 +13,3 @@ contract C {
}
}
// ----
// Warning: (162-175): Assertion violation happens here
// Warning: (179-193): Assertion violation happens here
@@ -1,5 +1,8 @@
pragma experimental SMTChecker;
// This test gets different results on Linux and OSX.
// Re-enable when fixed (SMTSolvers: z3)
contract Simple {
function f() public pure {
uint x = 10;
@@ -16,4 +19,7 @@ contract Simple {
}
}
// ====
// SMTSolvers: z3
// SMTSolvers: none
// ----
// Warning: (195-209): Error trying to invoke SMT solver.
// Warning: (195-209): Assertion violation happens here
@@ -12,5 +12,4 @@ contract Simple {
assert(y == x);
}
}
// ====
// SMTSolvers: z3
// ----
@@ -5,10 +5,6 @@ contract C
function f(uint x, bool b) public pure {
require(x < 10);
for (; x < 10; ) {
if (b) {
x = 20;
continue;
}
++x;
}
assert(x > 15);
@@ -17,4 +13,5 @@ contract C
// ====
// SMTSolvers: z3
// ----
// Warning: (185-199): Assertion violation happens here
// Warning: (66-72): Unused function parameter. Remove or comment out the variable name to silence this warning.
// Warning: (142-156): Assertion violation happens here
@@ -13,8 +13,6 @@ contract C
assert(x > 0);
}
}
// ====
// SMTSolvers: z3
// ----
// Warning: (296-309): Error trying to invoke SMT solver.
// Warning: (176-181): Overflow (resulting value larger than 2**256 - 1) happens here
@@ -14,8 +14,6 @@ contract LoopFor2 {
assert(b[0] == 900);
}
}
// ====
// SMTSolvers: z3
// ----
// Warning: (281-301): Assertion violation happens here
// Warning: (305-324): Assertion violation happens here
@@ -12,12 +12,12 @@ contract LoopFor2 {
b[i] = i + 1;
c[i] = b[i];
}
// This is safe but too hard to solve currently.
assert(b[0] == c[0]);
assert(a[0] == 900);
assert(b[0] == 900);
}
}
// ====
// SMTSolvers: z3
// ----
// Warning: (312-331): Assertion violation happens here
// Warning: (316-336): Assertion violation happens here
// Warning: (363-382): Assertion violation happens here
@@ -12,13 +12,13 @@ contract LoopFor2 {
b[i] = i + 1;
c[i] = b[i];
}
// This is safe but too hard to prove currently.
assert(b[0] == c[0]);
assert(a[0] == 900);
assert(b[0] == 900);
}
}
// ====
// SMTSolvers: z3
// ----
// Warning: (290-309): Assertion violation happens here
// Warning: (313-332): Assertion violation happens here
// Warning: (317-337): Assertion violation happens here
// Warning: (341-360): Assertion violation happens here
// Warning: (364-383): Assertion violation happens here
@@ -4,6 +4,7 @@ contract C {
function f(uint x, uint y) public pure {
x = 7;
while ((x = y) > 0) {
--y;
}
assert(x == 7);
}
@@ -11,4 +12,4 @@ contract C {
// ====
// SMTSolvers: z3
// ----
// Warning: (216-230): Assertion violation happens here
// Warning: (224-238): Assertion violation happens here
@@ -28,8 +28,6 @@ contract C
assert(x >= 20);
}
}
// ====
// SMTSolvers: z3
// ----
// Warning: (329-344): Assertion violation happens here
// Warning: (380-395): Assertion violation happens here
@@ -26,8 +26,6 @@ contract C
assert(x >= 20);
}
}
// ====
// SMTSolvers: z3
// ----
// Warning: (323-338): Assertion violation happens here
// Warning: (362-377): Assertion violation happens here
@@ -21,4 +21,5 @@ contract C
}
}
// ----
// Warning: (203-208): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning: (136-149): Assertion violation happens here
@@ -17,6 +17,3 @@ contract C
}
}
// ----
// Warning: (86-93): Assertion checker does not support recursive function calls.
// Warning: (86-93): Assertion checker does not support recursive function calls.
// Warning: (253-266): Assertion violation happens here
@@ -4,7 +4,7 @@ contract C
{
uint[][] a;
function f(bool b) public {
require(a[2][3] == 4);
a[2][3] = 4;
if (b)
delete a;
else
@@ -15,3 +15,5 @@ contract C
}
// ====
// SMTSolvers: z3
// ----
// Warning: (174-194): Assertion violation happens here
@@ -20,6 +20,7 @@ contract C
// Warning: (165-204): Assertion violation happens here
// Warning: (208-240): Assertion violation happens here
// Warning: (244-275): Assertion violation happens here
// Warning: (311-316): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning: (304-332): Assertion violation happens here
// Warning: (336-352): Assertion violation happens here
// Warning: (356-379): Assertion violation happens here
@@ -1,13 +1,23 @@
pragma experimental SMTChecker;
contract C {
function(uint) returns (uint) a;
function(uint) returns (uint) b;
function f(function(uint) returns (uint) g, function(uint) returns (uint) h) internal {
assert(g(2) == h(2));
assert(g == h);
}
function g() public {
f(a, b);
}
}
// ----
// Warning: (146-150): Assertion checker does not yet implement this type of function call.
// Warning: (154-158): Assertion checker does not yet implement this type of function call.
// Warning: (170-176): Assertion checker does not yet implement the type function (uint256) returns (uint256) for comparisons
// Warning: (139-159): Assertion violation happens here
// Warning: (163-177): Assertion violation happens here
// Warning: (214-218): Assertion checker does not yet implement this type of function call.
// Warning: (222-226): Assertion checker does not yet implement this type of function call.
// Warning: (238-244): Assertion checker does not yet implement the type function (uint256) returns (uint256) for comparisons
// Warning: (207-227): Assertion violation happens here
// Warning: (231-245): Assertion violation happens here
// Warning: (214-218): Assertion checker does not yet implement this type of function call.
// Warning: (222-226): Assertion checker does not yet implement this type of function call.
// Warning: (238-244): Assertion checker does not yet implement the type function (uint256) returns (uint256) for comparisons
// Warning: (207-227): Assertion violation happens here
// Warning: (231-245): Assertion violation happens here
@@ -10,5 +10,4 @@ contract B {
}
// ----
// Warning: (162-184): Assertion violation happens here
// Warning: (136-158): Assertion violation happens here
// Warning: (162-184): Assertion violation happens here
@@ -1,4 +1,5 @@
pragma experimental SMTChecker;
pragma experimental ABIEncoderV2;
contract C
{
@@ -8,24 +9,21 @@ contract C
uint[][] memory cc,
uint8[][] memory dd,
uint[][][] memory eee
) internal pure {
require(a[0] == 2);
require(cc[0][0] == 50);
require(dd[0][0] == 10);
require(eee[0][0][0] == 50);
) public pure {
a[0] = 2;
cc[0][0] = 50;
dd[0][0] = 10;
eee[0][0][0] = 50;
b[0] = 1;
// Fails because b == a is possible.
assert(a[0] == 2);
// Fails because b == cc[0] is possible.
assert(cc[0][0] == 50);
// Fails because
// b == a is possible
// b == cc[0] is possible
// b == ee[0][0] is possible
assert(a[0] == 2 || cc[0][0] == 50 || eee[0][0][0] == 50);
// Should not fail since knowledge is erased only for uint[].
assert(dd[0][0] == 10);
// Fails because b == ee[0][0] is possible.
assert(eee[0][0][0] == 50);
assert(b[0] == 1);
}
}
// ----
// Warning: (345-362): Assertion violation happens here
// Warning: (409-431): Assertion violation happens here
// Warning: (571-597): Assertion violation happens here
// Warning: (400-457): Assertion violation happens here
@@ -1,11 +1,12 @@
pragma experimental SMTChecker;
pragma experimental ABIEncoderV2;
contract C
{
uint[] array;
function f(uint[] memory a, uint[] memory b) internal view {
require(array[0] == 42);
require(a[0] == 2);
function f(uint[] memory a, uint[] memory b) public {
array[0] = 42;
a[0] = 2;
b[0] = 1;
// Erasing knowledge about memory references should not
// erase knowledge about state variables.
@@ -15,4 +16,4 @@ contract C
}
}
// ----
// Warning: (314-331): Assertion violation happens here
// Warning: (321-338): Assertion violation happens here
@@ -1,12 +1,13 @@
pragma experimental SMTChecker;
pragma experimental ABIEncoderV2;
contract C
{
uint[] array;
function f(uint[] memory a, uint[] memory b) internal view {
require(array[0] == 42);
function f(uint[] memory a, uint[] memory b) public {
array[0] = 42;
uint[] storage c = array;
require(a[0] == 2);
a[0] = 2;
b[0] = 1;
// Erasing knowledge about memory references should not
// erase knowledge about state variables.
@@ -19,4 +20,4 @@ contract C
}
}
// ----
// Warning: (469-486): Assertion violation happens here
// Warning: (476-493): Assertion violation happens here
@@ -4,7 +4,9 @@ contract C
{
uint[] array;
uint[][] array2d;
uint[][][][] array4d;
uint8[] tinyArray;
uint8[][][] tinyArray3d;
function f(
uint[] storage a,
uint[] storage b,
@@ -12,13 +14,13 @@ contract C
uint8[][] storage dd,
uint[][][] storage eee
) internal {
require(a[0] == 2);
require(array[0] == 42);
require(array2d[0][0] == 42);
require(tinyArray[0] == 42);
require(cc[0][0] == 42);
require(dd[0][0] == 42);
require(eee[0][0][0] == 42);
a[0] = 2;
array[0] = 42;
array2d[0][0] = 42;
tinyArray[0] = 42;
cc[0][0] = 42;
dd[0][0] = 42;
eee[0][0][0] = 42;
b[0] = 1;
// Fails because b == a is possible.
assert(a[0] == 2);
@@ -36,10 +38,19 @@ contract C
assert(eee[0][0][0] == 42);
assert(b[0] == 1);
}
function g(uint a, uint b, uint c, uint d, uint e) public {
f(array2d[a], array2d[b], array4d[c][c], tinyArray3d[d], array4d[e]);
}
}
// ----
// Warning: (489-506): Assertion violation happens here
// Warning: (553-575): Assertion violation happens here
// Warning: (627-654): Assertion violation happens here
// Warning: (795-817): Assertion violation happens here
// Warning: (957-983): Assertion violation happens here
// Warning: (468-485): Assertion violation happens here
// Warning: (532-554): Assertion violation happens here
// Warning: (606-633): Assertion violation happens here
// Warning: (774-796): Assertion violation happens here
// Warning: (936-962): Assertion violation happens here
// Warning: (468-485): Assertion violation happens here
// Warning: (532-554): Assertion violation happens here
// Warning: (606-633): Assertion violation happens here
// Warning: (774-796): Assertion violation happens here
// Warning: (936-962): Assertion violation happens here
@@ -2,9 +2,14 @@ pragma experimental SMTChecker;
contract C
{
uint[][] array2d;
function g(uint x, uint y, uint[] memory c) public {
f(array2d[x], array2d[y], c);
}
function f(uint[] storage a, uint[] storage b, uint[] memory c) internal {
require(c[0] == 42);
require(a[0] == 2);
c[0] = 42;
a[0] = 2;
b[0] = 1;
// Erasing knowledge about storage references should not
// erase knowledge about memory references.
@@ -15,4 +20,5 @@ contract C
}
}
// ----
// Warning: (347-364): Assertion violation happens here
// Warning: (436-453): Assertion violation happens here
// Warning: (436-453): Assertion violation happens here
@@ -2,10 +2,14 @@ pragma experimental SMTChecker;
contract C
{
uint[][] array2d;
function g(uint x, uint y, uint[] memory c) public {
f(array2d[x], array2d[y], c);
}
function f(uint[] storage a, uint[] storage b, uint[] memory c) internal {
uint[] memory d = c;
require(c[0] == 42);
require(a[0] == 2);
c[0] = 42;
a[0] = 2;
b[0] = 1;
// Erasing knowledge about storage references should not
// erase knowledge about memory references.
@@ -19,4 +23,7 @@ contract C
}
}
// ----
// Warning: (497-514): Assertion violation happens here
// Warning: (524-542): Assertion violation happens here
// Warning: (585-602): Assertion violation happens here
// Warning: (524-542): Assertion violation happens here
// Warning: (585-602): Assertion violation happens here
@@ -3,9 +3,10 @@ pragma experimental SMTChecker;
contract C
{
uint[] array;
uint[][] array2d;
function f(uint[] storage a, uint[] storage b) internal {
require(a[0] == 2);
require(b[0] == 42);
a[0] = 2;
b[0] = 42;
array[0] = 1;
// Fails because array == a is possible.
assert(a[0] == 2);
@@ -13,7 +14,12 @@ contract C
assert(b[0] == 42);
assert(array[0] == 1);
}
function g(uint x, uint y) public {
f(array2d[x], array2d[y]);
}
}
// ----
// Warning: (226-243): Assertion violation happens here
// Warning: (290-308): Assertion violation happens here
// Warning: (225-242): Assertion violation happens here
// Warning: (289-307): Assertion violation happens here
// Warning: (225-242): Assertion violation happens here
// Warning: (289-307): Assertion violation happens here
@@ -4,20 +4,29 @@ contract C
{
uint[] b;
uint[] d;
uint[][] array2d;
function g(uint x, uint[] memory c) public {
f(array2d[x], c);
}
function f(uint[] storage a, uint[] memory c) internal {
require(d[0] == 42);
require(c[0] == 42);
require(a[0] == 2);
d[0] = 42;
c[0] = 42;
a[0] = 2;
b[0] = 1;
// Erasing knowledge about storage variables should not
// erase knowledge about memory references.
assert(c[0] == 42);
// Should not fail since b == d is not possible.
// Fails because d == a is possible.
assert(d[0] == 42);
// Fails because b == a is possible.
// Fails because b == a and d == a are possible.
assert(a[0] == 2);
// b == a is possible, but does not fail because b
// was the last assignment.
assert(b[0] == 1);
}
}
// ----
// Warning: (446-463): Assertion violation happens here
// Warning: (431-449): Assertion violation happens here
// Warning: (504-521): Assertion violation happens here
// Warning: (431-449): Assertion violation happens here
// Warning: (504-521): Assertion violation happens here
@@ -7,9 +7,9 @@ contract C
mapping (uint => uint8)[] severalMaps8;
mapping (uint => uint)[][] severalMaps3d;
function f(mapping (uint => uint) storage map) internal {
require(severalMaps[0][0] == 42);
require(severalMaps8[0][0] == 42);
require(severalMaps3d[0][0][0] == 42);
severalMaps[0][0] = 42;
severalMaps8[0][0] = 42;
severalMaps3d[0][0][0] = 42;
map[0] = 2;
// Should fail since map == severalMaps[0] is possible.
assert(severalMaps[0][0] == 42);
@@ -18,7 +18,12 @@ contract C
// Should fail since map == severalMaps3d[0][0] is possible.
assert(severalMaps3d[0][0][0] == 42);
}
function g(uint x) public {
f(severalMaps[x]);
}
}
// ----
// Warning: (451-482): Assertion violation happens here
// Warning: (665-701): Assertion violation happens here
// Warning: (421-452): Assertion violation happens here
// Warning: (635-671): Assertion violation happens here
// Warning: (421-452): Assertion violation happens here
// Warning: (635-671): Assertion violation happens here
@@ -8,9 +8,9 @@ contract C
mapping (uint => uint)[][] severalMaps3d;
function f(mapping (uint => uint) storage map) internal {
map[0] = 42;
require(severalMaps[0][0] == 42);
require(severalMaps8[0][0] == 42);
require(severalMaps3d[0][0][0] == 42);
severalMaps[0][0] = 42;
severalMaps8[0][0] = 42;
severalMaps3d[0][0][0] = 42;
singleMap[0] = 2;
// Should not fail since singleMap == severalMaps[0] is not possible.
assert(severalMaps[0][0] == 42);
@@ -21,6 +21,10 @@ contract C
// Should fail since singleMap == map is possible.
assert(map[0] == 42);
}
function g(uint x) public {
f(severalMaps[x]);
}
}
// ----
// Warning: (807-827): Assertion violation happens here
// Warning: (777-797): Assertion violation happens here
// Warning: (777-797): Assertion violation happens here
@@ -2,7 +2,7 @@ pragma experimental SMTChecker;
contract C
{
function f(uint[2] memory a, uint[2] memory b, uint[2] memory c) internal pure {
function f(uint[2] memory a, uint[2] memory b, uint[2] memory c) public pure {
require(c[0] == 42);
require(a[0] == 2);
b[0] = 1;
@@ -14,5 +14,5 @@ contract C
}
}
// ----
// Warning: (230-248): Assertion violation happens here
// Warning: (295-312): Assertion violation happens here
// Warning: (228-246): Assertion violation happens here
// Warning: (293-310): Assertion violation happens here
@@ -2,18 +2,25 @@ pragma experimental SMTChecker;
contract C
{
uint[2] b;
uint[2] b1;
uint[2] b2;
function f(uint[2] storage a, uint[2] memory c) internal {
require(c[0] == 42);
require(a[0] == 2);
b[0] = 1;
c[0] = 42;
a[0] = 2;
b1[0] = 1;
// Erasing knowledge about storage variables should not
// erase knowledge about memory references.
assert(c[0] == 42);
// Fails because b == a is possible.
// Fails because b1 == a is possible.
assert(a[0] == 2);
assert(b[0] == 1);
assert(b1[0] == 1);
}
function g(bool x, uint[2] memory c) public {
if (x) f(b1, c);
else f(b2, c);
}
}
// ----
// Warning: (342-359): Assertion violation happens here
// Warning: (338-355): Assertion violation happens here
// Warning: (338-355): Assertion violation happens here
// Warning: (338-355): Assertion violation happens here
@@ -7,9 +7,9 @@ contract C
mapping (uint => uint8)[2] severalMaps8;
mapping (uint => uint)[2][2] severalMaps3d;
function f(mapping (uint => uint) storage map) internal {
require(severalMaps[0][0] == 42);
require(severalMaps8[0][0] == 42);
require(severalMaps3d[0][0][0] == 42);
severalMaps[0][0] = 42;
severalMaps8[0][0] = 42;
severalMaps3d[0][0][0] = 42;
map[0] = 2;
// Should fail since map == severalMaps[0] is possible.
assert(severalMaps[0][0] == 42);
@@ -18,7 +18,12 @@ contract C
// Should fail since map == severalMaps3d[0][0] is possible.
assert(severalMaps3d[0][0][0] == 42);
}
function g(uint x) public {
f(severalMaps[x]);
}
}
// ----
// Warning: (455-486): Assertion violation happens here
// Warning: (669-705): Assertion violation happens here
// Warning: (425-456): Assertion violation happens here
// Warning: (639-675): Assertion violation happens here
// Warning: (425-456): Assertion violation happens here
// Warning: (639-675): Assertion violation happens here
@@ -8,9 +8,9 @@ contract C
mapping (uint => uint)[2][2] severalMaps3d;
function f(mapping (uint => uint) storage map) internal {
map[0] = 42;
require(severalMaps[0][0] == 42);
require(severalMaps8[0][0] == 42);
require(severalMaps3d[0][0][0] == 42);
severalMaps[0][0] = 42;
severalMaps8[0][0] = 42;
severalMaps3d[0][0][0] = 42;
singleMap[0] = 2;
// Should not fail since singleMap == severalMaps[0] is not possible.
assert(severalMaps[0][0] == 42);
@@ -21,6 +21,10 @@ contract C
// Should fail since singleMap == map is possible.
assert(map[0] == 42);
}
function g(uint x) public {
f(severalMaps3d[x][0]);
}
}
// ----
// Warning: (811-831): Assertion violation happens here
// Warning: (781-801): Assertion violation happens here
// Warning: (781-801): Assertion violation happens here
@@ -8,7 +8,7 @@ library L
contract C
{
enum E { Left, Right }
function f(E _d) internal pure {
function f(E _d) public pure {
_d = E.Left;
assert(_d == E.Left);
}
@@ -8,10 +8,10 @@ library L
contract C
{
enum E { Left, Right }
function f(E _d) internal pure {
function f(E _d) public pure {
_d = E.Right;
assert(_d == E.Left);
}
}
// ----
// Warning: (161-181): Assertion violation happens here
// Warning: (159-179): Assertion violation happens here
@@ -1,19 +1,20 @@
pragma experimental SMTChecker;
pragma experimental ABIEncoderV2;
contract C
{
enum D { Left, Right }
struct S { uint x; D d; }
function f(S memory s) internal pure {
function f(S memory s) public pure {
s.d = D.Left;
assert(s.d == D.Left);
}
}
// ----
// Warning: (109-119): Assertion checker does not yet support the type of this variable.
// Warning: (139-142): Assertion checker does not yet support this expression.
// Warning: (139-140): Assertion checker does not yet implement type struct C.S memory
// Warning: (139-151): Assertion checker does not yet implement such assignments.
// Warning: (162-165): Assertion checker does not yet support this expression.
// Warning: (162-163): Assertion checker does not yet implement type struct C.S memory
// Warning: (155-176): Assertion violation happens here
// Warning: (143-153): Assertion checker does not yet support the type of this variable.
// Warning: (171-174): Assertion checker does not yet support this expression.
// Warning: (171-172): Assertion checker does not yet implement type struct C.S memory
// Warning: (171-183): Assertion checker does not yet implement such assignments.
// Warning: (194-197): Assertion checker does not yet support this expression.
// Warning: (194-195): Assertion checker does not yet implement type struct C.S memory
// Warning: (187-208): Assertion violation happens here
@@ -0,0 +1,15 @@
pragma experimental SMTChecker;
contract C
{
bytes32 x;
function f(bytes8 y) public view {
assert(x == g());
assert(x != y);
}
function g() public view returns (bytes32) {
return x;
}
}
// ----
// Warning: (116-130): Assertion violation happens here
@@ -0,0 +1,10 @@
pragma experimental SMTChecker;
contract K {
function f() public pure {
(abi.encode, 2);
}
}
// ----
// Warning: (76-91): Statement has no effect.
// Warning: (77-80): Assertion checker does not yet implement type abi
@@ -0,0 +1,10 @@
pragma experimental SMTChecker;
contract K {
function f() public pure {
(abi.encode, "");
}
}
// ----
// Warning: (76-92): Statement has no effect.
// Warning: (77-80): Assertion checker does not yet implement type abi
@@ -3,9 +3,12 @@ contract C {
function f(function(uint) external payable g) internal {
g.selector;
g.gas(2).value(3)(4);
g{gas: 2, value: 3}(4);
}
}
// ----
// Warning: (122-127): Using ".gas(...)" is deprecated. Use "{gas: ...}" instead.
// Warning: (122-136): Using ".value(...)" is deprecated. Use "{value: ...}" instead.
// Warning: (108-118): Assertion checker does not yet support this expression.
// Warning: (122-130): Assertion checker does not yet implement this type of function call.
// Warning: (122-139): Assertion checker does not yet implement this type of function call.
@@ -5,8 +5,9 @@ contract C
mapping (uint => uint) a;
mapping (uint => uint) b;
function f() public {
require(a[1] == b[1]);
function f(uint x) public {
a[1] = x;
b[1] = x;
a[1] = 2;
mapping (uint => uint) storage c = a;
assert(c[1] == 2);
@@ -15,4 +16,4 @@ contract C
}
}
// ----
// Warning: (261-281): Assertion violation happens here
// Warning: (266-286): Assertion violation happens here
@@ -6,10 +6,10 @@ contract C
mapping (uint => mapping (uint => uint)) maps;
mapping (uint => mapping (uint => uint8)) maps8;
function f(mapping (uint => uint) storage map1, mapping (uint => uint) storage map2) internal {
require(map1[0] == 2);
require(a[0] == 42);
require(maps[0][0] == 42);
require(maps8[0][0] == 42);
map1[0] = 2;
a[0] = 42;
maps[0][0] = 42;
maps8[0][0] = 42;
map2[0] = 1;
// Fails because map2 == map1 is possible.
assert(map1[0] == 2);
@@ -21,8 +21,21 @@ contract C
assert(maps8[0][0] == 42);
assert(map2[0] == 1);
}
function g(bool b, uint x, uint y) public {
if (b)
f(a, maps[y]);
else
f(maps[x], maps[y]);
}
}
// ----
// Warning: (437-457): Assertion violation happens here
// Warning: (503-521): Assertion violation happens here
// Warning: (573-597): Assertion violation happens here
// Warning: (397-417): Assertion violation happens here
// Warning: (463-481): Assertion violation happens here
// Warning: (533-557): Assertion violation happens here
// Warning: (397-417): Assertion violation happens here
// Warning: (463-481): Assertion violation happens here
// Warning: (533-557): Assertion violation happens here
// Warning: (397-417): Assertion violation happens here
// Warning: (463-481): Assertion violation happens here
// Warning: (533-557): Assertion violation happens here
@@ -11,3 +11,4 @@ contract C {
}
// ----
// Warning: (147-166): Assertion violation happens here
// Warning: (170-190): Assertion violation happens here
@@ -15,3 +15,4 @@ contract C
}
// ----
// Warning: (182-196): Assertion violation happens here
// Warning: (200-214): Assertion violation happens here
@@ -17,3 +17,4 @@ contract C
}
// ----
// Warning: (205-219): Assertion violation happens here
// Warning: (223-237): Assertion violation happens here
@@ -0,0 +1,9 @@
pragma experimental SMTChecker;
contract C {
function f() public pure {
(("", 2));
}
}
// ----
// Warning: (76-85): Statement has no effect.
@@ -0,0 +1,9 @@
pragma experimental SMTChecker;
contract C {
function f() public pure {
(("", ""));
}
}
// ----
// Warning: (76-86): Statement has no effect.
@@ -0,0 +1,9 @@
pragma experimental SMTChecker;
contract C {
function f() public pure {
(2);
}
}
// ----
// Warning: (76-79): Statement has no effect.
@@ -3,7 +3,7 @@
{
"smtlib2responses":
{
"0x82fb8ee094f0f56b7a63a74177b54a1710d6fc531d426f288c18f36b76cf6a8b": "sat\n((|EVALEXPR_0| 1))\n",
"0x9c50514d749eabf3c13d97ad7d787e682dd99a114bad652b10a01b8c6ad6c1fb": "sat\n((|EVALEXPR_0| 1))\n",
"0xb524e7c577188e2e36f0e67fead51269fa0f8b8fb41bff2d973dcf584d38cd1e": "sat\n((|EVALEXPR_0| 0))\n"
}
}
@@ -0,0 +1,10 @@
contract C {
constructor() public payable { }
}
contract D {
function createC() public returns (C) {
C c = (new C){value: 1}();
return c;
}
}
@@ -0,0 +1,11 @@
contract C {
function f() public pure {
assembly {
function f() {
// Make sure this doesn't trigger the unimplemented assertion in the control flow builder.
leave
}
}
}
}
// ----

Some files were not shown because too many files have changed in this diff Show More