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

SMTChecker: Bring back counterexample checks in regression tests

Browse Source 
Since the default is now to ignore the counterexamples when checking
test output, we bring back counterexample checks in tests where the
counterexample is (mostly) deterministic.
This commit is contained in:
Martin Blicha 2023-07-24 18:33:43 +02:00
parent 2e38798408
commit cdfc19b503
56 changed files with 147 additions and 57 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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.