cerc-io/solidity
16
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Merge pull request #12037 from ethereum/smt_ignore_os

Browse Source 
Add isoltest option to ignore OS
This commit is contained in:
Leonardo 2021-10-01 13:29:32 +02:00 committed by GitHub
commit 089cad0319
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
2 changed files with 23 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

15
test/libsolidity/SMTCheckerTest.cpp
View File

@ -66,6 +66,21 @@ SMTCheckerTest::SMTCheckerTest(string const& _filename): SyntaxTest(_filename, E
m_ignoreCex = true;
else
BOOST_THROW_EXCEPTION(runtime_error("Invalid SMT counterexample choice."));
auto const& ignoreOSSetting = m_reader.stringSetting("SMTIgnoreOS", "none");
for (string const& os: ignoreOSSetting | ranges::views::split(',') | ranges::to<vector<string>>())
{
#ifdef __APPLE__
if (os == "macos")
m_shouldRun = false;
#elif _WIN32
if (os == "windows")
m_shouldRun = false;
#elif __linux__
if (os == "linux")
m_shouldRun = false;
#endif
}
}
TestCase::TestResult SMTCheckerTest::run(ostream& _stream, string const& _linePrefix, bool _formatted)

12
test/libsolidity/smtCheckerTests/external_calls/call_with_value_1.sol
View File

@ -2,13 +2,17 @@ contract C {
function g(address payable i) public {
require(address(this).balance == 100);
i.call{value: 10}("");
// Disabled due to Spacer nondeterminism
//assert(address(this).balance == 90); // should hold
// Disabled due to Spacer nondeterminism
//assert(address(this).balance == 100); // should fail
assert(address(this).balance == 90); // should hold
assert(address(this).balance == 100); // should fail
}
}
// ====
// SMTEngine: all
// SMTIgnoreOS: macos
// ----
// Warning 9302: (96-117): Return value of low-level calls not used.
// Warning 1218: (175-211): CHC: Error trying to invoke SMT solver.
// Warning 6328: (121-156): CHC: Assertion violation might happen here.
// Warning 6328: (175-211): CHC: Assertion violation might happen here.
// Warning 4661: (121-156): BMC: Assertion violation happens here.
// Warning 4661: (175-211): BMC: Assertion violation happens here.