Skip to content

Commit 08f11e6

Browse files
matheusaaguiarmatheusaaguiar
committed
[WIP] Updated smt tests
1 parent 5396e44 commit 08f11e6

12 files changed

+15
-24
lines changed

‎test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_array_slice.sol‎

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -27,8 +27,6 @@ contract C {
2727
// SMTIgnoreCex: yes
2828
// SMTIgnoreOS: macos
2929
// ----
30-
// Warning 6328: (325-355): CHC: Assertion violation happens here.
30+
// Warning 6328: (325-355): CHC: Assertion violation happens here.\nCounterexample:\n\nsel = 0x0\ndata = [0x52]\nb2 = [0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53]\nb3 = []\nb4 = []\nx = 0\ny = 0\nb5 = []\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiEncodeSlice(0x0, [0x52])
3131
// Warning 6328: (578-608): CHC: Assertion violation happens here.
32-
// Warning 6328: (691-721): CHC: Assertion violation happens here.
33-
// Warning 6328: (959-989): CHC: Assertion violation happens here.
34-
// Warning 6328: (1079-1109): CHC: Assertion violation happens here.
32+
// Info 1391: CHC: 3 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

‎test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_array_slice_2.sol‎

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -29,6 +29,4 @@ contract C {
2929
// ----
3030
// Warning 6328: (326-356): CHC: Assertion violation happens here.
3131
// Warning 6328: (579-609): CHC: Assertion violation happens here.
32-
// Warning 6328: (692-722): CHC: Assertion violation happens here.
33-
// Warning 6328: (960-990): CHC: Assertion violation happens here.
34-
// Warning 6328: (1080-1110): CHC: Assertion violation happens here.
32+
// Info 1391: CHC: 3 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

‎test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_vs_sig.sol‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -12,4 +12,4 @@ contract C {
1212
// SMTIgnoreOS: macos
1313
// ----
1414
// Warning 6328: (330-360): CHC: Assertion violation might happen here.
15-
// Warning 4661: (330-360): BMC: Assertion violation happens here.
15+
// Warning 7812: (330-360): BMC: Assertion violation might happen here.

‎test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_array_slice.sol‎

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -24,11 +24,9 @@ contract C {
2424
}
2525
// ====
2626
// SMTEngine: chc
27-
// SMTIgnoreOS: macos
2827
// SMTIgnoreCex: yes
28+
// SMTIgnoreOS: macos
2929
// ----
3030
// Warning 6328: (334-364): CHC: Assertion violation happens here.
3131
// Warning 6328: (588-618): CHC: Assertion violation happens here.
32-
// Warning 6328: (702-732): CHC: Assertion violation happens here.
33-
// Warning 6328: (971-1001): CHC: Assertion violation happens here.
34-
// Warning 6328: (1086-1116): CHC: Assertion violation happens here.
32+
// Info 1391: CHC: 3 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

‎test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_array_slice_2.sol‎

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -24,11 +24,9 @@ contract C {
2424
}
2525
// ====
2626
// SMTEngine: chc
27-
// SMTIgnoreOS: macos
2827
// SMTIgnoreCex: yes
28+
// SMTIgnoreOS: macos
2929
// ----
3030
// Warning 6328: (335-365): CHC: Assertion violation happens here.
3131
// Warning 6328: (589-619): CHC: Assertion violation happens here.
32-
// Warning 6328: (703-733): CHC: Assertion violation happens here.
33-
// Warning 6328: (972-1002): CHC: Assertion violation happens here.
34-
// Warning 6328: (1087-1117): CHC: Assertion violation happens here.
32+
// Info 1391: CHC: 3 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

‎test/libsolidity/smtCheckerTests/bmc_coverage/compound_bitwise_or_uint_3.sol‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -12,4 +12,4 @@ contract C {
1212
// SMTEngine: bmc
1313
// SMTShowUnproved: no
1414
// ----
15-
// Info 6002: BMC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
15+
// 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.

‎test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_2.sol‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -50,5 +50,5 @@ contract C {
5050
// SMTIgnoreOS: macos
5151
// ----
5252
// Warning 6328: (434-455): CHC: Assertion violation happens here.
53-
// Warning 6328: (1270-1291): CHC: Assertion violation happens here.
53+
// Warning 6328: (1270-1291): CHC: Assertion violation might happen here.
5454
// Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

‎test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_3.sol‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -42,5 +42,5 @@ contract C {
4242
// SMTExtCalls: trusted
4343
// SMTIgnoreOS: macos
4444
// ----
45-
// Warning 6328: (561-582): CHC: Assertion violation happens here.
45+
// Warning 6328: (561-582): CHC: Assertion violation might happen here.
4646
// Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

‎test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_5.sol‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -47,5 +47,5 @@ contract C {
4747
// SMTEngine: chc
4848
// SMTExtCalls: trusted
4949
// ----
50-
// Warning 6328: (601-622): CHC: Assertion violation happens here.
50+
// Warning 6328: (601-622): CHC: Assertion violation might happen here.
5151
// Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

‎test/libsolidity/smtCheckerTests/functions/getters/array_2.sol‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -19,5 +19,5 @@ contract C {
1919
// SMTEngine: all
2020
// SMTIgnoreCex: no
2121
// ----
22-
// 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()
22+
// Warning 6328: (242-256): CHC: Assertion violation happens here.
2323
// Info 1391: CHC: 7 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

0 commit comments

Comments
 (0)