cerc-io/solidity
10
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

[test] Update tests to include location string.

Browse Source
This commit is contained in:
Alexander Arlt 2022-04-01 22:45:12 -05:00
parent d4c02f2270
commit 0783ad9000
2684 changed files with 5877 additions and 5877 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
test/libsolidity/errorRecoveryTests/constructor_recovers.sol
View File

@ -16,5 +16,5 @@ contract Error1 {
}
}
// ----
// ParserError 6933: (88-89): Expected primary expression.
// Warning 3347: (88-89): Recovered in Statement at ';'.
// ParserError 6933: (88-89=';'): Expected primary expression.
// Warning 3347: (88-89=';'): Recovered in Statement at ';'.

4
test/libsolidity/errorRecoveryTests/contract_recovery.sol
View File

@ -3,5 +3,5 @@ contract Errort6 {
}
// ----
// ParserError 3546: (36-37): Expected type name
// Warning 3796: (59-60): Recovered in ContractDefinition at '}'.
// ParserError 3546: (36-37=';'): Expected type name
// Warning 3796: (59-60='}'): Recovered in ContractDefinition at '}'.

2
test/libsolidity/errorRecoveryTests/do_not_delete_at_error.sol
View File

@ -10,4 +10,4 @@ contract Error2 {
mapping (address => uint balances; // missing ) before "balances"
}
// ----
// ParserError 6635: (417-425): Expected ')' but got identifier
// ParserError 6635: (417-425='balances'): Expected ')' but got identifier

8
test/libsolidity/errorRecoveryTests/error_to_eos.sol
View File

@ -17,7 +17,7 @@ contract SendCoin {
}
// ----
// ParserError 6635: (212-220): Expected ')' but got identifier
// ParserError 6635: (220-221): Expected ';' but got ')'
// ParserError 9182: (220-221): Function, variable, struct or modifier declaration expected.
// Warning 3796: (235-236): Recovered in ContractDefinition at '}'.
// ParserError 6635: (212-220='balances'): Expected ')' but got identifier
// ParserError 6635: (220-221=')'): Expected ';' but got ')'
// ParserError 9182: (220-221=')'): Function, variable, struct or modifier declaration expected.
// Warning 3796: (235-236='}'): Recovered in ContractDefinition at '}'.

4
test/libsolidity/errorRecoveryTests/missing_rhs.sol
View File

@ -7,5 +7,5 @@ contract Error3 {
}
// ----
// ParserError 6933: (88-89): Expected primary expression.
// Warning 3347: (88-89): Recovered in Statement at ';'.
// ParserError 6933: (88-89=';'): Expected primary expression.
// Warning 3347: (88-89=';'): Recovered in Statement at ';'.

12
test/libsolidity/errorRecoveryTests/multiple_errors.sol
View File

@ -21,9 +21,9 @@ contract Error4 {
}
// ----
// ParserError 6635: (242-243): Expected ';' but got 'Number'
// ParserError 6635: (464-472): Expected ';' but got identifier
// ParserError 6635: (522-526): Expected ';' but got 'emit'
// ParserError 6635: (570-576): Expected ',' but got 'return'
// ParserError 6933: (570-576): Expected primary expression.
// Warning 3796: (581-582): Recovered in Statement at ';'.
// ParserError 6635: (242-243='2'): Expected ';' but got 'Number'
// ParserError 6635: (464-472='balances'): Expected ';' but got identifier
// ParserError 6635: (522-526='emit'): Expected ';' but got 'emit'
// ParserError 6635: (570-576='return'): Expected ',' but got 'return'
// ParserError 6933: (570-576='return'): Expected primary expression.
// Warning 3796: (581-582=';'): Recovered in Statement at ';'.

2
test/libsolidity/errorRecoveryTests/wrong_compiler_recovers_1.sol
View File

@ -1,3 +1,3 @@
pragma solidity ^99.99.0;
// ----
// SyntaxError 3997: (0-25): Source file requires different compiler version (current compiler is ....
// SyntaxError 3997: (0-25='pragma solidity ^99.99.0;'): Source file requires different compiler version (current compiler is ....

4
test/libsolidity/errorRecoveryTests/wrong_compiler_recovers_2.sol
View File

@ -1,6 +1,6 @@
pragma solidity ^99.99.0;
this is surely invalid
// ----
// ParserError 6635: (31-33): Expected identifier but got 'is'
// ParserError 6635: (34-40): Expected ';' but got identifier
// ParserError 6635: (31-33='is'): Expected identifier but got 'is'
// ParserError 6635: (34-40='surely'): Expected ';' but got identifier
// ParserError 6635: (49-49): Expected ';' but got end of source

4
test/libsolidity/errorRecoveryTests/wrong_compiler_recovers_3.sol
View File

@ -3,5 +3,5 @@ contract C {
uint ;
}
// ----
// ParserError 6635: (48-49): Expected identifier but got ';'
// ParserError 6635: (50-51): Expected ';' but got '}'
// ParserError 6635: (48-49=';'): Expected identifier but got ';'
// ParserError 6635: (50-51='}'): Expected ';' but got '}'

4
test/libsolidity/errorRecoveryTests/wrong_compiler_recovers_4.sol
View File

@ -3,5 +3,5 @@ contract C {
function f() {}
}
// ----
// SyntaxError 3997: (0-25): Source file requires different compiler version (current compiler is ....
// SyntaxError 4937: (43-58): No visibility specified. Did you intend to add "public"?
// SyntaxError 3997: (0-25='pragma solidity ^99.99.0;'): Source file requires different compiler version (current compiler is ....
// SyntaxError 4937: (43-58='function f() {}'): No visibility specified. Did you intend to add "public"?

18
test/libsolidity/smtCheckerTests/abi/abi_decode_array.sol
View File

@ -32,13 +32,13 @@ contract C {
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6328: (182-210): CHC: Assertion violation happens here.
// Warning 6328: (335-363): CHC: Assertion violation happens here.
// Warning 6328: (414-442): CHC: Assertion violation happens here.
// Warning 6328: (560-588): CHC: Assertion violation happens here.
// Warning 6328: (607-635): CHC: Assertion violation happens here.
// Warning 6328: (654-682): CHC: Assertion violation happens here.
// Warning 6328: (182-210='assert(a.length == b.length)'): CHC: Assertion violation happens here.
// Warning 6328: (335-363='assert(a.length == d.length)'): CHC: Assertion violation happens here.
// Warning 6328: (414-442='assert(b.length == c.length)'): CHC: Assertion violation happens here.
// Warning 6328: (560-588='assert(e.length == a.length)'): CHC: Assertion violation happens here.
// Warning 6328: (607-635='assert(f.length == b.length)'): CHC: Assertion violation happens here.
// Warning 6328: (654-682='assert(e.length == g.length)'): CHC: Assertion violation happens here.
// Warning 6328: (879-916): CHC: Assertion violation happens here.
// Warning 6328: (1009-1037): CHC: Assertion violation happens here.
// Warning 6328: (1056-1084): CHC: Assertion violation happens here.
// Warning 6328: (1103-1131): CHC: Assertion violation happens here.
// Warning 6328: (1009-1037='assert(k.length == a.length)'): CHC: Assertion violation happens here.
// Warning 6328: (1056-1084='assert(k.length == l.length)'): CHC: Assertion violation happens here.
// Warning 6328: (1103-1131='assert(l.length == b.length)'): CHC: Assertion violation happens here.

22
test/libsolidity/smtCheckerTests/abi/abi_decode_simple.sol
View File

@ -21,14 +21,14 @@ contract C {
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 1218: (505-519): CHC: Error trying to invoke SMT solver.
// Warning 1218: (538-552): CHC: Error trying to invoke SMT solver.
// Warning 6328: (209-223): CHC: Assertion violation happens here.
// Warning 6328: (260-274): CHC: Assertion violation happens here.
// Warning 6328: (359-373): CHC: Assertion violation happens here.
// Warning 6328: (392-406): CHC: Assertion violation happens here.
// Warning 6328: (425-434): CHC: Assertion violation happens here.
// Warning 6328: (505-519): CHC: Assertion violation might happen here.
// Warning 6328: (538-552): CHC: Assertion violation might happen here.
// Warning 4661: (505-519): BMC: Assertion violation happens here.
// Warning 4661: (538-552): BMC: Assertion violation happens here.
// Warning 1218: (505-519='assert(k == x)'): CHC: Error trying to invoke SMT solver.
// Warning 1218: (538-552='assert(l == y)'): CHC: Error trying to invoke SMT solver.
// Warning 6328: (209-223='assert(x == y)'): CHC: Assertion violation happens here.
// Warning 6328: (260-274='assert(z == w)'): CHC: Assertion violation happens here.
// Warning 6328: (359-373='assert(a == x)'): CHC: Assertion violation happens here.
// Warning 6328: (392-406='assert(b == y)'): CHC: Assertion violation happens here.
// Warning 6328: (425-434='assert(c)'): CHC: Assertion violation happens here.
// Warning 6328: (505-519='assert(k == x)'): CHC: Assertion violation might happen here.
// Warning 6328: (538-552='assert(l == y)'): CHC: Assertion violation might happen here.
// Warning 4661: (505-519='assert(k == x)'): BMC: Assertion violation happens here.
// Warning 4661: (538-552='assert(l == y)'): BMC: Assertion violation happens here.

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

@ -26,4 +26,4 @@ contract C {
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6328: (279-309): CHC: Assertion violation happens here.
// Warning 6328: (279-309='assert(b1.length == b2.length)'): CHC: Assertion violation happens here.

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

@ -26,7 +26,7 @@ contract C {
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 2072: (332-347): Unused local variable.
// Warning 2072: (618-633): Unused local variable.
// Warning 2072: (791-806): Unused local variable.
// Warning 6328: (280-310): CHC: Assertion violation happens here.
// Warning 2072: (332-347='bytes memory b3'): Unused local variable.
// Warning 2072: (618-633='bytes memory b4'): Unused local variable.
// Warning 2072: (791-806='bytes memory b5'): Unused local variable.
// Warning 6328: (280-310='assert(b1.length == b2.length)'): CHC: Assertion violation happens here.

18
test/libsolidity/smtCheckerTests/abi/abi_encode_call_simple.sol
View File

@ -15,12 +15,12 @@ contract C {
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6031: (233-249): Internal error: Expression undefined for SMT solver.
// Warning 6031: (298-314): Internal error: Expression undefined for SMT solver.
// Warning 6031: (398-414): Internal error: Expression undefined for SMT solver.
// Warning 1218: (330-360): CHC: Error trying to invoke SMT solver.
// Warning 1218: (430-460): CHC: Error trying to invoke SMT solver.
// Warning 6328: (330-360): CHC: Assertion violation might happen here.
// Warning 6328: (430-460): CHC: Assertion violation might happen here.
// Warning 4661: (330-360): BMC: Assertion violation happens here.
// Warning 4661: (430-460): BMC: Assertion violation happens here.
// Warning 6031: (233-249='this.callMeMaybe'): Internal error: Expression undefined for SMT solver.
// Warning 6031: (298-314='this.callMeMaybe'): Internal error: Expression undefined for SMT solver.
// Warning 6031: (398-414='this.callMeMaybe'): Internal error: Expression undefined for SMT solver.
// Warning 1218: (330-360='assert(b1.length == b2.length)'): CHC: Error trying to invoke SMT solver.
// Warning 1218: (430-460='assert(b1.length == b3.length)'): CHC: Error trying to invoke SMT solver.
// Warning 6328: (330-360='assert(b1.length == b2.length)'): CHC: Assertion violation might happen here.
// Warning 6328: (430-460='assert(b1.length == b3.length)'): CHC: Assertion violation might happen here.
// Warning 4661: (330-360='assert(b1.length == b2.length)'): BMC: Assertion violation happens here.
// Warning 4661: (430-460='assert(b1.length == b3.length)'): BMC: Assertion violation happens here.

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

@ -6,4 +6,4 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 6031: (54-60): Internal error: Expression undefined for SMT solver.
// Warning 6031: (54-60='this.f'): Internal error: Expression undefined for SMT solver.

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

@ -16,7 +16,7 @@ contract C {
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6328: (120-142): CHC: Assertion violation happens here.
// Warning 6328: (231-253): CHC: Assertion violation happens here.
// Warning 6328: (307-330): CHC: Assertion violation happens here.
// Warning 6328: (423-446): CHC: Assertion violation happens here.
// Warning 6328: (120-142='assert(res.length > 0)'): CHC: Assertion violation happens here.
// Warning 6328: (231-253='assert(res.length > 0)'): CHC: Assertion violation happens here.
// Warning 6328: (307-330='assert(res.length == 4)'): CHC: Assertion violation happens here.
// Warning 6328: (423-446='assert(res.length == 4)'): CHC: Assertion violation happens here.

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

@ -30,7 +30,7 @@ contract C {
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 2072: (127-142): Unused local variable.
// Warning 2072: (691-706): Unused local variable.
// Warning 2072: (1099-1114): Unused local variable.
// Warning 6328: (1047-1077): CHC: Assertion violation happens here.
// Warning 2072: (127-142='bytes memory b2'): Unused local variable.
// Warning 2072: (691-706='bytes memory b4'): Unused local variable.
// Warning 2072: (1099-1114='bytes memory b6'): Unused local variable.
// Warning 6328: (1047-1077='assert(b1.length == b5.length)'): CHC: Assertion violation happens here.

4
test/libsolidity/smtCheckerTests/abi/abi_encode_packed_array_slice_2.sol
View File

@ -30,5 +30,5 @@ contract C {
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 2072: (643-658): Unused local variable.
// Warning 6328: (298-328): CHC: Assertion violation happens here.
// Warning 2072: (643-658='bytes memory b4'): Unused local variable.
// Warning 6328: (298-328='assert(b1.length == b2.length)'): CHC: Assertion violation happens here.

24
test/libsolidity/smtCheckerTests/abi/abi_encode_packed_simple.sol
View File

@ -23,15 +23,15 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 1218: (322-352): CHC: Error trying to invoke SMT solver.
// Warning 1218: (419-449): CHC: Error trying to invoke SMT solver.
// Warning 1218: (528-558): CHC: Error trying to invoke SMT solver.
// Warning 1218: (577-607): CHC: Error trying to invoke SMT solver.
// Warning 6328: (322-352): CHC: Assertion violation might happen here.
// Warning 6328: (419-449): CHC: Assertion violation might happen here.
// Warning 6328: (528-558): CHC: Assertion violation might happen here.
// Warning 6328: (577-607): CHC: Assertion violation might happen here.
// Warning 4661: (322-352): BMC: Assertion violation happens here.
// Warning 4661: (419-449): BMC: Assertion violation happens here.
// Warning 4661: (528-558): BMC: Assertion violation happens here.
// Warning 4661: (577-607): BMC: Assertion violation happens here.
// Warning 1218: (322-352='assert(b1.length == b3.length)'): CHC: Error trying to invoke SMT solver.
// Warning 1218: (419-449='assert(b1.length == b4.length)'): CHC: Error trying to invoke SMT solver.
// Warning 1218: (528-558='assert(b1.length != b5.length)'): CHC: Error trying to invoke SMT solver.
// Warning 1218: (577-607='assert(b1.length == b5.length)'): CHC: Error trying to invoke SMT solver.
// Warning 6328: (322-352='assert(b1.length == b3.length)'): CHC: Assertion violation might happen here.
// Warning 6328: (419-449='assert(b1.length == b4.length)'): CHC: Assertion violation might happen here.
// Warning 6328: (528-558='assert(b1.length != b5.length)'): CHC: Assertion violation might happen here.
// Warning 6328: (577-607='assert(b1.length == b5.length)'): CHC: Assertion violation might happen here.
// Warning 4661: (322-352='assert(b1.length == b3.length)'): BMC: Assertion violation happens here.
// Warning 4661: (419-449='assert(b1.length == b4.length)'): BMC: Assertion violation happens here.
// Warning 4661: (528-558='assert(b1.length != b5.length)'): BMC: Assertion violation happens here.
// Warning 4661: (577-607='assert(b1.length == b5.length)'): BMC: Assertion violation happens here.

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

@ -22,18 +22,18 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 1218: (226-256): CHC: Error trying to invoke SMT solver.
// 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 might happen 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: (226-256): BMC: Assertion violation happens here.
// 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.
// Warning 1218: (226-256='assert(b1.length == b2.length)'): CHC: Error trying to invoke SMT solver.
// Warning 1218: (310-340='assert(b1.length == b3.length)'): CHC: Error trying to invoke SMT solver.
// Warning 1218: (483-513='assert(b1.length == b4.length)'): CHC: Error trying to invoke SMT solver.
// Warning 1218: (568-598='assert(b1.length == b5.length)'): CHC: Error trying to invoke SMT solver.
// Warning 1218: (654-684='assert(b1.length == b6.length)'): CHC: Error trying to invoke SMT solver.
// Warning 6328: (226-256='assert(b1.length == b2.length)'): CHC: Assertion violation might happen here.
// Warning 6328: (310-340='assert(b1.length == b3.length)'): CHC: Assertion violation might happen here.
// Warning 6328: (483-513='assert(b1.length == b4.length)'): CHC: Assertion violation might happen here.
// Warning 6328: (568-598='assert(b1.length == b5.length)'): CHC: Assertion violation might happen here.
// Warning 6328: (654-684='assert(b1.length == b6.length)'): CHC: Assertion violation might happen here.
// Warning 4661: (226-256='assert(b1.length == b2.length)'): BMC: Assertion violation happens here.
// Warning 4661: (310-340='assert(b1.length == b3.length)'): BMC: Assertion violation happens here.
// Warning 4661: (483-513='assert(b1.length == b4.length)'): BMC: Assertion violation happens here.
// Warning 4661: (568-598='assert(b1.length == b5.length)'): BMC: Assertion violation happens here.
// Warning 4661: (654-684='assert(b1.length == b6.length)'): BMC: Assertion violation happens here.

20
test/libsolidity/smtCheckerTests/abi/abi_encode_packed_string_literal_no_unproved.sol
View File

@ -23,14 +23,14 @@ contract C {
// SMTEngine: all
// SMTShowUnproved: no
// ----
// Warning 1218: (226-256): CHC: Error trying to invoke SMT solver.
// 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 1218: (226-256='assert(b1.length == b2.length)'): CHC: Error trying to invoke SMT solver.
// Warning 1218: (310-340='assert(b1.length == b3.length)'): CHC: Error trying to invoke SMT solver.
// Warning 1218: (483-513='assert(b1.length == b4.length)'): CHC: Error trying to invoke SMT solver.
// Warning 1218: (568-598='assert(b1.length == b5.length)'): CHC: Error trying to invoke SMT solver.
// Warning 1218: (654-684='assert(b1.length == b6.length)'): CHC: Error trying to invoke SMT solver.
// Warning 5840: CHC: 5 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: (226-256): BMC: Assertion violation happens here.
// 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.
// Warning 4661: (226-256='assert(b1.length == b2.length)'): BMC: Assertion violation happens here.
// Warning 4661: (310-340='assert(b1.length == b3.length)'): BMC: Assertion violation happens here.
// Warning 4661: (483-513='assert(b1.length == b4.length)'): BMC: Assertion violation happens here.
// Warning 4661: (568-598='assert(b1.length == b5.length)'): BMC: Assertion violation happens here.
// Warning 4661: (654-684='assert(b1.length == b6.length)'): BMC: Assertion violation happens here.

18
test/libsolidity/smtCheckerTests/abi/abi_encode_simple.sol
View File

@ -20,12 +20,12 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 1218: (298-328): CHC: Error trying to invoke SMT solver.
// Warning 1218: (389-419): CHC: Error trying to invoke SMT solver.
// Warning 1218: (492-522): CHC: Error trying to invoke SMT solver.
// Warning 6328: (298-328): CHC: Assertion violation might happen here.
// Warning 6328: (389-419): CHC: Assertion violation might happen here.
// Warning 6328: (492-522): CHC: Assertion violation might happen here.
// Warning 4661: (298-328): BMC: Assertion violation happens here.
// Warning 4661: (389-419): BMC: Assertion violation happens here.
// Warning 4661: (492-522): BMC: Assertion violation happens here.
// Warning 1218: (298-328='assert(b1.length == b3.length)'): CHC: Error trying to invoke SMT solver.
// Warning 1218: (389-419='assert(b1.length == b4.length)'): CHC: Error trying to invoke SMT solver.
// Warning 1218: (492-522='assert(b1.length != b5.length)'): CHC: Error trying to invoke SMT solver.
// Warning 6328: (298-328='assert(b1.length == b3.length)'): CHC: Assertion violation might happen here.
// Warning 6328: (389-419='assert(b1.length == b4.length)'): CHC: Assertion violation might happen here.
// Warning 6328: (492-522='assert(b1.length != b5.length)'): CHC: Assertion violation might happen here.
// Warning 4661: (298-328='assert(b1.length == b3.length)'): BMC: Assertion violation happens here.
// Warning 4661: (389-419='assert(b1.length == b4.length)'): BMC: Assertion violation happens here.
// Warning 4661: (492-522='assert(b1.length != b5.length)'): BMC: Assertion violation happens here.

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

@ -19,15 +19,15 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 1218: (208-238): CHC: Error trying to invoke SMT solver.
// Warning 1218: (286-316): CHC: Error trying to invoke SMT solver.
// Warning 1218: (453-483): CHC: Error trying to invoke SMT solver.
// Warning 1218: (532-562): CHC: Error trying to invoke SMT solver.
// Warning 6328: (208-238): CHC: Assertion violation might happen 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: (208-238): BMC: Assertion violation happens here.
// Warning 4661: (286-316): BMC: Assertion violation happens here.
// Warning 4661: (453-483): BMC: Assertion violation happens here.
// Warning 4661: (532-562): BMC: Assertion violation happens here.
// Warning 1218: (208-238='assert(b1.length == b2.length)'): CHC: Error trying to invoke SMT solver.
// Warning 1218: (286-316='assert(b1.length == b3.length)'): CHC: Error trying to invoke SMT solver.
// Warning 1218: (453-483='assert(b1.length == b4.length)'): CHC: Error trying to invoke SMT solver.
// Warning 1218: (532-562='assert(b1.length == b5.length)'): CHC: Error trying to invoke SMT solver.
// Warning 6328: (208-238='assert(b1.length == b2.length)'): CHC: Assertion violation might happen here.
// Warning 6328: (286-316='assert(b1.length == b3.length)'): CHC: Assertion violation might happen here.
// Warning 6328: (453-483='assert(b1.length == b4.length)'): CHC: Assertion violation might happen here.
// Warning 6328: (532-562='assert(b1.length == b5.length)'): CHC: Assertion violation might happen here.
// Warning 4661: (208-238='assert(b1.length == b2.length)'): BMC: Assertion violation happens here.
// Warning 4661: (286-316='assert(b1.length == b3.length)'): BMC: Assertion violation happens here.
// Warning 4661: (453-483='assert(b1.length == b4.length)'): BMC: Assertion violation happens here.
// Warning 4661: (532-562='assert(b1.length == b5.length)'): BMC: Assertion violation happens here.

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

@ -26,16 +26,16 @@ contract C {
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 1218: (578-608): CHC: Error trying to invoke SMT solver.
// 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 might happen here.
// Warning 6328: (691-721): CHC: Assertion violation might happen here.
// Warning 6328: (959-989): CHC: Assertion violation might happen here.
// Warning 6328: (1079-1109): CHC: Assertion violation might happen here.
// Warning 4661: (578-608): BMC: Assertion violation happens here.
// Warning 4661: (691-721): BMC: Assertion violation happens here.
// Warning 4661: (959-989): BMC: Assertion violation happens here.
// Warning 4661: (1079-1109): BMC: Assertion violation happens here.
// Warning 1218: (578-608='assert(b1.length == b3.length)'): CHC: Error trying to invoke SMT solver.
// Warning 1218: (691-721='assert(b1.length == b4.length)'): CHC: Error trying to invoke SMT solver.
// Warning 1218: (959-989='assert(b1.length == b5.length)'): CHC: Error trying to invoke SMT solver.
// Warning 1218: (1079-1109='assert(b4.length == b6.length)'): CHC: Error trying to invoke SMT solver.
// Warning 6328: (325-355='assert(b1.length == b2.length)'): CHC: Assertion violation happens here.
// Warning 6328: (578-608='assert(b1.length == b3.length)'): CHC: Assertion violation might happen here.
// Warning 6328: (691-721='assert(b1.length == b4.length)'): CHC: Assertion violation might happen here.
// Warning 6328: (959-989='assert(b1.length == b5.length)'): CHC: Assertion violation might happen here.
// Warning 6328: (1079-1109='assert(b4.length == b6.length)'): CHC: Assertion violation might happen here.
// Warning 4661: (578-608='assert(b1.length == b3.length)'): BMC: Assertion violation happens here.
// Warning 4661: (691-721='assert(b1.length == b4.length)'): BMC: Assertion violation happens here.
// Warning 4661: (959-989='assert(b1.length == b5.length)'): BMC: Assertion violation happens here.
// Warning 4661: (1079-1109='assert(b4.length == b6.length)'): BMC: Assertion violation happens here.

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

@ -25,16 +25,16 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 1218: (579-609): CHC: Error trying to invoke SMT solver.
// 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 might happen here.
// Warning 6328: (692-722): CHC: Assertion violation might happen here.
// Warning 6328: (960-990): CHC: Assertion violation might happen here.
// Warning 6328: (1080-1110): CHC: Assertion violation might happen here.
// Warning 4661: (579-609): BMC: Assertion violation happens here.
// Warning 4661: (692-722): BMC: Assertion violation happens here.
// Warning 4661: (960-990): BMC: Assertion violation happens here.
// Warning 4661: (1080-1110): BMC: Assertion violation happens here.
// Warning 1218: (579-609='assert(b1.length == b3.length)'): CHC: Error trying to invoke SMT solver.
// Warning 1218: (692-722='assert(b1.length == b4.length)'): CHC: Error trying to invoke SMT solver.
// Warning 1218: (960-990='assert(b1.length == b5.length)'): CHC: Error trying to invoke SMT solver.
// Warning 1218: (1080-1110='assert(b4.length == b6.length)'): CHC: Error trying to invoke SMT solver.
// Warning 6328: (326-356='assert(b1.length == b2.length)'): CHC: Assertion violation happens here.
// Warning 6328: (579-609='assert(b1.length == b3.length)'): CHC: Assertion violation might happen here.
// Warning 6328: (692-722='assert(b1.length == b4.length)'): CHC: Assertion violation might happen here.
// Warning 6328: (960-990='assert(b1.length == b5.length)'): CHC: Assertion violation might happen here.
// Warning 6328: (1080-1110='assert(b4.length == b6.length)'): CHC: Assertion violation might happen here.
// Warning 4661: (579-609='assert(b1.length == b3.length)'): BMC: Assertion violation happens here.
// Warning 4661: (692-722='assert(b1.length == b4.length)'): BMC: Assertion violation happens here.
// Warning 4661: (960-990='assert(b1.length == b5.length)'): BMC: Assertion violation happens here.
// Warning 4661: (1080-1110='assert(b4.length == b6.length)'): BMC: Assertion violation happens here.

14
test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_simple.sol
View File

@ -25,10 +25,10 @@ contract C {
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 5667: (100-115): Unused function parameter. Remove or comment out the variable name to silence this warning.
// Warning 1218: (855-885): CHC: Error trying to invoke SMT solver.
// Warning 6328: (571-601): CHC: Assertion violation happens here.
// Warning 6328: (691-721): CHC: Assertion violation happens here.
// Warning 6328: (740-770): CHC: Assertion violation happens here.
// Warning 6328: (855-885): CHC: Assertion violation might happen here.
// Warning 4661: (855-885): BMC: Assertion violation happens here.
// Warning 5667: (100-115='uint[] memory b'): Unused function parameter. Remove or comment out the variable name to silence this warning.
// Warning 1218: (855-885='assert(b1.length == b6.length)'): CHC: Error trying to invoke SMT solver.
// Warning 6328: (571-601='assert(b1.length == b4.length)'): CHC: Assertion violation happens here.
// Warning 6328: (691-721='assert(b1.length != b5.length)'): CHC: Assertion violation happens here.
// Warning 6328: (740-770='assert(b1.length == b5.length)'): CHC: Assertion violation happens here.
// Warning 6328: (855-885='assert(b1.length == b6.length)'): CHC: Assertion violation might happen here.
// Warning 4661: (855-885='assert(b1.length == b6.length)'): BMC: Assertion violation happens here.

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

@ -22,18 +22,18 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 1218: (252-282): CHC: Error trying to invoke SMT solver.
// Warning 1218: (347-377): CHC: Error trying to invoke SMT solver.
// Warning 1218: (531-561): CHC: Error trying to invoke SMT solver.
// Warning 1218: (627-657): CHC: Error trying to invoke SMT solver.
// Warning 1218: (746-776): CHC: Error trying to invoke SMT solver.
// Warning 6328: (252-282): CHC: Assertion violation might happen 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: (252-282): BMC: Assertion violation happens here.
// Warning 4661: (347-377): BMC: Assertion violation happens here.
// Warning 4661: (531-561): BMC: Assertion violation happens here.
// Warning 4661: (627-657): BMC: Assertion violation happens here.
// Warning 4661: (746-776): BMC: Assertion violation happens here.
// Warning 1218: (252-282='assert(b1.length == b2.length)'): CHC: Error trying to invoke SMT solver.
// Warning 1218: (347-377='assert(b1.length == b3.length)'): CHC: Error trying to invoke SMT solver.
// Warning 1218: (531-561='assert(b1.length == b4.length)'): CHC: Error trying to invoke SMT solver.
// Warning 1218: (627-657='assert(b1.length == b5.length)'): CHC: Error trying to invoke SMT solver.
// Warning 1218: (746-776='assert(b4.length == b6.length)'): CHC: Error trying to invoke SMT solver.
// Warning 6328: (252-282='assert(b1.length == b2.length)'): CHC: Assertion violation might happen here.
// Warning 6328: (347-377='assert(b1.length == b3.length)'): CHC: Assertion violation might happen here.
// Warning 6328: (531-561='assert(b1.length == b4.length)'): CHC: Assertion violation might happen here.
// Warning 6328: (627-657='assert(b1.length == b5.length)'): CHC: Assertion violation might happen here.
// Warning 6328: (746-776='assert(b4.length == b6.length)'): CHC: Assertion violation might happen here.
// Warning 4661: (252-282='assert(b1.length == b2.length)'): BMC: Assertion violation happens here.
// Warning 4661: (347-377='assert(b1.length == b3.length)'): BMC: Assertion violation happens here.
// Warning 4661: (531-561='assert(b1.length == b4.length)'): BMC: Assertion violation happens here.
// Warning 4661: (627-657='assert(b1.length == b5.length)'): BMC: Assertion violation happens here.
// Warning 4661: (746-776='assert(b4.length == b6.length)'): BMC: Assertion violation happens here.

4
test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_vs_sig.sol
View File

@ -9,5 +9,5 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 6328: (294-324): CHC: Assertion violation might happen here.
// Warning 7812: (294-324): BMC: Assertion violation might happen here.
// Warning 6328: (294-324='assert(b1.length == b2.length)'): CHC: Assertion violation might happen here.
// Warning 7812: (294-324='assert(b1.length == b2.length)'): BMC: Assertion violation might happen here.

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

@ -25,16 +25,16 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 1218: (588-618): CHC: Error trying to invoke SMT solver.
// 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 might happen here.
// Warning 6328: (702-732): CHC: Assertion violation might happen here.
// Warning 6328: (971-1001): CHC: Assertion violation might happen here.
// Warning 6328: (1086-1116): CHC: Assertion violation might happen here.
// Warning 4661: (588-618): BMC: Assertion violation happens here.
// Warning 4661: (702-732): BMC: Assertion violation happens here.
// Warning 4661: (971-1001): BMC: Assertion violation happens here.
// Warning 4661: (1086-1116): BMC: Assertion violation happens here.
// Warning 1218: (588-618='assert(b1.length == b3.length)'): CHC: Error trying to invoke SMT solver.
// Warning 1218: (702-732='assert(b1.length == b4.length)'): CHC: Error trying to invoke SMT solver.
// Warning 1218: (971-1001='assert(b1.length == b5.length)'): CHC: Error trying to invoke SMT solver.
// Warning 1218: (1086-1116='assert(b4.length == b6.length)'): CHC: Error trying to invoke SMT solver.
// Warning 6328: (334-364='assert(b1.length == b2.length)'): CHC: Assertion violation happens here.
// Warning 6328: (588-618='assert(b1.length == b3.length)'): CHC: Assertion violation might happen here.
// Warning 6328: (702-732='assert(b1.length == b4.length)'): CHC: Assertion violation might happen here.
// Warning 6328: (971-1001='assert(b1.length == b5.length)'): CHC: Assertion violation might happen here.
// Warning 6328: (1086-1116='assert(b4.length == b6.length)'): CHC: Assertion violation might happen here.
// Warning 4661: (588-618='assert(b1.length == b3.length)'): BMC: Assertion violation happens here.
// Warning 4661: (702-732='assert(b1.length == b4.length)'): BMC: Assertion violation happens here.
// Warning 4661: (971-1001='assert(b1.length == b5.length)'): BMC: Assertion violation happens here.
// Warning 4661: (1086-1116='assert(b4.length == b6.length)'): BMC: Assertion violation happens here.

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

@ -25,16 +25,16 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 1218: (589-619): CHC: Error trying to invoke SMT solver.
// 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 might happen here.
// Warning 6328: (703-733): CHC: Assertion violation might happen here.
// Warning 6328: (972-1002): CHC: Assertion violation might happen here.
// Warning 6328: (1087-1117): CHC: Assertion violation might happen here.
// Warning 4661: (589-619): BMC: Assertion violation happens here.
// Warning 4661: (703-733): BMC: Assertion violation happens here.
// Warning 4661: (972-1002): BMC: Assertion violation happens here.
// Warning 4661: (1087-1117): BMC: Assertion violation happens here.
// Warning 1218: (589-619='assert(b1.length == b3.length)'): CHC: Error trying to invoke SMT solver.
// Warning 1218: (703-733='assert(b1.length == b4.length)'): CHC: Error trying to invoke SMT solver.
// Warning 1218: (972-1002='assert(b1.length == b5.length)'): CHC: Error trying to invoke SMT solver.
// Warning 1218: (1087-1117='assert(b4.length == b6.length)'): CHC: Error trying to invoke SMT solver.
// Warning 6328: (335-365='assert(b1.length == b2.length)'): CHC: Assertion violation happens here.
// Warning 6328: (589-619='assert(b1.length == b3.length)'): CHC: Assertion violation might happen here.
// Warning 6328: (703-733='assert(b1.length == b4.length)'): CHC: Assertion violation might happen here.
// Warning 6328: (972-1002='assert(b1.length == b5.length)'): CHC: Assertion violation might happen here.
// Warning 6328: (1087-1117='assert(b4.length == b6.length)'): CHC: Assertion violation might happen here.
// Warning 4661: (589-619='assert(b1.length == b3.length)'): BMC: Assertion violation happens here.
// Warning 4661: (703-733='assert(b1.length == b4.length)'): BMC: Assertion violation happens here.
// Warning 4661: (972-1002='assert(b1.length == b5.length)'): BMC: Assertion violation happens here.
// Warning 4661: (1087-1117='assert(b4.length == b6.length)'): BMC: Assertion violation happens here.

14
test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_simple.sol
View File

@ -23,10 +23,10 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 5667: (107-122): Unused function parameter. Remove or comment out the variable name to silence this warning.
// Warning 1218: (824-854): CHC: Error trying to invoke SMT solver.
// Warning 6328: (543-573): CHC: Assertion violation happens here.
// Warning 6328: (664-694): CHC: Assertion violation happens here.
// Warning 6328: (713-743): CHC: Assertion violation happens here.
// Warning 6328: (824-854): CHC: Assertion violation might happen here.
// Warning 4661: (824-854): BMC: Assertion violation happens here.
// Warning 5667: (107-122='uint[] memory b'): Unused function parameter. Remove or comment out the variable name to silence this warning.
// Warning 1218: (824-854='assert(b1.length == b6.length)'): CHC: Error trying to invoke SMT solver.
// Warning 6328: (543-573='assert(b1.length == b4.length)'): CHC: Assertion violation happens here.
// Warning 6328: (664-694='assert(b1.length != b5.length)'): CHC: Assertion violation happens here.
// Warning 6328: (713-743='assert(b1.length == b5.length)'): CHC: Assertion violation happens here.
// Warning 6328: (824-854='assert(b1.length == b6.length)'): CHC: Assertion violation might happen here.
// Warning 4661: (824-854='assert(b1.length == b6.length)'): BMC: Assertion violation happens here.

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

@ -22,18 +22,18 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 1218: (261-291): CHC: Error trying to invoke SMT solver.
// Warning 1218: (357-387): CHC: Error trying to invoke SMT solver.
// Warning 1218: (542-572): CHC: Error trying to invoke SMT solver.
// Warning 1218: (639-669): CHC: Error trying to invoke SMT solver.
// Warning 1218: (753-783): CHC: Error trying to invoke SMT solver.
// Warning 6328: (261-291): CHC: Assertion violation might happen 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: (261-291): BMC: Assertion violation happens here.
// Warning 4661: (357-387): BMC: Assertion violation happens here.
// Warning 4661: (542-572): BMC: Assertion violation happens here.
// Warning 4661: (639-669): BMC: Assertion violation happens here.
// Warning 4661: (753-783): BMC: Assertion violation happens here.
// Warning 1218: (261-291='assert(b1.length == b2.length)'): CHC: Error trying to invoke SMT solver.
// Warning 1218: (357-387='assert(b1.length == b3.length)'): CHC: Error trying to invoke SMT solver.
// Warning 1218: (542-572='assert(b1.length == b4.length)'): CHC: Error trying to invoke SMT solver.
// Warning 1218: (639-669='assert(b1.length == b5.length)'): CHC: Error trying to invoke SMT solver.
// Warning 1218: (753-783='assert(b4.length == b6.length)'): CHC: Error trying to invoke SMT solver.
// Warning 6328: (261-291='assert(b1.length == b2.length)'): CHC: Assertion violation might happen here.
// Warning 6328: (357-387='assert(b1.length == b3.length)'): CHC: Assertion violation might happen here.
// Warning 6328: (542-572='assert(b1.length == b4.length)'): CHC: Assertion violation might happen here.
// Warning 6328: (639-669='assert(b1.length == b5.length)'): CHC: Assertion violation might happen here.
// Warning 6328: (753-783='assert(b4.length == b6.length)'): CHC: Assertion violation might happen here.
// Warning 4661: (261-291='assert(b1.length == b2.length)'): BMC: Assertion violation happens here.
// Warning 4661: (357-387='assert(b1.length == b3.length)'): BMC: Assertion violation happens here.
// Warning 4661: (542-572='assert(b1.length == b4.length)'): BMC: Assertion violation happens here.
// Warning 4661: (639-669='assert(b1.length == b5.length)'): BMC: Assertion violation happens here.
// Warning 4661: (753-783='assert(b4.length == b6.length)'): BMC: Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/array_members/array_pop_length_1.sol
View File

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

2
test/libsolidity/smtCheckerTests/array_members/array_pop_length_2.sol
View File

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

4
test/libsolidity/smtCheckerTests/array_members/array_pop_length_3.sol
View File

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

2
test/libsolidity/smtCheckerTests/array_members/array_pop_length_4.sol
View File

@ -8,4 +8,4 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 2529: (61-68): CHC: Empty array "pop" happens here.\nCounterexample:\na = []\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f()
// Warning 2529: (61-68='a.pop()'): CHC: Empty array "pop" happens here.\nCounterexample:\na = []\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f()

2
test/libsolidity/smtCheckerTests/array_members/array_pop_length_5.sol
View File

@ -11,4 +11,4 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 2529: (89-96): CHC: Empty array "pop" happens here.\nCounterexample:\na = []\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f()
// Warning 2529: (89-96='a.pop()'): CHC: Empty array "pop" happens here.\nCounterexample:\na = []\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f()

2
test/libsolidity/smtCheckerTests/array_members/array_pop_length_6.sol
View File

@ -11,4 +11,4 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 2529: (94-101): CHC: Empty array "pop" happens here.\nCounterexample:\na = []\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f()
// Warning 2529: (94-101='a.pop()'): CHC: Empty array "pop" happens here.\nCounterexample:\na = []\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f()

2
test/libsolidity/smtCheckerTests/array_members/array_pop_length_8.sol
View File

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

2
test/libsolidity/smtCheckerTests/array_members/length_basic.sol
View File

@ -10,4 +10,4 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 6328: (120-143): CHC: Assertion violation happens here.\nCounterexample:\narr = []\nx = 0\ny = 0\n\nTransaction trace:\nC.constructor()\nState: arr = []\nC.f()
// Warning 6328: (120-143='assert(arr.length != y)'): CHC: Assertion violation happens here.\nCounterexample:\narr = []\nx = 0\ny = 0\n\nTransaction trace:\nC.constructor()\nState: arr = []\nC.f()

6
test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment_2_fail.sol
View File

@ -24,7 +24,7 @@ contract C {
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6328: (291-317): CHC: Assertion violation happens here.
// Warning 6328: (321-347): CHC: Assertion violation happens here.
// Warning 6328: (351-374): CHC: Assertion violation happens here.
// Warning 6328: (291-317='assert(arr[2].length != x)'): CHC: Assertion violation happens here.
// Warning 6328: (321-347='assert(arr[3].length != y)'): CHC: Assertion violation happens here.
// Warning 6328: (351-374='assert(arr.length != z)'): CHC: Assertion violation happens here.
// Info 1180: Contract invariant(s) for :C:\n!(arr.length <= 2)\n!(arr.length <= 3)\n!(arr[2].length <= 3)\n

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

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

2
test/libsolidity/smtCheckerTests/array_members/pop_2d_unsafe.sol
View File

@ -10,4 +10,4 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 2529: (90-100): CHC: Empty array "pop" happens here.\nCounterexample:\na = [[0], []]\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f()
// Warning 2529: (90-100='a[1].pop()'): CHC: Empty array "pop" happens here.\nCounterexample:\na = [[0], []]\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f()

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

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

2
test/libsolidity/smtCheckerTests/array_members/pop_loop_unsafe.sol
View File

@ -11,4 +11,4 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 2529: (117-124): CHC: Empty array "pop" happens here.\nCounterexample:\na = []\nl = 0\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f(0)
// Warning 2529: (117-124='a.pop()'): CHC: Empty array "pop" happens here.\nCounterexample:\na = []\nl = 0\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f(0)

2
test/libsolidity/smtCheckerTests/array_members/push_2d_arg_1_unsafe.sol
View File

@ -11,5 +11,5 @@ contract C {
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 3944: (129-144): CHC: Underflow (resulting value less than 0) happens here.
// Warning 3944: (129-144='a[0].length - 1'): CHC: Underflow (resulting value less than 0) happens here.
// Warning 6328: (117-151): CHC: Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/array_members/push_as_lhs_and_rhs_2d_1.sol
View File

@ -16,4 +16,4 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 6328: (284-310): CHC: Assertion violation happens here.\nCounterexample:\nb = [[0], [0]]\n\nTransaction trace:\nC.constructor()\nState: b = []\nC.f()
// Warning 6328: (284-310='assert(b[0][0] != b[1][0])'): CHC: Assertion violation happens here.\nCounterexample:\nb = [[0], [0]]\n\nTransaction trace:\nC.constructor()\nState: b = []\nC.f()

2
test/libsolidity/smtCheckerTests/array_members/push_as_lhs_compound_assignment.sol
View File

@ -12,4 +12,4 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 6328: (128-145): CHC: Assertion violation happens here.\nCounterexample:\nu = [(- 1)]\n\nTransaction trace:\nC.constructor()\nState: u = []\nC.t()
// Warning 6328: (128-145='assert(u[0] >= 0)'): CHC: Assertion violation happens here.\nCounterexample:\nu = [(- 1)]\n\nTransaction trace:\nC.constructor()\nState: u = []\nC.t()

4
test/libsolidity/smtCheckerTests/array_members/push_function_return_value.sol
View File

@ -16,5 +16,5 @@ contract C {
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6328: (168-189): CHC: Assertion violation happens here.
// Warning 6328: (259-280): CHC: Assertion violation happens here.
// Warning 6328: (168-189='assert(x.length == 1)'): CHC: Assertion violation happens here.
// Warning 6328: (259-280='assert(x.length == 0)'): CHC: Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/array_members/push_push_no_args_1_fail.sol
View File

@ -9,5 +9,5 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 6328: (81-107): CHC: Assertion violation happens here.\nCounterexample:\narray2d = [[0]]\n\nTransaction trace:\nC.constructor()\nState: array2d = []\nC.l()
// Warning 6328: (81-107='assert(array2d.length > 2)'): CHC: Assertion violation happens here.\nCounterexample:\narray2d = [[0]]\n\nTransaction trace:\nC.constructor()\nState: array2d = []\nC.l()
// Warning 6328: (111-157): CHC: Assertion violation happens here.\nCounterexample:\narray2d = [[0]]\n\nTransaction trace:\nC.constructor()\nState: array2d = []\nC.l()

6
test/libsolidity/smtCheckerTests/array_members/push_storage_ref_safe_aliasing.sol
View File

@ -13,7 +13,7 @@ contract C {
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6368: (179-183): CHC: Out of bounds access happens here.
// Warning 6368: (184-188): CHC: Out of bounds access happens here.
// Warning 3944: (184-199): CHC: Underflow (resulting value less than 0) happens here.
// Warning 6368: (179-183='a[0]'): CHC: Out of bounds access happens here.
// Warning 6368: (184-188='a[0]'): CHC: Out of bounds access happens here.
// Warning 3944: (184-199='a[0].length - 1'): CHC: Underflow (resulting value less than 0) happens here.
// Warning 6328: (172-206): CHC: Assertion violation happens here.

20
test/libsolidity/smtCheckerTests/array_members/push_storage_ref_unsafe_length.sol
View File

@ -26,13 +26,13 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 6368: (238-242): CHC: Out of bounds access happens here.
// Warning 6368: (238-245): CHC: Out of bounds access might happen here.
// Warning 6368: (238-248): CHC: Out of bounds access might happen here.
// Warning 6368: (311-315): CHC: Out of bounds access happens here.
// Warning 6368: (343-347): CHC: Out of bounds access happens here.
// Warning 6328: (336-360): CHC: Assertion violation happens here.
// Warning 6368: (513-517): CHC: Out of bounds access happens here.
// Warning 6368: (513-520): CHC: Out of bounds access happens here.
// Warning 6368: (513-523): CHC: Out of bounds access happens here.
// Warning 6328: (506-530): CHC: Assertion violation happens here.
// Warning 6368: (238-242='c[0]'): CHC: Out of bounds access happens here.
// Warning 6368: (238-245='c[0][0]'): CHC: Out of bounds access might happen here.
// Warning 6368: (238-248='c[0][0][0]'): CHC: Out of bounds access might happen here.
// Warning 6368: (311-315='d[1]'): CHC: Out of bounds access happens here.
// Warning 6368: (343-347='a[0]'): CHC: Out of bounds access happens here.
// Warning 6328: (336-360='assert(a[0].length == 0)'): CHC: Assertion violation happens here.
// Warning 6368: (513-517='c[0]'): CHC: Out of bounds access happens here.
// Warning 6368: (513-520='c[0][0]'): CHC: Out of bounds access happens here.
// Warning 6368: (513-523='c[0][0][0]'): CHC: Out of bounds access happens here.
// Warning 6328: (506-530='assert(c[0][0][0] == 12)'): CHC: Assertion violation happens here.

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

@ -8,4 +8,4 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 6328: (61-91): CHC: Assertion violation happens here.\nCounterexample:\na = [0]\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f()
// Warning 6328: (61-91='assert(a[a.length - 1] == 100)'): CHC: Assertion violation happens here.\nCounterexample:\na = [0]\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f()

4
test/libsolidity/smtCheckerTests/array_members/storage_pointer_push_1.sol
View File

@ -17,5 +17,5 @@ contract C {
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6368: (159-169): CHC: Out of bounds access happens here.
// Warning 6328: (152-181): CHC: Assertion violation happens here.
// Warning 6368: (159-169='array2d[2]'): CHC: Out of bounds access happens here.
// Warning 6328: (152-181='assert(array2d[2].length > 0)'): CHC: Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_2.sol
View File

@ -16,6 +16,6 @@ contract C {
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 4984: (266-272): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 4984: (266-272='x + 10'): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 6328: (235-273): CHC: Assertion violation happens here.
// Info 1180: Contract invariant(s) for :C:\nonce\n

2
test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_ext_calls_2.sol
View File

@ -11,5 +11,5 @@ contract C {
// SMTIgnoreCex: yes
// SMTIgnoreInv: yes
// ----
// Warning 9302: (82-93): Return value of low-level calls not used.
// Warning 9302: (82-93='_a.call("")'): Return value of low-level calls not used.
// Warning 6328: (97-131): CHC: Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/blockchain_state/balance_spend.sol
View File

@ -20,4 +20,4 @@ contract C {
// ----
// Warning 6328: (280-314): CHC: Assertion violation happens here.
// Info 1180: Contract invariant(s) for :C:\n((!(c <= 1) || !((:var 1).balances[address(this)] <= 90)) && !((:var 1).balances[address(this)] <= 81) && (!(c <= 0) || !((:var 1).balances[address(this)] <= 100)))\n
// Warning 1236: (175-190): BMC: Insufficient funds happens here.
// Warning 1236: (175-190='_a.transfer(_v)'): BMC: Insufficient funds happens here.

2
test/libsolidity/smtCheckerTests/blockchain_state/balance_spend_2.sol
View File

@ -19,5 +19,5 @@ contract C {
// Warning 6328: (193-226): CHC: Assertion violation might happen here.
// Warning 6328: (245-279): CHC: Assertion violation happens here.
// Warning 6328: (298-332): CHC: Assertion violation happens here.
// Warning 1236: (141-156): BMC: Insufficient funds happens here.
// Warning 1236: (141-156='_a.transfer(_v)'): BMC: Insufficient funds happens here.
// Warning 4661: (193-226): BMC: Assertion violation happens here.

8
test/libsolidity/smtCheckerTests/blockchain_state/balance_zero_3.sol
View File

@ -12,7 +12,7 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 6328: (65-79): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor()
// Warning 6328: (150-163): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nC.constructor()
// Warning 6328: (213-227): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor()\nState: x = 1\nC.f()
// Warning 6328: (298-311): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f()
// Warning 6328: (65-79='assert(x == 0)'): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor()
// Warning 6328: (150-163='assert(x > 0)'): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nC.constructor()
// Warning 6328: (213-227='assert(x == 0)'): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor()\nState: x = 1\nC.f()
// Warning 6328: (298-311='assert(x > 0)'): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f()

8
test/libsolidity/smtCheckerTests/blockchain_state/balance_zero_4.sol
View File

@ -15,7 +15,7 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 6328: (127-141): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor()
// Warning 6328: (212-225): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nC.constructor()
// Warning 6328: (275-289): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor()\nState: x = 1\nC.f()
// Warning 6328: (360-373): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f()
// Warning 6328: (127-141='assert(x == 0)'): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor()
// Warning 6328: (212-225='assert(x > 0)'): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nC.constructor()
// Warning 6328: (275-289='assert(x == 0)'): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor()\nState: x = 1\nC.f()
// Warning 6328: (360-373='assert(x > 0)'): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f()

4
test/libsolidity/smtCheckerTests/blockchain_state/free_function_2.sol
View File

@ -19,6 +19,6 @@ contract C {
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6328: (258-274): CHC: Assertion violation happens here.
// Warning 6328: (258-274='assert(b1 == b2)'): CHC: Assertion violation happens here.
// Info 1180: Contract invariant(s) for :C:\n(x <= 0)\n
// Warning 1236: (33-46): BMC: Insufficient funds happens here.
// Warning 1236: (33-46='a.transfer(1)'): BMC: Insufficient funds happens here.

4
test/libsolidity/smtCheckerTests/blockchain_state/library_internal_2.sol
View File

@ -22,6 +22,6 @@ contract C {
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6328: (315-331): CHC: Assertion violation happens here.
// Warning 6328: (315-331='assert(b1 == b2)'): CHC: Assertion violation happens here.
// Info 1180: Contract invariant(s) for :C:\n(x <= 0)\n
// Warning 1236: (87-100): BMC: Insufficient funds happens here.
// Warning 1236: (87-100='a.transfer(1)'): BMC: Insufficient funds happens here.

6
test/libsolidity/smtCheckerTests/blockchain_state/library_public_1.sol
View File

@ -18,6 +18,6 @@ contract C {
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 4588: (219-224): Assertion checker does not yet implement this type of function call.
// Warning 6328: (263-279): CHC: Assertion violation happens here.
// Warning 6328: (359-373): CHC: Assertion violation happens here.
// Warning 4588: (219-224='a.l()'): Assertion checker does not yet implement this type of function call.
// Warning 6328: (263-279='assert(b1 == b2)'): CHC: Assertion violation happens here.
// Warning 6328: (359-373='assert(x == 0)'): CHC: Assertion violation happens here.

8
test/libsolidity/smtCheckerTests/blockchain_state/library_public_2.sol
View File

@ -20,7 +20,7 @@ contract C {
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 4588: (238-243): Assertion checker does not yet implement this type of function call.
// Warning 6328: (282-298): CHC: Assertion violation happens here.
// Warning 6328: (317-331): CHC: Assertion violation happens here.
// Warning 1236: (54-67): BMC: Insufficient funds happens here.
// Warning 4588: (238-243='a.l()'): Assertion checker does not yet implement this type of function call.
// Warning 6328: (282-298='assert(b1 == b2)'): CHC: Assertion violation happens here.
// Warning 6328: (317-331='assert(x == 0)'): CHC: Assertion violation happens here.
// Warning 1236: (54-67='a.transfer(1)'): BMC: Insufficient funds happens here.

10
test/libsolidity/smtCheckerTests/blockchain_state/library_public_3.sol
View File

@ -21,8 +21,8 @@ contract C {
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 5667: (24-41): Unused function parameter. Remove or comment out the variable name to silence this warning.
// Warning 4588: (265-270): Assertion checker does not yet implement this type of function call.
// Warning 6328: (309-325): CHC: Assertion violation happens here.
// Warning 6328: (405-419): CHC: Assertion violation happens here.
// Warning 6328: (464-486): CHC: Assertion violation happens here.
// Warning 5667: (24-41='address payable a'): Unused function parameter. Remove or comment out the variable name to silence this warning.
// Warning 4588: (265-270='a.l()'): Assertion checker does not yet implement this type of function call.
// Warning 6328: (309-325='assert(b1 == b2)'): CHC: Assertion violation happens here.
// Warning 6328: (405-419='assert(x == 0)'): CHC: Assertion violation happens here.
// Warning 6328: (464-486='assert(v == msg.value)'): CHC: Assertion violation happens here.

10
test/libsolidity/smtCheckerTests/blockchain_state/library_public_4.sol
View File

@ -21,9 +21,9 @@ contract C {
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 5667: (24-41): Unused function parameter. Remove or comment out the variable name to silence this warning.
// Warning 5667: (24-41='address payable a'): Unused function parameter. Remove or comment out the variable name to silence this warning.
// Warning 2018: (13-93): Function state mutability can be restricted to view
// Warning 4588: (272-277): Assertion checker does not yet implement this type of function call.
// Warning 6328: (316-332): CHC: Assertion violation happens here.
// Warning 6328: (412-426): CHC: Assertion violation happens here.
// Warning 6328: (471-494): CHC: Assertion violation happens here.
// Warning 4588: (272-277='a.l()'): Assertion checker does not yet implement this type of function call.
// Warning 6328: (316-332='assert(b1 == b2)'): CHC: Assertion violation happens here.
// Warning 6328: (412-426='assert(x == 0)'): CHC: Assertion violation happens here.
// Warning 6328: (471-494='assert(v == msg.sender)'): CHC: Assertion violation happens here.

8
test/libsolidity/smtCheckerTests/bmc_coverage/assert.sol
View File

@ -19,7 +19,7 @@ contract C {
// ====
// SMTEngine: bmc
// ----
// Warning 4661: (49-62): BMC: Assertion violation happens here.
// Warning 6838: (111-117): BMC: Condition is always true.
// Warning 6838: (186-192): BMC: Condition is always false.
// Warning 2512: (254-260): BMC: Condition unreachable.
// Warning 4661: (49-62='assert(x > 0)'): BMC: Assertion violation happens here.
// Warning 6838: (111-117='x >= 0'): BMC: Condition is always true.
// Warning 6838: (186-192='x != 2'): BMC: Condition is always false.
// Warning 2512: (254-260='x != 2'): BMC: Condition unreachable.

2
test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/branches_in_modifiers.sol
View File

@ -23,4 +23,4 @@ contract C {
// ====
// SMTEngine: bmc
// ----
// Warning 4661: (70-84): BMC: Assertion violation happens here.
// Warning 4661: (70-84='assert(x == 1)'): BMC: Assertion violation happens here.

6
test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/branches_in_modifiers_2.sol
View File

@ -38,6 +38,6 @@ contract C {
// ====
// SMTEngine: bmc
// ----
// Warning 4661: (351-365): BMC: Assertion violation happens here.
// Warning 4661: (602-619): BMC: Assertion violation happens here.
// Warning 4661: (748-762): BMC: Assertion violation happens here.
// Warning 4661: (351-365='assert(x == 1)'): BMC: Assertion violation happens here.
// Warning 4661: (602-619='assert(oldx == x)'): BMC: Assertion violation happens here.
// Warning 4661: (748-762='assert(x == 0)'): BMC: Assertion violation happens here.

8
test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/constructor_state_variable_init.sol
View File

@ -35,7 +35,7 @@ contract C is B {
// ====
// SMTEngine: bmc
// ----
// Warning 4661: (297-311): BMC: Assertion violation happens here.
// Warning 4661: (389-412): BMC: Assertion violation happens here.
// Warning 4661: (489-513): BMC: Assertion violation happens here.
// Warning 4661: (533-546): BMC: Assertion violation happens here.
// Warning 4661: (297-311='assert(y == 4)'): BMC: Assertion violation happens here.
// Warning 4661: (389-412='assert(x < 0 && y == 4)'): BMC: Assertion violation happens here.
// Warning 4661: (489-513='assert(x >= 0 && y == 2)'): BMC: Assertion violation happens here.
// Warning 4661: (533-546='assert(x > 0)'): BMC: Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/constructor_state_variable_init_chain_alternate.sol
View File

@ -25,4 +25,4 @@ contract D is C {
// ====
// SMTEngine: bmc
// ----
// Warning 4661: (286-300): BMC: Assertion violation happens here.
// Warning 4661: (286-300='assert(x == 1)'): BMC: Assertion violation happens here.

16
test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/constructor_state_variable_init_diamond.sol
View File

@ -60,11 +60,11 @@ contract D4 is B, C {
// ====
// SMTEngine: bmc
// ----
// Warning 4661: (337-351): BMC: Assertion violation happens here.
// Warning 4661: (370-385): BMC: Assertion violation happens here.
// Warning 4661: (460-474): BMC: Assertion violation happens here.
// Warning 4661: (493-507): BMC: Assertion violation happens here.
// Warning 4661: (670-684): BMC: Assertion violation happens here.
// Warning 4661: (736-751): BMC: Assertion violation happens here.
// Warning 4661: (827-841): BMC: Assertion violation happens here.
// Warning 4661: (860-874): BMC: Assertion violation happens here.
// Warning 4661: (337-351='assert(x == 1)'): BMC: Assertion violation happens here.
// Warning 4661: (370-385='assert(x == -1)'): BMC: Assertion violation happens here.
// Warning 4661: (460-474='assert(x == 0)'): BMC: Assertion violation happens here.
// Warning 4661: (493-507='assert(x == 1)'): BMC: Assertion violation happens here.
// Warning 4661: (670-684='assert(x == 0)'): BMC: Assertion violation happens here.
// Warning 4661: (736-751='assert(x == -1)'): BMC: Assertion violation happens here.
// Warning 4661: (827-841='assert(x == 0)'): BMC: Assertion violation happens here.
// Warning 4661: (860-874='assert(x == 1)'): BMC: Assertion violation happens here.

8
test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/constructors.sol
View File

@ -25,7 +25,7 @@ contract C is B {
// ====
// SMTEngine: bmc
// ----
// Warning 5740: (119-124): Unreachable code.
// Warning 4661: (277-291): BMC: Assertion violation happens here.
// Warning 4661: (310-324): BMC: Assertion violation happens here.
// Warning 4661: (343-357): BMC: Assertion violation happens here.
// Warning 5740: (119-124='x = 3'): Unreachable code.
// Warning 4661: (277-291='assert(x == 3)'): BMC: Assertion violation happens here.
// Warning 4661: (310-324='assert(x == 2)'): BMC: Assertion violation happens here.
// Warning 4661: (343-357='assert(x == 1)'): BMC: Assertion violation happens here.

4
test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/nested_if.sol
View File

@ -22,5 +22,5 @@ contract C {
// ====
// SMTEngine: bmc
// ----
// Warning 4661: (114-141): BMC: Assertion violation happens here.
// Warning 6838: (299-315): BMC: Condition is always false.
// Warning 4661: (114-141='assert(nested_if(a,b) == 1)'): BMC: Assertion violation happens here.
// Warning 6838: (299-315='a == 2 && b == 2'): BMC: Condition is always false.

2
test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/return_in_both_branches.sol
View File

@ -18,4 +18,4 @@ contract C {
// ====
// SMTEngine: bmc
// ----
// Warning 5740: (232-240): Unreachable code.
// Warning 5740: (232-240='return 1'): Unreachable code.

2
test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/simple_if2.sol
View File

@ -14,4 +14,4 @@ contract C {
// ====
// SMTEngine: bmc
// ----
// Warning 4661: (56-81): BMC: Assertion violation happens here.
// Warning 4661: (56-81='assert(simple_if(a) == 1)'): BMC: Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/simple_if_array.sol
View File

@ -25,4 +25,4 @@ contract C {
// ====
// SMTEngine: bmc
// ----
// Warning 4661: (172-189): BMC: Assertion violation happens here.
// Warning 4661: (172-189='assert(a[1] == 1)'): BMC: Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/simple_if_state_var.sol
View File

@ -19,4 +19,4 @@ contract C {
// ====
// SMTEngine: bmc
// ----
// Warning 4661: (99-113): BMC: Assertion violation happens here.
// Warning 4661: (99-113='assert(x == 1)'): BMC: Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/simple_if_struct.sol
View File

@ -22,4 +22,4 @@ contract C {
// ====
// SMTEngine: bmc
// ----
// Warning 4661: (123-139): BMC: Assertion violation happens here.
// Warning 4661: (123-139='assert(s.x == 1)'): BMC: Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/simple_if_struct_2.sol
View File

@ -22,4 +22,4 @@ contract C {
// ====
// SMTEngine: bmc
// ----
// Warning 4661: (123-139): BMC: Assertion violation happens here.
// Warning 4661: (123-139='assert(s.x == 1)'): BMC: Assertion violation happens here.

4
test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/simple_if_tuple.sol
View File

@ -23,5 +23,5 @@ contract C {
// ====
// SMTEngine: bmc
// ----
// Warning 4661: (127-141): BMC: Assertion violation happens here.
// Warning 4661: (161-175): BMC: Assertion violation happens here.
// Warning 4661: (127-141='assert(x == 0)'): BMC: Assertion violation happens here.
// Warning 4661: (161-175='assert(x == 1)'): BMC: Assertion violation happens here.

4
test/libsolidity/smtCheckerTests/bmc_coverage/call_balance.sol
View File

@ -9,5 +9,5 @@ contract C {
// ====
// SMTEngine: bmc
// ----
// Warning 9302: (83-94): Return value of low-level calls not used.
// Warning 4661: (133-149): BMC: Assertion violation happens here.
// Warning 9302: (83-94='_a.call("")'): Return value of low-level calls not used.
// Warning 4661: (133-149='assert(b1 == b2)'): BMC: Assertion violation happens here.

4
test/libsolidity/smtCheckerTests/bmc_coverage/call_state_var.sol
View File

@ -9,5 +9,5 @@ contract C {
// ====
// SMTEngine: bmc
// ----
// Warning 9302: (66-77): Return value of low-level calls not used.
// Warning 4661: (81-95): BMC: Assertion violation happens here.
// Warning 9302: (66-77='_a.call("")'): Return value of low-level calls not used.
// Warning 4661: (81-95='assert(x == 2)'): BMC: Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/bmc_coverage/funds.sol
View File

@ -6,4 +6,4 @@ contract C {
// ====
// SMTEngine: bmc
// ----
// Warning 1236: (55-70): BMC: Insufficient funds happens here.
// Warning 1236: (55-70='a.transfer(200)'): BMC: Insufficient funds happens here.

2
test/libsolidity/smtCheckerTests/bmc_coverage/implicit_constructor_with_function_calls.sol
View File

@ -14,4 +14,4 @@ contract C {
// ====
// SMTEngine: bmc
// ----
// Warning 4661: (172-187): BMC: Assertion violation happens here.
// Warning 4661: (172-187='assert(x == 42)'): BMC: Assertion violation happens here.

8
test/libsolidity/smtCheckerTests/bmc_coverage/math.sol
View File

@ -15,7 +15,7 @@ contract C {
// ====
// SMTEngine: bmc
// ----
// Warning 2661: (79-84): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 4144: (155-160): BMC: Underflow (resulting value less than 0) happens here.
// Warning 2661: (231-236): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 3046: (307-312): BMC: Division by zero happens here.
// Warning 2661: (79-84='x + y'): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 4144: (155-160='x - y'): BMC: Underflow (resulting value less than 0) happens here.
// Warning 2661: (231-236='x * y'): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 3046: (307-312='x / y'): BMC: Division by zero happens here.

2
test/libsolidity/smtCheckerTests/bmc_coverage/math_constructor.sol
View File

@ -5,4 +5,4 @@ contract C {
// ====
// SMTEngine: bmc
// ----
// Warning 4144: (36-41): BMC: Underflow (resulting value less than 0) happens here.
// Warning 4144: (36-41='z - 3'): BMC: Underflow (resulting value less than 0) happens here.

2
test/libsolidity/smtCheckerTests/bmc_coverage/msg_value_4.sol
View File

@ -13,4 +13,4 @@ contract B {
// ====
// SMTEngine: bmc
// ----
// Warning 4661: (154-176): BMC: Assertion violation happens here.
// Warning 4661: (154-176='assert(msg.value == 0)'): BMC: Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/bmc_coverage/staticcall_balance.sol
View File

@ -9,4 +9,4 @@ contract C {
// ====
// SMTEngine: bmc
// ----
// Warning 9302: (88-105): Return value of low-level calls not used.
// Warning 9302: (88-105='_a.staticcall("")'): Return value of low-level calls not used.

2
test/libsolidity/smtCheckerTests/bmc_coverage/staticcall_state_var.sol
View File

@ -9,4 +9,4 @@ contract C {
// ====
// SMTEngine: bmc
// ----
// Warning 9302: (66-83): Return value of low-level calls not used.
// Warning 9302: (66-83='_a.staticcall("")'): Return value of low-level calls not used.

2
test/libsolidity/smtCheckerTests/bmc_coverage/try_multiple_catch_clauses_2.sol
View File

@ -20,4 +20,4 @@ contract C {
// ====
// SMTEngine: bmc
// ----
// Warning 4661: (306-320): BMC: Assertion violation happens here.
// Warning 4661: (306-320='assert(x == 0)'): BMC: Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/bmc_coverage/try_multiple_returned_values_with_tuple.sol
View File

@ -24,4 +24,4 @@ contract C {
// ====
// SMTEngine: bmc
// ----
// Warning 4661: (336-351): BMC: Assertion violation happens here.
// Warning 4661: (336-351='assert(success)'): BMC: Assertion violation happens here.

4
test/libsolidity/smtCheckerTests/bmc_coverage/unary_add_minus_overflow_detected.sol
View File

@ -23,5 +23,5 @@ contract C {
// ====
// SMTEngine: bmc
// ----
// Warning 2661: (55-58): BMC: Overflow (resulting value larger than 255) happens here.
// Warning 4144: (95-98): BMC: Underflow (resulting value less than 0) happens here.
// Warning 2661: (55-58='++x'): BMC: Overflow (resulting value larger than 255) happens here.
// Warning 4144: (95-98='--x'): BMC: Underflow (resulting value less than 0) happens here.

2
test/libsolidity/smtCheckerTests/bmc_coverage/unchecked_function_call_with_unchecked_block.sol
View File

@ -12,4 +12,4 @@ contract C {
// ====
// SMTEngine: bmc
// ----
// Warning 4661: (85-98): BMC: Assertion violation happens here.
// Warning 4661: (85-98='assert(y < x)'): BMC: Assertion violation happens here.

4
test/libsolidity/smtCheckerTests/complex/slither/const_state_variables.sol
View File

@ -52,6 +52,6 @@ contract MyConc{
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 2519: (740-759): This declaration shadows an existing declaration.
// Warning 2519: (740-759='uint constant A = 1'): This declaration shadows an existing declaration.
// Warning 2018: (976-1053): Function state mutability can be restricted to view
// Warning 4984: (952-969): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 4984: (952-969='10 + block.number'): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.

10
test/libsolidity/smtCheckerTests/complex/slither/external_function.sol
View File

@ -74,9 +74,9 @@ contract InternalCall {
// SMTEngine: all
// ----
// Warning 9302: (727-782): Return value of low-level calls not used.
// Warning 2072: (84-93): Unused local variable.
// Warning 2072: (227-236): Unused local variable.
// Warning 2072: (634-643): Unused local variable.
// Warning 2072: (84-93='uint256 i'): Unused local variable.
// Warning 2072: (227-236='uint256 i'): Unused local variable.
// Warning 2072: (634-643='uint256 i'): Unused local variable.
// Warning 2018: (42-104): Function state mutability can be restricted to pure
// Warning 2018: (185-247): Function state mutability can be restricted to pure
// Warning 2018: (437-506): Function state mutability can be restricted to pure
@ -84,5 +84,5 @@ contract InternalCall {
// Warning 2018: (1179-1241): Function state mutability can be restricted to pure
// Warning 2018: (1247-1309): Function state mutability can be restricted to pure
// Warning 4588: (681-716): Assertion checker does not yet implement this type of function call.
// Warning 4588: (854-886): Assertion checker does not yet implement this type of function call.
// Warning 5729: (1370-1375): BMC does not yet implement this type of function call.
// Warning 4588: (854-886='new ContractWithFunctionCalled()'): Assertion checker does not yet implement this type of function call.
// Warning 5729: (1370-1375='ptr()'): BMC does not yet implement this type of function call.

2
test/libsolidity/smtCheckerTests/control_flow/branches_inside_modifiers_1.sol
View File

@ -22,5 +22,5 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 6328: (327-341): CHC: Assertion violation happens here.\nCounterexample:\nx = 7\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.g()\n C.f() -- internal call
// Warning 6328: (327-341='assert(x == 6)'): CHC: Assertion violation happens here.\nCounterexample:\nx = 7\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.g()\n C.f() -- internal call
// Info 1180: Contract invariant(s) for :C:\n((x = 0) || (x = 7))\n

2
test/libsolidity/smtCheckerTests/control_flow/branches_inside_modifiers_2.sol
View File

@ -22,5 +22,5 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 6328: (333-347): CHC: Assertion violation happens here.\nCounterexample:\nx = 3\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.g()\n C.f() -- internal call
// Warning 6328: (333-347='assert(x == 6)'): CHC: Assertion violation happens here.\nCounterexample:\nx = 3\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.g()\n C.f() -- internal call
// Info 1180: Contract invariant(s) for :C:\n((x = 0) || (x = 3))\n

2
test/libsolidity/smtCheckerTests/control_flow/branches_inside_modifiers_3.sol
View File

@ -22,5 +22,5 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 6328: (326-340): CHC: Assertion violation happens here.\nCounterexample:\nx = 3\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.g()\n C.f() -- internal call
// Warning 6328: (326-340='assert(x == 6)'): CHC: Assertion violation happens here.\nCounterexample:\nx = 3\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.g()\n C.f() -- internal call
// Info 1180: Contract invariant(s) for :C:\n((x = 0) || (x = 3))\n

Some files were not shown because too many files have changed in this diff Show More