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

adjust nondet

Browse Source
This commit is contained in:
Leo Alt 2022-05-12 16:37:59 +02:00
parent 0d0add2afc
commit d85494a77d
16 changed files with 32 additions and 14 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -20,5 +20,6 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6328: (362-420): CHC: Assertion violation happens here.

1
test/libsolidity/smtCheckerTests/deployment/deploy_trusted_flow.sol
View File

@ -18,6 +18,7 @@ contract C {
// ====
// SMTEngine: all
// SMTExtCalls: trusted
// SMTIgnoreOS: macos
// ----
// Warning 4984: (47-50): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 6328: (167-185): CHC: Assertion violation might happen here.

1
test/libsolidity/smtCheckerTests/deployment/deploy_trusted_state_flow.sol
View File

@ -17,6 +17,7 @@ contract C {
// ====
// SMTEngine: all
// SMTExtCalls: trusted
// SMTIgnoreOS: macos
// ----
// Warning 1218: (233-251): CHC: Error trying to invoke SMT solver.
// Warning 4984: (47-50): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.

7
test/libsolidity/smtCheckerTests/external_calls/call_abstract_constructor_trusted_1.sol
View File

@ -21,7 +21,8 @@ contract C {
// ====
// SMTEngine: chc
// SMTExtCalls: trusted
// SMTIgnoreCex: yes
// ----
// Warning 6328: (231-253): CHC: Assertion violation happens here.\nCounterexample:\n\nd = 0x0119\ny = 0\n\nTransaction trace:\nC.constructor()
// Warning 6328: (293-307): CHC: Assertion violation happens here.\nCounterexample:\n\nd = 0x0217\ny = 3\n\nTransaction trace:\nC.constructor()
// Warning 6328: (359-374): CHC: Assertion violation happens here.\nCounterexample:\n\nd = 0x188b\ny = 0\n\nTransaction trace:\nC.constructor()
// Warning 6328: (231-253): CHC: Assertion violation happens here.
// Warning 6328: (293-307): CHC: Assertion violation happens here.
// Warning 6328: (359-374): CHC: Assertion violation happens here.

7
test/libsolidity/smtCheckerTests/external_calls/call_abstract_constructor_trusted_2.sol
View File

@ -17,8 +17,9 @@ contract C {
// ====
// SMTEngine: chc
// SMTExtCalls: trusted
// SMTIgnoreCex: yes
// ----
// Warning 9302: (257-293): Return value of low-level calls not used.
// Warning 6328: (216-238): CHC: Assertion violation happens here.\nCounterexample:\n\nd = 0x0119\n\nTransaction trace:\nC.constructor()
// Warning 6328: (297-319): CHC: Assertion violation happens here.\nCounterexample:\n\nd = 0x1720\n\nTransaction trace:\nC.constructor()
// Warning 6328: (404-426): CHC: Assertion violation happens here.\nCounterexample:\n\nd = 0x1720\n\nTransaction trace:\nC.constructor()
// Warning 6328: (216-238): CHC: Assertion violation happens here.
// Warning 6328: (297-319): CHC: Assertion violation happens here.
// Warning 6328: (404-426): CHC: Assertion violation happens here.

1
test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_1.sol
View File

@ -35,6 +35,7 @@ contract C {
// ====
// SMTEngine: chc
// SMTExtCalls: trusted
// SMTIgnoreOS: macos
// ----
// Warning 6328: (256-277): CHC: Assertion violation happens here.
// Warning 6328: (533-554): CHC: Assertion violation might happen here.

1
test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_3.sol
View File

@ -40,5 +40,6 @@ contract C {
// ====
// SMTEngine: chc
// SMTExtCalls: trusted
// SMTIgnoreOS: macos
// ----
// Warning 6328: (561-582): CHC: Assertion violation might happen here.

1
test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_4.sol
View File

@ -43,5 +43,6 @@ contract C {
// ====
// SMTEngine: chc
// SMTExtCalls: trusted
// SMTIgnoreOS: macos
// ----
// Warning 6328: (641-662): CHC: Assertion violation might happen here.

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

@ -12,5 +12,6 @@ contract C {
// SMTEngine: chc
// SMTExtCalls: trusted
// SMTTargets: assert
// SMTIgnoreCex: yes
// ----
// Warning 6328: (147-161): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f()\n C.i() -- trusted external call
// Warning 6328: (147-161): CHC: Assertion violation happens here.

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

@ -16,5 +16,6 @@ contract C {
// SMTEngine: chc
// SMTExtCalls: trusted
// SMTTargets: assert
// SMTIgnoreCex: yes
// ----
// Warning 6328: (165-187): CHC: Assertion violation happens here.\nCounterexample:\nds = [37]\n\nTransaction trace:\nC.constructor()\nState: ds = [37]\nC.f()
// Warning 6328: (165-187): CHC: Assertion violation happens here.

1
test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_unsafe_trusted.sol
View File

@ -38,6 +38,7 @@ contract C {
// SMTContract: C
// SMTEngine: chc
// SMTExtCalls: trusted
// SMTIgnoreOS: macos
// ----
// Warning 6328: (396-410): CHC: Assertion violation might happen here.
// Warning 6328: (429-455): CHC: Assertion violation happens here.

1
test/libsolidity/smtCheckerTests/imports/import_as_module_2.sol
View File

@ -17,6 +17,7 @@ function f(uint _x) pure {
}
// ====
// SMTEngine: all
// SMTIgnoreOS: macos
// ----
// Warning 6328: (A:50-64): CHC: Assertion violation happens here.\nCounterexample:\n\n_y = 0\n\nTransaction trace:\nD.constructor()\nD.g(0)\n s1.sol:f(200) -- internal call\n s1.sol:f(0) -- internal call\n A:f(10) -- internal call\n A:f(0) -- internal call
// Warning 6328: (s1.sol:28-44): CHC: Assertion violation happens here.\nCounterexample:\n\n_y = 0\n\nTransaction trace:\nD.constructor()\nD.g(0)\n s1.sol:f(200) -- internal call\n s1.sol:f(0) -- internal call

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

@ -11,5 +11,6 @@ contract C
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6328: (164-183): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\np = 0\n\nTransaction trace:\nC.constructor()\nC.f(0, 0)
// Warning 6328: (164-183): CHC: Assertion violation happens here.

1
test/libsolidity/smtCheckerTests/operators/index_access_for_bytesNN.sol
View File

@ -6,5 +6,6 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreOS: macos
// ----
// Warning 6368: (76-90): CHC: Out of bounds access might happen here.

11
test/libsolidity/smtCheckerTests/typecast/bytes_to_fixed_bytes_1.sol
View File

@ -15,8 +15,11 @@ contract C {
assert(g == 0x0001020304050607080900010203040506070809000102030405060708090002); // should fail
}
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6328: (225-256): CHC: Assertion violation happens here.\nCounterexample:\n\nc = 0x01020304050607\nd = 0x0\ne = 0x0\ng = 0x0\n\nTransaction trace:\nC.constructor()\nC.f()
// Warning 6328: (352-399): CHC: Assertion violation happens here.\nCounterexample:\n\nc = 0x01020304050607\nd = 0x010203040506070809000102030405\ne = 0x0\ng = 0x0\n\nTransaction trace:\nC.constructor()\nC.f()
// Warning 6328: (526-589): CHC: Assertion violation happens here.\nCounterexample:\n\nc = 0x01020304050607\nd = 0x010203040506070809000102030405\ne = 0x0102030405060708090001020304050607080900010203\ng = 0x0\n\nTransaction trace:\nC.constructor()\nC.f()
// Warning 6328: (732-811): CHC: Assertion violation happens here.\nCounterexample:\n\nc = 0x01020304050607\nd = 0x010203040506070809000102030405\ne = 0x0102030405060708090001020304050607080900010203\ng = 0x01020304050607080900010203040506070809000102030405060708090001\n\nTransaction trace:\nC.constructor()\nC.f()
// Warning 6328: (225-256): CHC: Assertion violation happens here.
// Warning 6328: (352-399): CHC: Assertion violation happens here.
// Warning 6328: (526-589): CHC: Assertion violation happens here.
// Warning 6328: (732-811): CHC: Assertion violation happens here.

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

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