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 tests for nondeterminism

Browse Source
This commit is contained in:
Leo Alt 2022-03-15 12:40:00 +01:00
parent 17add47a27
commit 7092caf6bf
5 changed files with 6 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_1_trusted.sol
View File

@ -16,6 +16,6 @@ contract C {
// SMTContract: C
// SMTEngine: all
// SMTExtCalls: trusted
// SMTIgnoreInv: 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)
// Info 1180: Contract invariant(s) for :C:\n(!(z >= 3) && !(z <= 1))\n

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

@ -19,5 +19,6 @@ contract C {
// SMTEngine: chc
// SMTExtCalls: trusted
// SMTTargets: assert
// SMTIgnoreCex: yes
// ----
// Warning 6328: (179-199): CHC: Assertion violation happens here.

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

@ -22,5 +22,6 @@ contract C {
// SMTEngine: chc
// SMTExtCalls: trusted
// SMTTargets: assert
// SMTIgnoreCex: yes
// ----
// Warning 6328: (205-227): CHC: Assertion violation happens here.\nCounterexample:\nt = {s: {d: 20819}}\n\nTransaction trace:\nC.constructor()\nState: t = {s: {d: 20819}}\nC.f()
// Warning 6328: (205-227): CHC: Assertion violation happens here.

1
test/libsolidity/smtCheckerTests/functions/getters/external_getter_this_1.sol
View File

@ -13,5 +13,6 @@ contract C {
// SMTEngine: chc
// SMTExtCalls: trusted
// SMTTargets: assert
// SMTIgnoreCex: yes
// ----
// Warning 6328: (127-141): CHC: Assertion violation happens here.

1
test/libsolidity/smtCheckerTests/functions/getters/external_getter_this_2.sol
View File

@ -14,5 +14,6 @@ contract C {
// SMTEngine: chc
// SMTExtCalls: trusted
// SMTTargets: assert
// SMTIgnoreCex: yes
// ----
// Warning 6328: (138-152): CHC: Assertion violation happens here.