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 #14446 from ethereum/smt-cex-tests

Browse Source 
SMTChecker tests: Keep counterexamples when updating expectations
This commit is contained in:
Martin Blicha 2023-07-25 19:52:26 +02:00 committed by GitHub
commit 95beef4072
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
58 changed files with 159 additions and 57 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
test/libsolidity/SMTCheckerTest.cpp
View File

@ -140,6 +140,7 @@ TestCase::TestResult SMTCheckerTest::run(ostream& _stream, string const& _linePr
void SMTCheckerTest::filterObtainedErrors()
{
SyntaxTest::filterObtainedErrors();
m_unfilteredErrorList = m_errorList;
static auto removeCex = [](vector<SyntaxTestError>& errors) {
for (auto& e: errors)
@ -156,3 +157,10 @@ void SMTCheckerTest::filterObtainedErrors()
removeCex(m_errorList);
}
}
void SMTCheckerTest::printUpdatedExpectations(ostream &_stream, const string &_linePrefix) const {
if (!m_unfilteredErrorList.empty())
printErrorList(_stream, m_unfilteredErrorList, _linePrefix, false);
else
CommonSyntaxTest::printUpdatedExpectations(_stream, _linePrefix);
}

4
test/libsolidity/SMTCheckerTest.h
View File

@ -42,6 +42,8 @@ public:
void filterObtainedErrors() override;
void printUpdatedExpectations(std::ostream& _stream, std::string const& _linePrefix) const override;
protected:
/*
Options that can be set in the test:
@ -62,6 +64,8 @@ protected:
ModelCheckerSettings m_modelCheckerSettings;
bool m_ignoreCex = false;
std::vector<SyntaxTestError> m_unfilteredErrorList;
};
}

1
test/libsolidity/smtCheckerTests/array_members/pop_1_unsafe.sol
View File

@ -6,5 +6,6 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: no
// ----
// Warning 2529: (49-56): CHC: Empty array "pop" happens here.\nCounterexample:\na = []\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f()

1
test/libsolidity/smtCheckerTests/array_members/pop_constructor_unsafe.sol
View File

@ -6,5 +6,6 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: no
// ----
// Warning 2529: (43-50): CHC: Empty array "pop" happens here.\nCounterexample:\na = []\n\nTransaction trace:\nC.constructor()

3
test/libsolidity/smtCheckerTests/array_members/push_zero_unsafe.sol
View File

@ -7,6 +7,7 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: no
// ----
// Warning 6328: (61-91): CHC: Assertion violation happens here.
// Warning 6328: (61-91): CHC: Assertion violation happens here.\nCounterexample:\na = [0]\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f()
// Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

3
test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_fail.sol
View File

@ -14,6 +14,7 @@ contract c {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: no
// ----
// Warning 6328: (194-203): CHC: Assertion violation happens here.
// Warning 6328: (194-203): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n = false\nb = false\n\nTransaction trace:\nc.constructor()\nState: x = 0\nc.g()\n c.f() -- internal call\n c.f() -- internal call
// Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

3
test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_need_both_fail.sol
View File

@ -14,6 +14,7 @@ contract c {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: no
// ----
// Warning 6328: (192-202): CHC: Assertion violation happens here.
// Warning 6328: (192-202): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n = false\nb = true\n\nTransaction trace:\nc.constructor()\nState: x = 0\nc.g()\n c.f() -- internal call\n c.f() -- internal call
// Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

3
test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_fail.sol
View File

@ -14,6 +14,7 @@ contract c {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: no
// ----
// Warning 6328: (192-202): CHC: Assertion violation happens here.
// Warning 6328: (192-202): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n = false\nb = true\n\nTransaction trace:\nc.constructor()\nState: x = 0\nc.g()\n c.f() -- internal call\n c.f() -- internal call
// Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

3
test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_need_both_fail.sol
View File

@ -14,6 +14,7 @@ contract c {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: no
// ----
// Warning 6328: (192-202): CHC: Assertion violation happens here.
// Warning 6328: (192-202): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n = false\nb = true\n\nTransaction trace:\nc.constructor()\nState: x = 0\nc.g()\n c.f() -- internal call\n c.f() -- internal call
// Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

4
test/libsolidity/smtCheckerTests/external_calls/call_mutex_unsafe.sol
View File

@ -21,7 +21,7 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// SMTIgnoreCex: no
// ----
// Warning 9302: (212-228): Return value of low-level calls not used.
// Warning 6328: (232-246): CHC: Assertion violation happens here.
// Warning 6328: (232-246): CHC: Assertion violation happens here.\nCounterexample:\nx = 0, lock = false\n_a = 0x0\ny = 1\n\nTransaction trace:\nC.constructor()\nState: x = 0, lock = false\nC.set(1)\nState: x = 1, lock = false\nC.f(0x0)\n _a.call("aaaaa") -- untrusted external call, synthesized as:\n C.set(0) -- reentrant call

3
test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_2.sol
View File

@ -12,5 +12,6 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: no
// ----
// Warning 6328: (117-131): CHC: Assertion violation happens here.
// Warning 6328: (117-131): CHC: Assertion violation happens here.\nCounterexample:\nlocked = false\ntarget = 0x0\n\nTransaction trace:\nC.constructor()\nState: locked = true\nC.call(0x0)\n D(target).e() -- untrusted external call, synthesized as:\n C.call(0x0) -- reentrant call

3
test/libsolidity/smtCheckerTests/external_calls/underflow_only_in_external_call.sol
View File

@ -18,6 +18,7 @@ contract C {
}
// ====
// SMTEngine: chc
// SMTIgnoreCex: no
// SMTTargets: underflow
// ----
// Warning 3944: (109-112): CHC: Underflow (resulting value less than 0) happens here.
// Warning 3944: (109-112): CHC: Underflow (resulting value less than 0) happens here.\nCounterexample:\nv = 0, guard = false\n = 0\n\nTransaction trace:\nC.constructor()\nState: v = 0, guard = true\nC.f()\n C.dec() -- trusted external call

3
test/libsolidity/smtCheckerTests/file_level/easy.sol
View File

@ -13,6 +13,7 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: no
// ----
// Warning 6328: (222-239): CHC: Assertion violation happens here.
// Warning 6328: (222-239): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g()\n C.f(7) -- internal call\n add(7, 2) -- internal call\n C.f(8) -- internal call\n add(8, 2) -- internal call
// Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

5
test/libsolidity/smtCheckerTests/file_level/struct.sol
View File

@ -22,7 +22,8 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: no
// ----
// Warning 6328: (317-333): CHC: Assertion violation happens here.
// Warning 6328: (352-371): CHC: Assertion violation happens here.
// Warning 6328: (317-333): CHC: Assertion violation happens here.\nCounterexample:\n\ns = {x: 2, a: [1]}\n\nTransaction trace:\nC.constructor()\nC.f()\n allocate(2, 1) -- internal call
// Warning 6328: (352-371): CHC: Assertion violation happens here.\nCounterexample:\n\ns = {x: 2, a: [1]}\n\nTransaction trace:\nC.constructor()\nC.f()\n allocate(2, 1) -- internal call
// Info 1391: CHC: 5 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

1
test/libsolidity/smtCheckerTests/functions/functions_identity_1_fail.sol
View File

@ -11,5 +11,6 @@ contract C
}
// ====
// SMTEngine: all
// SMTIgnoreCex: no
// ----
// Warning 6328: (129-142): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\n\nTransaction trace:\nC.constructor()\nC.g()\n C.h(0) -- internal call

1
test/libsolidity/smtCheckerTests/functions/functions_identity_2_fail.sol
View File

@ -15,5 +15,6 @@ contract C
}
// ====
// SMTEngine: all
// SMTIgnoreCex: no
// ----
// Warning 6328: (197-210): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\n\nTransaction trace:\nC.constructor()\nC.g()\n C.h(0) -- internal call\n C.k(0) -- internal call

4
test/libsolidity/smtCheckerTests/functions/getters/array_2.sol
View File

@ -17,7 +17,7 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// SMTIgnoreCex: no
// ----
// Warning 6328: (242-256): CHC: Assertion violation happens here.
// Warning 6328: (242-256): CHC: Assertion violation happens here.\nCounterexample:\na = [[], [], [0, 0, 0, 0]]\ny = 0\n\nTransaction trace:\nC.constructor()\nState: a = [[], [], [0, 0, 0, 0]]\nC.f()
// Info 1391: CHC: 7 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

3
test/libsolidity/smtCheckerTests/functions/getters/array_of_structs_2.sol
View File

@ -18,6 +18,7 @@ contract D {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: no
// ----
// Warning 6328: (267-281): CHC: Assertion violation happens here.
// Warning 6328: (267-281): CHC: Assertion violation happens here.\nCounterexample:\nitems = [{x: 42, y: 43}]\na = 42\nb = 43\n\nTransaction trace:\nD.constructor()\nState: items = []\nD.test()
// Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

3
test/libsolidity/smtCheckerTests/functions/getters/mapping_1.sol
View File

@ -9,6 +9,7 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: no
// ----
// Warning 6328: (142-156): CHC: Assertion violation happens here.
// Warning 6328: (142-156): CHC: Assertion violation happens here.\nCounterexample:\n\ny = 0\n\nTransaction trace:\nC.constructor()\nC.f()
// Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

3
test/libsolidity/smtCheckerTests/functions/getters/mapping_2.sol
View File

@ -9,6 +9,7 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: no
// ----
// Warning 6328: (166-180): CHC: Assertion violation happens here.
// Warning 6328: (166-180): CHC: Assertion violation happens here.\nCounterexample:\n\ny = 0\n\nTransaction trace:\nC.constructor()\nC.f()
// Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

3
test/libsolidity/smtCheckerTests/functions/getters/struct_1.sol
View File

@ -26,6 +26,7 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: no
// ----
// Warning 6328: (338-355): CHC: Assertion violation happens here.
// Warning 6328: (338-355): CHC: Assertion violation happens here.\nCounterexample:\ns = {x: 0, t: {t: 0}, b: false, a: []}\ny = 0\nc = false\nt = {t: 0}\n\nTransaction trace:\nC.constructor()\nState: s = {x: 0, t: {t: 0}, b: false, a: []}\nC.f()
// Info 1391: CHC: 3 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

3
test/libsolidity/smtCheckerTests/functions/getters/struct_2.sol
View File

@ -16,6 +16,7 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: no
// ----
// Warning 6328: (175-189): CHC: Assertion violation happens here.
// Warning 6328: (175-189): CHC: Assertion violation happens here.\nCounterexample:\ns = {a: [0, 0], u: 0}\nu = 0\n\nTransaction trace:\nC.constructor()\nState: s = {a: [0, 0], u: 0}\nC.f()
// Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

5
test/libsolidity/smtCheckerTests/functions/getters/struct_with_reassignment.sol
View File

@ -27,7 +27,8 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: no
// ----
// Warning 6328: (255-272): CHC: Assertion violation happens here.
// Warning 6328: (377-391): CHC: Assertion violation happens here.
// Warning 6328: (255-272): CHC: Assertion violation happens here.\nCounterexample:\ns = {x: 1, b: false}\nx = 1\nb = false\ny = 0\nc = false\n\nTransaction trace:\nC.constructor()\nState: s = {x: 1, b: false}\nC.f()
// Warning 6328: (377-391): CHC: Assertion violation happens here.\nCounterexample:\ns = {x: 42, b: false}\nx = 1\nb = false\ny = 42\nc = false\n\nTransaction trace:\nC.constructor()\nState: s = {x: 1, b: false}\nC.f()
// Info 1391: CHC: 3 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

3
test/libsolidity/smtCheckerTests/functions/getters/uint.sol
View File

@ -9,6 +9,7 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: no
// ----
// Warning 6328: (114-128): CHC: Assertion violation happens here.
// Warning 6328: (114-128): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\ny = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f()
// Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

5
test/libsolidity/smtCheckerTests/functions/super_function_assert.sol
View File

@ -28,7 +28,8 @@ contract D is C {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: no
// ----
// Warning 6328: (205-219): CHC: Assertion violation happens here.
// Warning 6328: (328-342): CHC: Assertion violation happens here.
// Warning 6328: (205-219): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n\nTransaction trace:\nC.constructor()\nState: x = 0\nA.proxy()\n C.f() -- internal call\n A.f() -- internal call
// Warning 6328: (328-342): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n\nTransaction trace:\nD.constructor()\nState: x = 0\nA.proxy()\n D.f() -- internal call\n C.f() -- internal call\n A.f() -- internal call
// Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

3
test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_1.sol
View File

@ -14,6 +14,7 @@ contract C is B {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: no
// ----
// Warning 6328: (52-66): CHC: Assertion violation happens here.
// Warning 6328: (52-66): CHC: Assertion violation happens here.\nCounterexample:\ny = 0, x = 1\n\nTransaction trace:\nC.constructor()\nState: y = 0, x = 0\nC.g()\n B.f() -- internal call
// Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

3
test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_2.sol
View File

@ -21,6 +21,7 @@ contract C is B {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: no
// ----
// Warning 6328: (54-68): CHC: Assertion violation happens here.
// Warning 6328: (54-68): CHC: Assertion violation happens here.\nCounterexample:\ny = 0, z = 0, w = 0, a = 0, b = 0, x = 1\n\nTransaction trace:\nC.constructor()\nState: y = 0, z = 0, w = 0, a = 0, b = 0, x = 0\nC.g()\n A.f() -- internal call
// Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

3
test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_3.sol
View File

@ -27,6 +27,7 @@ contract C is B {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: no
// ----
// Warning 6328: (64-78): CHC: Assertion violation happens here.
// Warning 6328: (64-78): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.g()\n B.f() -- internal call\n A.f() -- internal call\n C.v() -- internal call
// Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

3
test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_4.sol
View File

@ -34,6 +34,7 @@ contract C is B, A1 {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: no
// ----
// Warning 6328: (64-78): CHC: Assertion violation happens here.
// Warning 6328: (64-78): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.g()\n C.f() -- internal call\n A1.f() -- internal call\n B.f() -- internal call\n A.f() -- internal call\n C.v() -- internal call
// Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

3
test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_5.sol
View File

@ -28,6 +28,7 @@ contract C is B {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: no
// ----
// Warning 6328: (97-111): CHC: Assertion violation happens here.
// Warning 6328: (97-111): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.g()\n B.f() -- internal call\n A.f() -- internal call\n C.v() -- internal call\n A.v() -- internal call
// Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

3
test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_6.sol
View File

@ -30,6 +30,7 @@ contract C is B {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: no
// ----
// Warning 6328: (183-197): CHC: Assertion violation happens here.
// Warning 6328: (183-197): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nA.constructor()\nState: x = 0\nA.g()\n A.v() -- internal call
// Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

3
test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_7.sol
View File

@ -21,6 +21,7 @@ contract C is A {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: no
// ----
// Warning 6328: (56-70): CHC: Assertion violation happens here.
// Warning 6328: (56-70): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.g()\n A.f() -- internal call\n C.v() -- internal call
// Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

1
test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_8.sol
View File

@ -14,5 +14,6 @@ contract C is A {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: no
// ----
// Warning 6328: (61-75): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nA.f()

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

@ -27,7 +27,8 @@ contract C is B {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: no
// ----
// Warning 6328: (62-76): CHC: Assertion violation happens here.
// Warning 6328: (131-145): CHC: Assertion violation happens here.
// 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
// Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

3
test/libsolidity/smtCheckerTests/inheritance/diamond_super_1.sol
View File

@ -28,6 +28,7 @@ contract D is B, C {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: no
// ----
// Warning 6328: (437-452): CHC: Assertion violation happens here.
// Warning 6328: (437-452): CHC: Assertion violation happens here.\nCounterexample:\n\nr = 15\n\nTransaction trace:\nD.constructor()\nD.f()\n C.f() -- internal call\n B.f() -- internal call\n A.f() -- internal call
// Info 1391: CHC: 4 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

5
test/libsolidity/smtCheckerTests/inheritance/diamond_super_2.sol
View File

@ -29,7 +29,8 @@ contract D is B, C {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: no
// ----
// Warning 6328: (443-458): CHC: Assertion violation happens here.
// Warning 6328: (477-492): CHC: Assertion violation happens here.
// Warning 6328: (443-458): CHC: Assertion violation happens here.\nCounterexample:\n\nr = 22\n\nTransaction trace:\nD.constructor()\nD.f()\n C.f() -- internal call\n B.f() -- internal call\n A.f() -- internal call
// Warning 6328: (477-492): CHC: Assertion violation happens here.\nCounterexample:\n\nr = 22\n\nTransaction trace:\nD.constructor()\nD.f()\n C.f() -- internal call\n B.f() -- internal call\n A.f() -- internal call
// Info 1391: CHC: 5 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

3
test/libsolidity/smtCheckerTests/inheritance/diamond_super_3.sol
View File

@ -31,6 +31,7 @@ contract E is C,D {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: no
// ----
// Warning 6328: (379-394): CHC: Assertion violation happens here.
// Warning 6328: (379-394): CHC: Assertion violation happens here.\nCounterexample:\nx = 111\n\nTransaction trace:\nE.constructor()\nState: x = 0\nE.f()\n C.f() -- internal call\n B.f() -- internal call\n A.f() -- internal call
// Info 1391: CHC: 3 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

1
test/libsolidity/smtCheckerTests/loops/while_loop_simple_1.sol
View File

@ -11,5 +11,6 @@ contract C {
// ====
// SMTEngine: all
// SMTSolvers: z3
// SMTIgnoreCex: no
// ----
// Warning 6328: (162-176): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 1\n\nTransaction trace:\nC.constructor()\nC.f(0)

5
test/libsolidity/smtCheckerTests/operators/assignment_chain_tuple_contract_2.sol
View File

@ -9,6 +9,9 @@ contract C {
assert(x != 2); // should fail
}
}
// ====
// SMTEngine: all
// SMTIgnoreCex: no
// ----
// Warning 6328: (174-188): CHC: Assertion violation happens here.
// Warning 6328: (174-188): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n\nTransaction trace:\nC.constructor()\nState: x = 2\nC.g()
// Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

7
test/libsolidity/smtCheckerTests/operators/assignment_chain_tuple_contract_3.sol
View File

@ -17,7 +17,10 @@ contract D is C {
assert(y == 3); // should hold
}
}
// ====
// SMTEngine: all
// SMTIgnoreCex: no
// ----
// Warning 6328: (95-109): CHC: Assertion violation happens here.
// Warning 6328: (180-194): CHC: Assertion violation happens here.
// Warning 6328: (95-109): CHC: Assertion violation happens here.\nCounterexample:\ny = 3, x = 3\n\nTransaction trace:\nD.constructor()\nState: y = 3, x = 3\nC.f()
// Warning 6328: (180-194): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n\nTransaction trace:\nC.constructor()\nState: x = 2\nC.g()
// Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

11
test/libsolidity/smtCheckerTests/operators/bitwise_and_int.sol
View File

@ -2,18 +2,19 @@ contract C {
function f() public pure {
int8 x = 1;
int8 y = 0;
assert(x & y != 0);
assert(x & y != 0); // should fail
x = -1; y = 3;
assert(x & y == 3);
assert(x & y == 3); // should hold
y = -1;
int8 z = x & y;
assert(z == -1);
assert(z == -1); // should hold
y = 127;
assert(x & y == 127);
assert(x & y == 127); // should hold
}
}
// ====
// SMTEngine: all
// SMTIgnoreCex: no
// ----
// Warning 6328: (71-89): CHC: Assertion violation happens here.
// Warning 6328: (71-89): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 1\ny = 0\nz = 0\n\nTransaction trace:\nC.constructor()\nC.f()
// Info 1391: CHC: 3 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

22
test/libsolidity/smtCheckerTests/operators/shifts/shift_cex.sol Normal file
View File

@ -0,0 +1,22 @@
contract C {
function left() public pure {
uint x = 0x4266;
assert(x << 0x0 == 0x4266);
// Fails because the above is true.
assert(x << 0x0 == 0x4268);
}
function right() public pure {
uint x = 0x4266;
assert(x >> 0x0 == 0x4266);
// Fails because the above is true.
assert(x >> 0x0 == 0x4268);
}
}
// ====
// SMTEngine: all
// SMTIgnoreCex: no
// ----
// Warning 6328: (133-159): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 16998\n\nTransaction trace:\nC.constructor()\nC.left()
// Warning 6328: (286-312): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 16998\n\nTransaction trace:\nC.constructor()\nC.right()
// Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

3
test/libsolidity/smtCheckerTests/operators/unary_add.sol
View File

@ -13,6 +13,7 @@ contract C
}
// ====
// SMTEngine: all
// SMTIgnoreCex: no
// ----
// Warning 6328: (161-174): CHC: Assertion violation happens here.
// Warning 6328: (161-174): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 4\na = 3\nb = 3\n\nTransaction trace:\nC.constructor()\nC.f()
// Info 1391: CHC: 5 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

3
test/libsolidity/smtCheckerTests/operators/unary_sub.sol
View File

@ -13,6 +13,7 @@ contract C
}
// ====
// SMTEngine: all
// SMTIgnoreCex: no
// ----
// Warning 6328: (161-174): CHC: Assertion violation happens here.
// Warning 6328: (161-174): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 3\na = 4\nb = 4\n\nTransaction trace:\nC.constructor()\nC.f()
// Info 1391: CHC: 5 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

1
test/libsolidity/smtCheckerTests/out_of_bounds/fixed_bytes_2.sol
View File

@ -5,5 +5,6 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: no
// ----
// Warning 6368: (83-87): CHC: Out of bounds access happens here.\nCounterexample:\n\nx = 0x0\ny = 4\n = 0x0\n\nTransaction trace:\nC.constructor()\nC.r(0x0, 4)

12
test/libsolidity/smtCheckerTests/simple/cex_smoke_test.sol Normal file
View File

@ -0,0 +1,12 @@
contract C {
function f() public pure {
uint x = 1;
assert(x == 2);
}
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6328: (73-87): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 1\n\nTransaction trace:\nC.constructor()\nC.f()

3
test/libsolidity/smtCheckerTests/try_catch/try_3.sol
View File

@ -21,7 +21,8 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: no
// ----
// Warning 5667: (259-273): Unused try/catch parameter. Remove or comment out the variable name to silence this warning.
// Warning 6328: (280-294): CHC: Assertion violation happens here.
// Warning 6328: (280-294): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\ns = []\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f()\n C.postinc() -- internal call
// Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

3
test/libsolidity/smtCheckerTests/types/array_literal_2.sol
View File

@ -10,6 +10,7 @@ contract C
}
// ====
// SMTEngine: all
// SMTIgnoreCex: no
// ----
// Warning 6328: (167-187): CHC: Assertion violation happens here.
// Warning 6328: (167-187): CHC: Assertion violation happens here.\nCounterexample:\n\na = [1, 2, 3]\nb = [1, 2, 4]\n\nTransaction trace:\nC.constructor()\nC.f()
// Info 1391: CHC: 8 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

1
test/libsolidity/smtCheckerTests/types/array_literal_3.sol
View File

@ -9,6 +9,7 @@ contract C
}
// ====
// SMTEngine: all
// SMTIgnoreCex: no
// ----
// Warning 6328: (168-188): CHC: Assertion violation happens here.
// Info 1391: CHC: 8 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

3
test/libsolidity/smtCheckerTests/types/array_literal_5.sol
View File

@ -12,6 +12,7 @@ contract C
}
// ====
// SMTEngine: all
// SMTIgnoreCex: no
// ----
// Warning 6328: (176-196): CHC: Assertion violation happens here.
// Warning 6328: (176-196): CHC: Assertion violation happens here.\nCounterexample:\ns = [1, 2, 3]\na = [1, 2, 3]\n\nTransaction trace:\nC.constructor()\nState: s = []\nC.f()
// Info 1391: CHC: 9 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

5
test/libsolidity/smtCheckerTests/types/array_literal_6.sol
View File

@ -13,7 +13,8 @@ contract C
}
// ====
// SMTEngine: all
// SMTIgnoreCex: no
// ----
// Warning 6328: (146-174): CHC: Assertion violation happens here.
// Warning 6328: (235-255): CHC: Assertion violation happens here.
// Warning 6328: (146-174): CHC: Assertion violation happens here.\nCounterexample:\n\na = [1, 2, 3]\nb = [1, 2, 4, 3]\nc = [1, 2, 4, 3]\n\nTransaction trace:\nC.constructor()\nC.f()
// Warning 6328: (235-255): CHC: Assertion violation happens here.\nCounterexample:\n\na = [1, 2, 3]\nb = [1, 2, 4, 3]\nc = [1, 2, 4, 3]\n\nTransaction trace:\nC.constructor()\nC.f()
// Info 1391: CHC: 11 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

1
test/libsolidity/smtCheckerTests/types/bool_simple_1.sol
View File

@ -5,5 +5,6 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: no
// ----
// Warning 6328: (58-67): CHC: Assertion violation happens here.\nCounterexample:\n\nx = false\n\nTransaction trace:\nC.constructor()\nC.f(false)

1
test/libsolidity/smtCheckerTests/types/mapping_1_fail.sol
View File

@ -9,5 +9,6 @@ contract C
}
// ====
// SMTEngine: all
// SMTIgnoreCex: no
// ----
// Warning 6328: (101-120): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 3\n\nTransaction trace:\nC.constructor()\nC.f(3)

3
test/libsolidity/smtCheckerTests/types/struct/struct_constructor_named_args.sol
View File

@ -19,6 +19,7 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: no
// ----
// Warning 6328: (232-255): CHC: Assertion violation happens here.
// Warning 6328: (232-255): CHC: Assertion violation happens here.\nCounterexample:\n\ninner = {x: 43}\nouter = {s: {x: 43}, y: 512}\n\nTransaction trace:\nC.constructor()\nC.test()
// Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

1
test/libsolidity/smtCheckerTests/types/tuple_function.sol
View File

@ -13,6 +13,7 @@ contract C
}
// ====
// SMTEngine: all
// SMTIgnoreCex: no
// ----
// Warning 6328: (149-163): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 2\ny = 3\n\nTransaction trace:\nC.constructor()\nC.g()\n C.f() -- internal call
// Warning 6328: (167-181): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 2\ny = 3\n\nTransaction trace:\nC.constructor()\nC.g()\n C.f() -- internal call

3
test/libsolidity/smtCheckerTests/types/tuple_function_2.sol
View File

@ -13,6 +13,7 @@ contract C
}
// ====
// SMTEngine: all
// SMTIgnoreCex: no
// ----
// Warning 6328: (166-180): CHC: Assertion violation happens here.
// Warning 6328: (166-180): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 2\ny = 0\n\nTransaction trace:\nC.constructor()\nC.g()\n C.f() -- internal call
// Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

5
test/libsolidity/smtCheckerTests/types/tuple_function_3.sol
View File

@ -15,7 +15,8 @@ contract C
}
// ====
// SMTEngine: all
// SMTIgnoreCex: no
// ----
// Warning 6328: (172-186): CHC: Assertion violation happens here.
// Warning 6328: (190-204): CHC: Assertion violation happens here.
// Warning 6328: (172-186): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\ny = 0\nb = false\n\nTransaction trace:\nC.constructor()\nC.g()\n C.f() -- internal call
// Warning 6328: (190-204): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\ny = 0\nb = false\n\nTransaction trace:\nC.constructor()\nC.g()\n C.f() -- internal call
// Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

3
test/libsolidity/smtCheckerTests/userTypes/constant.sol
View File

@ -14,6 +14,7 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: no
// ----
// Warning 6328: (531-555): CHC: Assertion violation happens here.
// Warning 6328: (531-555): CHC: Assertion violation happens here.\nCounterexample:\nu = 165521356710917456517261742455526507355687727119203895813322792776\n\nTransaction trace:\nC.constructor()\nState: u = 165521356710917456517261742455526507355687727119203895813322792776\nC.f()
// Info 1391: CHC: 3 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.