From 64f81fe82b9a9246e01e2756aec6723744ae07c0 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Thu, 10 Dec 2020 18:53:25 +0100 Subject: [PATCH] Fix SMT tests --- .../external_hash_known_code_state_unsafe.sol | 6 ++++-- .../smtCheckerTests/external_calls/external_inc.sol | 2 +- .../smtCheckerTests/types/contract_address_conversion.sol | 2 +- .../types/struct/struct_state_var_array_pop_1.sol | 6 ++++-- 4 files changed, 10 insertions(+), 6 deletions(-) diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_unsafe.sol b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_unsafe.sol index 3d513a34e..b75510a58 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_unsafe.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_unsafe.sol @@ -37,6 +37,8 @@ contract C { assert(owner == address(0) || y != z); } } +// ==== +// SMTIgnoreCex: yes // ---- -// Warning 6328: (435-461): CHC: Assertion violation happens here.\nCounterexample:\nowner = 1, y = 0, z = 0, s = 0\n\n\n\nTransaction trace:\nconstructor()\nState: owner = 0, y = 0, z = 0, s = 0\nf() -// Warning 6328: (594-631): CHC: Assertion violation happens here.\nCounterexample:\nowner = 1, y = 0, z = 0, s = 0\n\n\n\nTransaction trace:\nconstructor()\nState: owner = 1, y = 0, z = 0, s = 0\ninv() +// Warning 6328: (435-461): CHC: Assertion violation happens here. +// Warning 6328: (594-631): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_inc.sol b/test/libsolidity/smtCheckerTests/external_calls/external_inc.sol index 9f6ce11a8..df0d61f5f 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/external_inc.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/external_inc.sol @@ -18,5 +18,5 @@ contract C { } } // ---- -// Warning 6328: (189-203): CHC: Assertion violation happens here.\nCounterexample:\nx = 10, d = 0\n\n\n\nTransaction trace:\nconstructor()\nState: x = 0, d = 0\ninc()\nState: x = 1, d = 0\nf() +// Warning 6328: (189-203): CHC: Assertion violation happens here.\nCounterexample:\nx = 10, d = 0\n\n\n\nTransaction trace:\nconstructor()\nState: x = 0, d = 0\ninc()\nState: x = 1, d = 0\ninc()\nState: x = 2, d = 0\nf() // Warning 2661: (146-149): BMC: Overflow (resulting value larger than 2**256 - 1) happens here. diff --git a/test/libsolidity/smtCheckerTests/types/contract_address_conversion.sol b/test/libsolidity/smtCheckerTests/types/contract_address_conversion.sol index db981653d..1e179dcaa 100644 --- a/test/libsolidity/smtCheckerTests/types/contract_address_conversion.sol +++ b/test/libsolidity/smtCheckerTests/types/contract_address_conversion.sol @@ -7,4 +7,4 @@ contract C } } // ---- -// Warning 6328: (90-113): CHC: Assertion violation happens here.\nCounterexample:\n\nc = 0\na = 1\n\n\nTransaction trace:\nconstructor()\nf(0, 1) +// Warning 6328: (90-113): CHC: Assertion violation happens here.\nCounterexample:\n\nc = 1\na = 0\n\n\nTransaction trace:\nconstructor()\nf(1, 0) diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_state_var_array_pop_1.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_state_var_array_pop_1.sol index d5276972e..50c9ede93 100644 --- a/test/libsolidity/smtCheckerTests/types/struct/struct_state_var_array_pop_1.sol +++ b/test/libsolidity/smtCheckerTests/types/struct/struct_state_var_array_pop_1.sol @@ -20,6 +20,8 @@ contract C { s.a.pop(); } } +// ==== +// SMTIgnoreCex: yes // ---- -// Warning 2529: (121-130): CHC: Empty array "pop" happens here.\nCounterexample:\ns = {x: 0, a: []}\n_x = 0\n\n\nTransaction trace:\nconstructor()\nState: s = {x: 0, a: []}\nf(0) -// Warning 6328: (230-254): CHC: Assertion violation happens here.\nCounterexample:\ns = {x: 7720, a: [7720, 0]}\n_x = 7720\n\n\nTransaction trace:\nconstructor()\nState: s = {x: 0, a: []}\nf(7720) +// Warning 2529: (121-130): CHC: Empty array "pop" happens here. +// Warning 6328: (230-254): CHC: Assertion violation happens here.