cerc-io/solidity
11
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] added missing type constraints for Address

Browse Source
This commit is contained in:
Martin Blicha
2021-01-27 20:39:24 +01:00
parent 49dbcba3a0
commit deb90d84a6
35 changed files with 846 additions and 823 deletions
Download Patch File Download Diff File Expand all files Collapse all files
test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_vs_sig.sol
+1 -2
View File
@@ -8,5 +8,4 @@ contract C {
}
}
// ----
// Warning 6328: (326-356): CHC: Assertion violation might happen here.
// Warning 7812: (326-356): BMC: Assertion violation might happen here.
// Warning 6328: (326-356): CHC: Assertion violation happens here.
test/libsolidity/smtCheckerTests/array_members/push_as_lhs_3d.sol
+3 -1
View File
@@ -25,5 +25,7 @@ contract C {
assert(c[length1 - 1][length2 - 1][length3 - 1] == 200);
}
}
// ====
// SMTIgnoreCex: yes
// ----
// Warning 6328: (570-625): CHC: Assertion violation happens here.\nCounterexample:\nc = [[[2]]]\n\nTransaction trace:\nC.constructor()\nState: c = []\nC.g()
// Warning 6328: (570-625): CHC: Assertion violation happens here.
test/libsolidity/smtCheckerTests/blockchain_state/transfer.sol
+1 -1
View File
@@ -10,4 +10,4 @@ contract C {
}
}
// ----
// Warning 6328: (199-234): CHC: Assertion violation happens here.\nCounterexample:\n\na = 2437\n\nTransaction trace:\nC.constructor()\nC.f(2437)
// Warning 6328: (199-234): CHC: Assertion violation happens here.\nCounterexample:\n\na = 21238\n\nTransaction trace:\nC.constructor()\nC.f(21238)
test/libsolidity/smtCheckerTests/crypto/crypto_functions_fail.sol
+1 -1
View File
@@ -29,7 +29,7 @@ contract C {
// Warning 6328: (305-321): CHC: Assertion violation might happen here.
// Warning 1218: (448-464): CHC: Error trying to invoke SMT solver.
// Warning 6328: (448-464): CHC: Assertion violation might happen here.
// Warning 6328: (673-689): CHC: Assertion violation happens here.\nCounterexample:\n\nh0 = 21238\nv0 = 173\nr0 = 30612\ns0 = 32285\nh1 = 7719\nv1 = 21\nr1 = 10450\ns1 = 8855\n\nTransaction trace:\nC.constructor()\nC.e(21238, 173, 30612, 32285, 7719, 21, 10450, 8855)
// Warning 6328: (673-689): CHC: Assertion violation happens here.\nCounterexample:\n\nh0 = 7719\nv0 = 21\nr0 = 10450\ns0 = 8365\nh1 = 38\nv1 = 151\nr1 = 32285\ns1 = 2437\n\nTransaction trace:\nC.constructor()\nC.e(7719, 21, 10450, 8365, 38, 151, 32285, 2437)
// Warning 4661: (168-184): BMC: Assertion violation happens here.
// Warning 4661: (305-321): BMC: Assertion violation happens here.
// Warning 4661: (448-464): BMC: Assertion violation happens here.
test/libsolidity/smtCheckerTests/crypto/crypto_functions_not_same.sol
+1 -1
View File
@@ -11,4 +11,4 @@ contract C {
}
}
// ----
// Warning 6328: (229-243): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f(data)\n C.fi(data, 2437) -- internal call
// Warning 6328: (229-243): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f(data)\n C.fi(data, 7719) -- internal call
test/libsolidity/smtCheckerTests/crypto/crypto_functions_same_input_over_state_same_output_fail.sol
+3 -1
View File
@@ -51,7 +51,9 @@ contract C {
// Warning 6328: (749-768): CHC: Assertion violation might happen here.
// Warning 1218: (772-791): CHC: Error trying to invoke SMT solver.
// Warning 6328: (772-791): CHC: Assertion violation might happen here.
// Warning 6328: (795-814): CHC: Assertion violation happens here.
// Warning 1218: (795-814): CHC: Error trying to invoke SMT solver.
// Warning 6328: (795-814): CHC: Assertion violation might happen here.
// Warning 4661: (726-745): BMC: Assertion violation happens here.
// Warning 4661: (749-768): BMC: Assertion violation happens here.
// Warning 4661: (772-791): BMC: Assertion violation happens here.
// Warning 4661: (795-814): BMC: Assertion violation happens here.
test/libsolidity/smtCheckerTests/loops/for_1_fail.sol
+2
View File
@@ -14,4 +14,6 @@ contract C
// ====
// SMTSolvers: z3
// ----
// Warning 4984: (176-181): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 6328: (189-203): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 14\n\nTransaction trace:\nC.constructor()\nC.f(4)
// Warning 2661: (176-181): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
test/libsolidity/smtCheckerTests/loops/while_2_break_fail.sol
+1 -1
View File
@@ -15,4 +15,4 @@ contract C
// SMTSolvers: z3
// ----
// Warning 5740: (120-123): Unreachable code.
// Warning 6328: (131-145): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 3\n\nTransaction trace:\nC.constructor()\nC.f(3)
// Warning 6328: (131-145): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 1\n\nTransaction trace:\nC.constructor()\nC.f(1)
test/libsolidity/smtCheckerTests/overflow/overflow_mul_cex_with_array.sol
+1 -1
View File
@@ -7,4 +7,4 @@ contract C {
}
}
// ----
// Warning 4984: (118-121): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\n\nx = [14, 14, 14, 14, 14, 14, 14, 14, 14, 11, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14]\ny = 23158417847463239084714197001737581570653996933128112807891516801582625927988\n\nTransaction trace:\nC.constructor()\nC.f([14, 14, 14, 14, 14, 14, 14, 14, 14, 11, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14], 23158417847463239084714197001737581570653996933128112807891516801582625927988)
// Warning 4984: (118-121): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\n\ny = 23158417847463239084714197001737581570653996933128112807891516801582625927988\n\nTransaction trace:\nC.constructor()\nC.f(x, 23158417847463239084714197001737581570653996933128112807891516801582625927988)
test/libsolidity/smtCheckerTests/special/abi_decode_simple.sol
+1 -1
View File
@@ -14,6 +14,6 @@ contract C {
// Warning 2072: (184-188): Unused local variable.
// Warning 8364: (155-156): Assertion checker does not yet implement type type(contract C)
// Warning 8364: (225-226): Assertion checker does not yet implement type type(contract C)
// Warning 6328: (252-268): CHC: Assertion violation happens here.\nCounterexample:\n\ndata = [16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 13, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16]\n\nTransaction trace:\nC.constructor()\nC.f([16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 13, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16])
// Warning 6328: (252-268): CHC: Assertion violation happens here.\nCounterexample:\n\ndata = [10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 13, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10]\n\nTransaction trace:\nC.constructor()\nC.f([10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 13, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10])
// Warning 8364: (155-156): Assertion checker does not yet implement type type(contract C)
// Warning 8364: (225-226): Assertion checker does not yet implement type type(contract C)
test/libsolidity/smtCheckerTests/special/blockhash.sol
+2 -2
View File
@@ -10,5 +10,5 @@ contract C
}
}
// ----
// Warning 6328: (85-109): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 7719\n\nTransaction trace:\nC.constructor()\nC.f(7719){ value: 21238 }
// Warning 6328: (113-137): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 7719\n\nTransaction trace:\nC.constructor()\nC.f(7719){ value: 2437 }
// Warning 6328: (85-109): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 38\n\nTransaction trace:\nC.constructor()\nC.f(38){ value: 7719 }
// Warning 6328: (113-137): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 38\n\nTransaction trace:\nC.constructor()\nC.f(38){ value: 21238 }
test/libsolidity/smtCheckerTests/special/msg_data.sol
+2 -2
View File
@@ -22,5 +22,5 @@ contract C
}
}
// ----
// Warning 6328: (153-180): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f(){ value: 8365 }
// Warning 6328: (500-527): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g(){ value: 8365 }
// Warning 6328: (153-180): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f(){ value: 10450 }
// Warning 6328: (500-527): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g(){ value: 10450 }
test/libsolidity/smtCheckerTests/special/msg_sender_fail_1.sol
+1 -1
View File
@@ -10,4 +10,4 @@ contract C
}
}
// ----
// Warning 6328: (155-178): CHC: Assertion violation happens here.\nCounterexample:\n\nc = 38\n\nTransaction trace:\nC.constructor()\nC.f(38)
// Warning 6328: (155-178): CHC: Assertion violation happens here.\nCounterexample:\n\nc = 39\n\nTransaction trace:\nC.constructor()\nC.f(39)
test/libsolidity/smtCheckerTests/special/msg_sender_range.sol
+9
View File
@@ -0,0 +1,9 @@
pragma experimental SMTChecker;
contract C {
function f() public view {
assert(msg.sender >= address(0)); // should hold
assert(msg.sender <= address(2**160-1)); // should hold
}
}
test/libsolidity/smtCheckerTests/try_catch/try_string_literal_to_fixed_bytes.sol
+1 -1
View File
@@ -14,4 +14,4 @@ contract C {
}
}
// ----
// Warning 6328: (250-294): CHC: Assertion violation happens here.
// Warning 6328: (250-294): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f()\n C.g() -- trusted external call
test/libsolidity/smtCheckerTests/types/array_branch_1d.sol
+1 -1
View File
@@ -11,4 +11,4 @@ contract C
}
}
// ----
// Warning 6328: (176-192): CHC: Assertion violation happens here.\nCounterexample:\n\nb = false\nc = [0, 11]\n\nTransaction trace:\nC.constructor()\nC.f(false, [38, 11])
// Warning 6328: (176-192): CHC: Assertion violation happens here.\nCounterexample:\n\nb = false\nc = [0, 8]\n\nTransaction trace:\nC.constructor()\nC.f(false, [38, 8])
test/libsolidity/smtCheckerTests/types/enum_range.sol
+9
View File
@@ -0,0 +1,9 @@
pragma experimental SMTChecker;
contract C
{
enum D { Left, Right }
function f(D a) public pure {
assert(a == D.Left || a == D.Right);
}
}
test/libsolidity/smtCheckerTests/types/fixed_bytes_access_2.sol
+1 -1
View File
@@ -6,4 +6,4 @@ contract C {
}
}
// ----
// Warning 4281: (117-120): CHC: Division by zero happens here.\nCounterexample:\n\nx = [14, 14, 14, 14, 14, 14, 14, 14, 14, 11, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14]\ny = 0\n\nTransaction trace:\nC.constructor()\nC.f([14, 14, 14, 14, 14, 14, 14, 14, 14, 11, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14], 0)
// Warning 4281: (117-120): CHC: Division by zero happens here.\nCounterexample:\n\ny = 0\n\nTransaction trace:\nC.constructor()\nC.f(x, 0)
test/libsolidity/smtCheckerTests/types/fixed_bytes_range.sol
+10
View File
@@ -0,0 +1,10 @@
pragma experimental SMTChecker;
contract C {
function f(bytes1 b) public pure {
bytes1 c = hex"7f";
require(b > c);
assert(uint8(b) > 127); // should hold
}
}
test/libsolidity/smtCheckerTests/types/mapping_as_parameter_1.sol
+1 -1
View File
@@ -12,4 +12,4 @@ contract c {
}
}
// ----
// Warning 6328: (289-306): CHC: Assertion violation happens here.\nCounterexample:\n\na = 38\nb = 21238\n\nTransaction trace:\nc.constructor()\nc.g(38, 21238)\n c.f(map, 38, 21238) -- internal call
// Warning 6328: (289-306): CHC: Assertion violation happens here.\nCounterexample:\n\na = 38\nb = 21239\n\nTransaction trace:\nc.constructor()\nc.g(38, 21239)\n c.f(map, 38, 21239) -- internal call
test/libsolidity/smtCheckerTests/types/string_literal_comparison_2.sol
+1 -1
View File
@@ -10,5 +10,5 @@ contract C {
}
}
// ----
// Warning 6328: (147-166): CHC: Assertion violation happens here.\nCounterexample:\n\n_x = 52647538817385212172903286807934654968315727694643370704309751478220717293569\n\nTransaction trace:\nC.constructor()\nC.f(52647538817385212172903286807934654968315727694643370704309751478220717293569)
// Warning 6328: (147-166): CHC: Assertion violation happens here.\nCounterexample:\n\n_x = 0\n\nTransaction trace:\nC.constructor()\nC.f(0)
// Warning 6328: (170-190): CHC: Assertion violation happens here.\nCounterexample:\n\n_x = 52647538830022687173130149211684818290356179572910782152375644828738034597888\n\nTransaction trace:\nC.constructor()\nC.f(52647538830022687173130149211684818290356179572910782152375644828738034597888)