cerc-io/solidity
16
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Merge pull request #11796 from ethereum/smt_fix_develop

Browse Source 
Fix SMT test develop
This commit is contained in:
Daniel Kirchner 2021-08-12 23:15:21 +02:00 committed by GitHub
commit 4fdf7db02e
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
2 changed files with 6 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_1.sol
View File

@ -14,6 +14,7 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6328: (69-85): CHC: Assertion violation happens here.\nCounterexample:\n\n_x = 100\n = 0\n\nTransaction trace:\nState.constructor()\nState.f(100)
// Warning 6328: (177-191): CHC: Assertion violation happens here.\nCounterexample:\ns = 0, z = 0\n\nTransaction trace:\nC.constructor()\nState: s = 0, z = 0\nC.f()
// Warning 6328: (69-85): CHC: Assertion violation happens here.
// Warning 6328: (177-191): CHC: Assertion violation happens here.

4
test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_reentrancy_1.sol
View File

@ -11,5 +11,7 @@ contract C {
assert(a == 2); // should fail
}
}
// ====
// SMTIgnoreCex: yes
// ----
// Warning 6328: (253-267): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\nd = 0\na = 3\n\nTransaction trace:\nC.constructor(0)
// Warning 6328: (253-267): CHC: Assertion violation happens here.