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

Tests

Browse Source
This commit is contained in:
Leo Alt 2021-07-02 15:05:24 +02:00
parent 700fe3e5d4
commit 3c1f555f71
35 changed files with 135 additions and 51 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
libsolidity/interface/StandardCompiler.cpp
View File

@ -958,7 +958,7 @@ std::variant<StandardCompiler::InputsAndSettings, Json::Value> StandardCompiler:
return formatFatalError("JSONError", "settings.modelChecker.showUnproved must be a Boolean value.");
ret.modelCheckerSettings.showUnproved = showUnproved.asBool();
}
if (modelCheckerSettings.isMember("solvers"))
{
auto const& solversArray = modelCheckerSettings["solvers"];

8
test/libsolidity/SMTCheckerTest.cpp
View File

@ -27,6 +27,14 @@ using namespace solidity::frontend::test;
SMTCheckerTest::SMTCheckerTest(string const& _filename): SyntaxTest(_filename, EVMVersion{})
{
auto const& showUnproved = m_reader.stringSetting("SMTShowUnproved", "yes");
if (showUnproved == "no")
m_modelCheckerSettings.showUnproved = false;
else if (showUnproved == "yes")
m_modelCheckerSettings.showUnproved = true;
else
BOOST_THROW_EXCEPTION(runtime_error("Invalid SMT \"show unproved\" choice."));
auto const& choice = m_reader.stringSetting("SMTSolvers", "any");
if (choice == "any")
m_modelCheckerSettings.solvers = smtutil::SMTSolverChoice::All();

8
test/libsolidity/smtCheckerTests/abi/abi_encode_packed_string_literal.sol
View File

@ -22,14 +22,14 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 6328: (226-256): CHC: Assertion violation happens here.
// Warning 1218: (310-340): CHC: Error trying to invoke SMT solver.
// Warning 6328: (310-340): CHC: Assertion violation might happen here.
// Warning 1218: (483-513): CHC: Error trying to invoke SMT solver.
// Warning 6328: (483-513): CHC: Assertion violation might happen here.
// Warning 1218: (568-598): CHC: Error trying to invoke SMT solver.
// Warning 6328: (568-598): CHC: Assertion violation might happen here.
// Warning 1218: (654-684): CHC: Error trying to invoke SMT solver.
// Warning 6328: (226-256): CHC: Assertion violation happens here.
// Warning 6328: (310-340): CHC: Assertion violation might happen here.
// Warning 6328: (483-513): CHC: Assertion violation might happen here.
// Warning 6328: (568-598): CHC: Assertion violation might happen here.
// Warning 6328: (654-684): CHC: Assertion violation might happen here.
// Warning 4661: (310-340): BMC: Assertion violation happens here.
// Warning 4661: (483-513): BMC: Assertion violation happens here.

35
test/libsolidity/smtCheckerTests/abi/abi_encode_packed_string_literal_no_unproved.sol Normal file
View File

@ -0,0 +1,35 @@
contract C {
function abiencodePackedStringLiteral() public pure {
bytes memory b1 = abi.encodePacked("");
bytes memory b2 = abi.encodePacked("");
// should hold, but currently fails due to string literal abstraction
assert(b1.length == b2.length);
bytes memory b3 = abi.encodePacked(bytes(""));
assert(b1.length == b3.length); // should fail
bytes memory b4 = abi.encodePacked(bytes24(""));
// should hold, but currently fails due to string literal abstraction
assert(b1.length == b4.length);
bytes memory b5 = abi.encodePacked(string(""));
assert(b1.length == b5.length); // should fail
bytes memory b6 = abi.encode("");
assert(b1.length == b6.length); // should fail
}
}
// ====
// SMTEngine: all
// SMTShowUnproved: no
// ----
// Warning 1218: (310-340): CHC: Error trying to invoke SMT solver.
// Warning 1218: (483-513): CHC: Error trying to invoke SMT solver.
// Warning 1218: (568-598): CHC: Error trying to invoke SMT solver.
// Warning 1218: (654-684): CHC: Error trying to invoke SMT solver.
// Warning 6328: (226-256): CHC: Assertion violation happens here.
// Warning 5840: CHC: 4 verification condition(s) could not be proved. Enable the model checker option "show unproved" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.
// Warning 4661: (310-340): BMC: Assertion violation happens here.
// Warning 4661: (483-513): BMC: Assertion violation happens here.
// Warning 4661: (568-598): BMC: Assertion violation happens here.
// Warning 4661: (654-684): BMC: Assertion violation happens here.

6
test/libsolidity/smtCheckerTests/abi/abi_encode_string_literal.sol
View File

@ -19,12 +19,12 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 6328: (208-238): CHC: Assertion violation happens here.
// Warning 1218: (286-316): CHC: Error trying to invoke SMT solver.
// Warning 6328: (286-316): CHC: Assertion violation might happen here.
// Warning 1218: (453-483): CHC: Error trying to invoke SMT solver.
// Warning 6328: (453-483): CHC: Assertion violation might happen here.
// Warning 1218: (532-562): CHC: Error trying to invoke SMT solver.
// Warning 6328: (208-238): CHC: Assertion violation happens here.
// Warning 6328: (286-316): CHC: Assertion violation might happen here.
// Warning 6328: (453-483): CHC: Assertion violation might happen here.
// Warning 6328: (532-562): CHC: Assertion violation might happen here.
// Warning 4661: (286-316): BMC: Assertion violation happens here.
// Warning 4661: (453-483): BMC: Assertion violation happens here.

6
test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_array_slice.sol
View File

@ -25,13 +25,13 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 1218: (691-721): CHC: Error trying to invoke SMT solver.
// Warning 1218: (959-989): CHC: Error trying to invoke SMT solver.
// Warning 1218: (1079-1109): CHC: Error trying to invoke SMT solver.
// Warning 6328: (325-355): CHC: Assertion violation happens here.
// Warning 6328: (578-608): CHC: Assertion violation happens here.
// Warning 1218: (691-721): CHC: Error trying to invoke SMT solver.
// Warning 6328: (691-721): CHC: Assertion violation might happen here.
// Warning 1218: (959-989): CHC: Error trying to invoke SMT solver.
// Warning 6328: (959-989): CHC: Assertion violation might happen here.
// Warning 1218: (1079-1109): CHC: Error trying to invoke SMT solver.
// Warning 6328: (1079-1109): CHC: Assertion violation might happen here.
// Warning 4661: (691-721): BMC: Assertion violation happens here.
// Warning 4661: (959-989): BMC: Assertion violation happens here.

6
test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_array_slice_2.sol
View File

@ -25,13 +25,13 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 1218: (692-722): CHC: Error trying to invoke SMT solver.
// Warning 1218: (960-990): CHC: Error trying to invoke SMT solver.
// Warning 1218: (1080-1110): CHC: Error trying to invoke SMT solver.
// Warning 6328: (326-356): CHC: Assertion violation happens here.
// Warning 6328: (579-609): CHC: Assertion violation happens here.
// Warning 1218: (692-722): CHC: Error trying to invoke SMT solver.
// Warning 6328: (692-722): CHC: Assertion violation might happen here.
// Warning 1218: (960-990): CHC: Error trying to invoke SMT solver.
// Warning 6328: (960-990): CHC: Assertion violation might happen here.
// Warning 1218: (1080-1110): CHC: Error trying to invoke SMT solver.
// Warning 6328: (1080-1110): CHC: Assertion violation might happen here.
// Warning 4661: (692-722): BMC: Assertion violation happens here.
// Warning 4661: (960-990): BMC: Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_hash.sol
View File

@ -14,8 +14,8 @@ contract C {
// SMTEngine: all
// ----
// Warning 1218: (333-371): CHC: Error trying to invoke SMT solver.
// Warning 6328: (333-371): CHC: Assertion violation might happen here.
// Warning 1218: (390-428): CHC: Error trying to invoke SMT solver.
// Warning 6328: (333-371): CHC: Assertion violation might happen here.
// Warning 6328: (390-428): CHC: Assertion violation might happen here.
// Warning 4661: (333-371): BMC: Assertion violation happens here.
// Warning 4661: (390-428): BMC: Assertion violation happens here.

8
test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_string_literal.sol
View File

@ -22,14 +22,14 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 6328: (252-282): CHC: Assertion violation happens here.
// Warning 1218: (347-377): CHC: Error trying to invoke SMT solver.
// Warning 6328: (347-377): CHC: Assertion violation might happen here.
// Warning 1218: (531-561): CHC: Error trying to invoke SMT solver.
// Warning 6328: (531-561): CHC: Assertion violation might happen here.
// Warning 1218: (627-657): CHC: Error trying to invoke SMT solver.
// Warning 6328: (627-657): CHC: Assertion violation might happen here.
// Warning 1218: (746-776): CHC: Error trying to invoke SMT solver.
// Warning 6328: (252-282): CHC: Assertion violation happens here.
// Warning 6328: (347-377): CHC: Assertion violation might happen here.
// Warning 6328: (531-561): CHC: Assertion violation might happen here.
// Warning 6328: (627-657): CHC: Assertion violation might happen here.
// Warning 6328: (746-776): CHC: Assertion violation might happen here.
// Warning 4661: (347-377): BMC: Assertion violation happens here.
// Warning 4661: (531-561): BMC: Assertion violation happens here.

6
test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_array_slice.sol
View File

@ -25,13 +25,13 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 1218: (702-732): CHC: Error trying to invoke SMT solver.
// Warning 1218: (971-1001): CHC: Error trying to invoke SMT solver.
// Warning 1218: (1086-1116): CHC: Error trying to invoke SMT solver.
// Warning 6328: (334-364): CHC: Assertion violation happens here.
// Warning 6328: (588-618): CHC: Assertion violation happens here.
// Warning 1218: (702-732): CHC: Error trying to invoke SMT solver.
// Warning 6328: (702-732): CHC: Assertion violation might happen here.
// Warning 1218: (971-1001): CHC: Error trying to invoke SMT solver.
// Warning 6328: (971-1001): CHC: Assertion violation might happen here.
// Warning 1218: (1086-1116): CHC: Error trying to invoke SMT solver.
// Warning 6328: (1086-1116): CHC: Assertion violation might happen here.
// Warning 4661: (702-732): BMC: Assertion violation happens here.
// Warning 4661: (971-1001): BMC: Assertion violation happens here.

6
test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_array_slice_2.sol
View File

@ -25,13 +25,13 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 1218: (703-733): CHC: Error trying to invoke SMT solver.
// Warning 1218: (972-1002): CHC: Error trying to invoke SMT solver.
// Warning 1218: (1087-1117): CHC: Error trying to invoke SMT solver.
// Warning 6328: (335-365): CHC: Assertion violation happens here.
// Warning 6328: (589-619): CHC: Assertion violation happens here.
// Warning 1218: (703-733): CHC: Error trying to invoke SMT solver.
// Warning 6328: (703-733): CHC: Assertion violation might happen here.
// Warning 1218: (972-1002): CHC: Error trying to invoke SMT solver.
// Warning 6328: (972-1002): CHC: Assertion violation might happen here.
// Warning 1218: (1087-1117): CHC: Error trying to invoke SMT solver.
// Warning 6328: (1087-1117): CHC: Assertion violation might happen here.
// Warning 4661: (703-733): BMC: Assertion violation happens here.
// Warning 4661: (972-1002): BMC: Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_hash.sol
View File

@ -14,8 +14,8 @@ contract C {
// SMTEngine: all
// ----
// Warning 1218: (337-375): CHC: Error trying to invoke SMT solver.
// Warning 6328: (337-375): CHC: Assertion violation might happen here.
// Warning 1218: (394-432): CHC: Error trying to invoke SMT solver.
// Warning 6328: (337-375): CHC: Assertion violation might happen here.
// Warning 6328: (394-432): CHC: Assertion violation might happen here.
// Warning 4661: (337-375): BMC: Assertion violation happens here.
// Warning 4661: (394-432): BMC: Assertion violation happens here.

8
test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_string_literal.sol
View File

@ -22,14 +22,14 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 6328: (261-291): CHC: Assertion violation happens here.
// Warning 1218: (357-387): CHC: Error trying to invoke SMT solver.
// Warning 6328: (357-387): CHC: Assertion violation might happen here.
// Warning 1218: (542-572): CHC: Error trying to invoke SMT solver.
// Warning 6328: (542-572): CHC: Assertion violation might happen here.
// Warning 1218: (639-669): CHC: Error trying to invoke SMT solver.
// Warning 6328: (639-669): CHC: Assertion violation might happen here.
// Warning 1218: (753-783): CHC: Error trying to invoke SMT solver.
// Warning 6328: (261-291): CHC: Assertion violation happens here.
// Warning 6328: (357-387): CHC: Assertion violation might happen here.
// Warning 6328: (542-572): CHC: Assertion violation might happen here.
// Warning 6328: (639-669): CHC: Assertion violation might happen here.
// Warning 6328: (753-783): CHC: Assertion violation might happen here.
// Warning 4661: (357-387): BMC: Assertion violation happens here.
// Warning 4661: (542-572): BMC: Assertion violation happens here.

15
test/libsolidity/smtCheckerTests/bmc_coverage/compound_bitwise_or_uint_3.sol Normal file
View File

@ -0,0 +1,15 @@
contract C {
struct S {
uint x;
}
S s;
function f(bool b) public {
s.x |= b ? 1 : 2;
assert(s.x > 0);
}
}
// ====
// SMTEngine: bmc
// SMTShowUnproved: no
// ----
// Warning 2788: BMC: 1 verification condition(s) could not be proved. Enable the model checker option "show unproved" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.

6
test/libsolidity/smtCheckerTests/crypto/crypto_functions_same_input_over_state_same_output_fail.sol
View File

@ -46,12 +46,12 @@ contract C {
// SMTEngine: all
// ----
// Warning 1218: (693-712): CHC: Error trying to invoke SMT solver.
// Warning 6328: (693-712): CHC: Assertion violation might happen here.
// Warning 1218: (716-735): CHC: Error trying to invoke SMT solver.
// Warning 6328: (716-735): CHC: Assertion violation might happen here.
// Warning 1218: (739-758): CHC: Error trying to invoke SMT solver.
// Warning 6328: (739-758): CHC: Assertion violation might happen here.
// Warning 1218: (762-781): CHC: Error trying to invoke SMT solver.
// Warning 6328: (693-712): CHC: Assertion violation might happen here.
// Warning 6328: (716-735): CHC: Assertion violation might happen here.
// Warning 6328: (739-758): CHC: Assertion violation might happen here.
// Warning 6328: (762-781): CHC: Assertion violation might happen here.
// Warning 4661: (693-712): BMC: Assertion violation happens here.
// Warning 4661: (716-735): BMC: Assertion violation happens here.

1
test/libsolidity/smtCheckerTests/external_calls/external_inc.sol
View File

@ -20,6 +20,5 @@ contract C {
// SMTIgnoreCex: yes
// ----
// Warning 4984: (113-116): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 4984: (113-116): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 6328: (156-170): CHC: Assertion violation happens here.
// Warning 2661: (113-116): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.

1
test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_crypto.sol
View File

@ -27,7 +27,6 @@ contract C {
// SMTEngine: all
// ----
// Warning 1218: (302-333): CHC: Error trying to invoke SMT solver.
// Warning 6328: (302-333): CHC: Assertion violation might happen here.
// Warning 1218: (302-333): CHC: Error trying to invoke SMT solver.
// Warning 6328: (302-333): CHC: Assertion violation might happen here.
// Warning 4661: (302-333): BMC: Assertion violation happens here.

1
test/libsolidity/smtCheckerTests/file_level/recursion.sol
View File

@ -25,4 +25,3 @@ contract C {
}
// ====
// SMTEngine: all
// ----

2
test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_3.sol
View File

@ -21,5 +21,5 @@ contract A is B {
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6328: (200-218): CHC: Assertion violation happens here.
// Warning 4984: (171-176): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 6328: (200-218): CHC: Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_4.sol
View File

@ -19,5 +19,5 @@ contract A is B {
// ====
// SMTEngine: all
// ----
// Warning 4984: (175-180): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\na = 0\nx = 115792089237316195423570985008687907853269984665640564039457584007913129639935\n\nTransaction trace:\nA.constructor(115792089237316195423570985008687907853269984665640564039457584007913129639935)
// Warning 4984: (166-171): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\na = 0\nx = 115792089237316195423570985008687907853269984665640564039457584007913129639934\n\nTransaction trace:\nA.constructor(115792089237316195423570985008687907853269984665640564039457584007913129639934)
// Warning 4984: (175-180): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\na = 0\nx = 115792089237316195423570985008687907853269984665640564039457584007913129639935\n\nTransaction trace:\nA.constructor(115792089237316195423570985008687907853269984665640564039457584007913129639935)

2
test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond_3.sol
View File

@ -29,6 +29,6 @@ contract A is B2, B1 {
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 4984: (209-214): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 4984: (193-198): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 4984: (209-214): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 6328: (302-318): CHC: Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/functions/constructor_state_value_parameter.sol
View File

@ -14,5 +14,5 @@ contract C {
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6328: (129-143): CHC: Assertion violation happens here.
// Warning 4984: (82-87): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 6328: (129-143): CHC: Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/functions/internal_call_with_assertion_1_fail.sol
View File

@ -21,8 +21,8 @@ contract C{
// SMTEngine: all
// ----
// Warning 5667: (37-43): Unused function parameter. Remove or comment out the variable name to silence this warning.
// Warning 6328: (49-63): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\ny = 0\n\nTransaction trace:\nC.constructor(0)
// Warning 6328: (105-119): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor(0)\nState: x = 1\nC.f()
// Warning 6328: (137-151): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor(0)\nState: x = 1\nC.f()\n C.g() -- internal call
// Warning 6328: (187-201): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n\nTransaction trace:\nC.constructor(0)\nState: x = 1\nC.f()\n C.g() -- internal call
// Warning 6328: (212-226): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor(0)\nState: x = 1\nC.f()\n C.g() -- internal call
// Warning 6328: (49-63): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\ny = 0\n\nTransaction trace:\nC.constructor(0)

2
test/libsolidity/smtCheckerTests/functions/internal_multiple_calls_with_assertion_1_fail.sol
View File

@ -21,6 +21,6 @@ contract C{
// SMTEngine: all
// ----
// Warning 5667: (37-43): Unused function parameter. Remove or comment out the variable name to silence this warning.
// Warning 6328: (49-63): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\ny = 0\n\nTransaction trace:\nC.constructor(0)
// Warning 6328: (105-119): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor(0)\nState: x = 1\nC.f()
// Warning 6328: (151-165): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor(0)\nState: x = 1\nC.f()\n C.g() -- internal call\n C.g() -- internal call
// Warning 6328: (49-63): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\ny = 0\n\nTransaction trace:\nC.constructor(0)

2
test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_9.sol
View File

@ -28,5 +28,5 @@ contract C is B {
// ====
// SMTEngine: all
// ----
// Warning 6328: (131-145): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nA.constructor()\nState: x = 0\nA.f()\n A.v() -- internal call
// Warning 6328: (62-76): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n\nTransaction trace:\nC.constructor()\nState: x = 0\nB.f()\n A.f() -- internal call\n C.v() -- internal call
// Warning 6328: (131-145): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nA.constructor()\nState: x = 0\nA.f()\n A.v() -- internal call

2
test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain_run_all.sol
View File

@ -23,6 +23,6 @@ contract A is B {
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6328: (243-261): CHC: Assertion violation happens here.
// Warning 4984: (125-130): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 4984: (184-189): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 6328: (243-261): CHC: Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain_run_all_2.sol
View File

@ -23,6 +23,6 @@ contract A is B {
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6328: (241-259): CHC: Assertion violation happens here.
// Warning 4984: (125-131): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 4984: (185-190): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 6328: (241-259): CHC: Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_diamond_middle.sol
View File

@ -25,5 +25,5 @@ contract D is B, C {
// ====
// SMTEngine: all
// ----
// Warning 6328: (223-237): CHC: Assertion violation happens here.\nCounterexample:\nx = 3\n\nTransaction trace:\nD.constructor()
// Warning 6328: (134-148): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n\nTransaction trace:\nD.constructor()
// Warning 6328: (223-237): CHC: Assertion violation happens here.\nCounterexample:\nx = 3\n\nTransaction trace:\nD.constructor()

2
test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_memory_memory.sol
View File

@ -24,5 +24,5 @@ contract LoopFor2 {
// ----
// Warning 2072: (202-217): Unused local variable.
// Warning 6368: (354-358): CHC: Out of bounds access happens here.
// Warning 6368: (378-382): CHC: Out of bounds access happens here.
// Warning 6368: (371-375): CHC: Out of bounds access happens here.
// Warning 6368: (378-382): CHC: Out of bounds access happens here.

1
test/libsolidity/smtCheckerTests/natspec/abstract_function_nondet_pow_no_abstraction.sol
View File

@ -35,4 +35,3 @@ contract C {
}
// ====
// SMTEngine: chc
// ----

2
test/libsolidity/smtCheckerTests/overflow/signed_div_overflow.sol
View File

@ -7,5 +7,5 @@ contract C {
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 4281: (77-82): CHC: Division by zero happens here.
// Warning 4984: (77-82): CHC: Overflow (resulting value larger than 0x80 * 2**248 - 1) happens here.
// Warning 4281: (77-82): CHC: Division by zero happens here.

2
test/libsolidity/smtCheckerTests/special/msg_value_inheritance_2.sol
View File

@ -14,5 +14,5 @@ contract C is A {
// ====
// SMTEngine: all
// ----
// Warning 6328: (240-254): CHC: Assertion violation happens here.\nCounterexample:\nv = 1, x = 1\n\nTransaction trace:\nC.constructor(){ value: 1 }
// Warning 6328: (60-74): CHC: Assertion violation happens here.\nCounterexample:\nv = 0, x = 1\n\nTransaction trace:\nC.constructor(){ value: 1 }
// Warning 6328: (240-254): CHC: Assertion violation happens here.\nCounterexample:\nv = 1, x = 1\n\nTransaction trace:\nC.constructor(){ value: 1 }

2
test/libsolidity/smtCheckerTests/typecast/string_literal_to_fixed_bytes_function_call.sol
View File

@ -11,5 +11,5 @@ contract B {
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6328: (130-152): CHC: Assertion violation happens here.
// Warning 6328: (104-126): CHC: Assertion violation happens here.
// Warning 6328: (130-152): CHC: Assertion violation happens here.

25
test/libsolidity/smtCheckerTests/types/array_branches_3d_show_unproved.sol Normal file
View File

@ -0,0 +1,25 @@
contract C
{
uint[][][] c;
constructor() {
c.push();
c[0].push();
c[0][0].push();
}
function f(bool b) public {
c[0][0][0] = 0;
if (b)
c[0][0][0] = 1;
assert(c[0][0][0] < 2);
}
}
// ====
// SMTEngine: all
// SMTShowUnproved: yes
// ----
// Warning 6368: (124-131): CHC: Out of bounds access might happen here.
// Warning 6368: (124-134): CHC: Out of bounds access might happen here.
// Warning 6368: (152-159): CHC: Out of bounds access might happen here.
// Warning 6368: (152-162): CHC: Out of bounds access might happen here.
// Warning 6368: (177-184): CHC: Out of bounds access might happen here.
// Warning 6368: (177-187): CHC: Out of bounds access might happen here.

5
test/solc/CommandLineParser.cpp
View File

@ -82,6 +82,7 @@ BOOST_AUTO_TEST_CASE(no_options)
expectedOptions.modelChecker.settings = {
ModelCheckerContracts::Default(),
ModelCheckerEngine::None(),
false,
smtutil::SMTSolverChoice::All(),
ModelCheckerTargets::Default(),
nullopt,
@ -151,6 +152,7 @@ BOOST_AUTO_TEST_CASE(cli_mode_options)
"--yul-optimizations=agf",
"--model-checker-contracts=contract1.yul:A,contract2.yul:B",
"--model-checker-engine=bmc",
"--model-checker-show-unproved=true",
"--model-checker-solvers=z3,smtlib2",
"--model-checker-targets=underflow,divByZero",
"--model-checker-timeout=5",
@ -209,6 +211,7 @@ BOOST_AUTO_TEST_CASE(cli_mode_options)
expectedOptions.modelChecker.settings = {
{{{"contract1.yul", {"A"}}, {"contract2.yul", {"B"}}}},
{true, false},
true,
{false, true, true},
{{VerificationTargetType::Underflow, VerificationTargetType::DivByZero}},
5,
@ -279,6 +282,7 @@ BOOST_AUTO_TEST_CASE(assembly_mode_options)
"contract1.yul:A,"
"contract2.yul:B",
"--model-checker-engine=bmc", // Ignored in assembly mode
"--model-checker-show-unproved=true", // Ignored in assembly mode
"--model-checker-solvers=z3,smtlib2", // Ignored in assembly mode
"--model-checker-targets=" // Ignored in assembly mode
"underflow,"
@ -377,6 +381,7 @@ BOOST_AUTO_TEST_CASE(standard_json_mode_options)
"contract1.yul:A,"
"contract2.yul:B",
"--model-checker-engine=bmc", // Ignored in Standard JSON mode
"--model-checker-show-unproved=true", // Ignored in Standard JSON mode
"--model-checker-solvers=z3,smtlib2", // Ignored in Standard JSON mode
"--model-checker-targets=" // Ignored in Standard JSON mode
"underflow,"