From e7dede36d02e70399824298a052d26058e613554 Mon Sep 17 00:00:00 2001 From: Leo Alt Date: Mon, 7 Mar 2022 13:28:13 +0100 Subject: [PATCH] adjust old tests --- .../array_members/length_1d_struct_array_2d_1.sol | 2 +- .../array_members/length_same_after_assignment_3_fail.sol | 2 +- .../smtCheckerTests/array_members/push_as_lhs_1d.sol | 1 + .../smtCheckerTests/complex/slither/external_function.sol | 4 ++-- .../smtCheckerTests/external_calls/call_reentrancy_view.sol | 2 +- .../external_calls/external_call_indirect_1.sol | 3 ++- .../external_calls/external_call_indirect_4.sol | 1 - .../external_calls/external_call_semantic_this_1.sol | 2 +- .../external_calls/external_call_semantic_this_2.sol | 2 +- .../external_calls/external_call_this_with_value_1.sol | 2 +- .../external_calls/external_call_this_with_value_2.sol | 6 +++++- .../external_calls/external_reentrancy_1.sol | 4 +--- .../external_calls/external_reentrancy_2.sol | 4 +--- .../libsolidity/smtCheckerTests/file_level/new_operator.sol | 2 +- .../smtCheckerTests/functions/functions_external_2.sol | 2 +- .../functions/virtual_function_called_by_constructor.sol | 2 +- test/libsolidity/smtCheckerTests/imports/ExtCall.sol | 2 +- .../modifiers/modifier_same_local_variables.sol | 2 +- .../smtCheckerTests/operators/compound_add_array_index.sol | 2 +- .../smtCheckerTests/operators/compound_bitwise_or_int_1.sol | 1 - .../smtCheckerTests/operators/conditional_assignment_5.sol | 4 +++- .../smtCheckerTests/operators/conditional_assignment_6.sol | 2 +- .../smtCheckerTests/special/tx_vars_chc_internal.sol | 2 +- .../smtCheckerTests/special/tx_vars_reentrancy_1.sol | 1 + test/libsolidity/smtCheckerTests/try_catch/try_new.sol | 4 ++-- .../smtCheckerTests/try_catch/try_public_var_mapping.sol | 2 +- .../smtCheckerTests/types/fixed_bytes_access_3.sol | 3 ++- 27 files changed, 35 insertions(+), 31 deletions(-) diff --git a/test/libsolidity/smtCheckerTests/array_members/length_1d_struct_array_2d_1.sol b/test/libsolidity/smtCheckerTests/array_members/length_1d_struct_array_2d_1.sol index ddda215df..7950c8612 100644 --- a/test/libsolidity/smtCheckerTests/array_members/length_1d_struct_array_2d_1.sol +++ b/test/libsolidity/smtCheckerTests/array_members/length_1d_struct_array_2d_1.sol @@ -22,4 +22,4 @@ contract C { // SMTEngine: all // SMTIgnoreOS: macos // ---- -// Info 1180: Contract invariant(s) for :C:\n!(s1.arr.length <= 0)\n!(s2.arr.length <= 0)\n(((s2.arr[0].length + ((- 1) * s1.arr[0].length)) <= 0) && ((s1.arr[0].length + ((- 1) * s2.arr[0].length)) <= 0))\n +// Info 1180: Contract invariant(s) for :C:\n!(s1.arr.length <= 0)\n!(s2.arr.length <= 0)\n(((s1.arr[0].length + ((- 1) * s2.arr[0].length)) <= 0) && ((s2.arr[0].length + ((- 1) * s1.arr[0].length)) <= 0))\n diff --git a/test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment_3_fail.sol b/test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment_3_fail.sol index 7a7db383b..7af3af40d 100644 --- a/test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment_3_fail.sol +++ b/test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment_3_fail.sol @@ -31,4 +31,4 @@ contract C { // Warning 6328: (349-375): CHC: Assertion violation happens here.\nCounterexample:\narr = [[], [], [], [], [], [], [], [], []]\nx = 0\ny = 0\nz = 9\nt = 0\n\nTransaction trace:\nC.constructor()\nState: arr = [[], [], [], [], [], [], [], [], []]\nC.f() // Warning 6328: (379-402): CHC: Assertion violation happens here.\nCounterexample:\narr = [[], [], [], [], [], [], [], [], []]\nx = 0\ny = 0\nz = 9\nt = 0\n\nTransaction trace:\nC.constructor()\nState: arr = [[], [], [], [], [], [], [], [], []]\nC.f() // Warning 6328: (406-432): CHC: Assertion violation happens here.\nCounterexample:\narr = [[], [], [], [], [], [], [], [], []]\nx = 0\ny = 0\nz = 9\nt = 0\n\nTransaction trace:\nC.constructor()\nState: arr = [[], [], [], [], [], [], [], [], []]\nC.f() -// Info 1180: Contract invariant(s) for :C:\n!(arr.length <= 7)\n!(arr.length <= 8)\n +// Info 1180: Contract invariant(s) for :C:\n!(arr.length <= 5)\n!(arr.length <= 7)\n!(arr.length <= 8)\n diff --git a/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_1d.sol b/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_1d.sol index b38963b59..c377a159d 100644 --- a/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_1d.sol +++ b/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_1d.sol @@ -18,5 +18,6 @@ contract C { // ==== // SMTEngine: all // SMTIgnoreOS: macos +// SMTIgnoreCex: yes // ---- // Warning 6328: (199-229): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/complex/slither/external_function.sol b/test/libsolidity/smtCheckerTests/complex/slither/external_function.sol index 3f5096a3b..936ad1703 100644 --- a/test/libsolidity/smtCheckerTests/complex/slither/external_function.sol +++ b/test/libsolidity/smtCheckerTests/complex/slither/external_function.sol @@ -83,6 +83,6 @@ contract InternalCall { // Warning 2018: (1111-1173): Function state mutability can be restricted to pure // Warning 2018: (1179-1241): Function state mutability can be restricted to pure // Warning 2018: (1247-1309): Function state mutability can be restricted to pure -// Warning 4588: (681-716): Assertion checker does not yet implement this type of function call. -// Warning 4588: (854-886): Assertion checker does not yet implement this type of function call. +// Warning 8729: (681-716): Contract deployment is only supported in the trusted mode for external calls with the CHC engine. +// Warning 8729: (854-886): Contract deployment is only supported in the trusted mode for external calls with the CHC engine. // Warning 5729: (1370-1375): BMC does not yet implement this type of function call. diff --git a/test/libsolidity/smtCheckerTests/external_calls/call_reentrancy_view.sol b/test/libsolidity/smtCheckerTests/external_calls/call_reentrancy_view.sol index 87a9e2261..f0f844fff 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/call_reentrancy_view.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/call_reentrancy_view.sol @@ -15,4 +15,4 @@ contract C { // Warning 2519: (106-112): This declaration shadows an existing declaration. // Warning 2072: (106-112): Unused local variable. // Warning 2072: (114-131): Unused local variable. -// Info 1180: Contract invariant(s) for :C:\n(x <= 0)\nReentrancy property(ies) for :C:\n((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || ( <= 0)))\n = 0 -> no errors\n = 1 -> Assertion failed at assert(x == 0)\n +// Info 1180: Contract invariant(s) for :C:\n(x <= 0)\nReentrancy property(ies) for :C:\n((!(x <= 0) || (x' <= 0)) && (( <= 0) || !(x <= 0)))\n = 0 -> no errors\n = 1 -> Assertion failed at assert(x == 0)\n diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_1.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_1.sol index 4fef1dc99..86d54ae0e 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_1.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_1.sol @@ -36,5 +36,6 @@ contract C { // SMTEngine: chc // SMTExtCalls: trusted // ---- -// Warning 6328: (256-277): CHC: Assertion violation happens here. +// Warning 1218: (256-277): CHC: Error trying to invoke SMT solver. +// Warning 6328: (256-277): CHC: Assertion violation might happen here. // Warning 6328: (533-554): CHC: Assertion violation might happen here. diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_4.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_4.sol index 336a5c2d1..e115eb0e3 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_4.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_4.sol @@ -44,5 +44,4 @@ contract C { // SMTEngine: chc // SMTExtCalls: trusted // ---- -// Warning 1218: (641-662): CHC: Error trying to invoke SMT solver. // Warning 6328: (641-662): CHC: Assertion violation might happen here. diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_semantic_this_1.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_semantic_this_1.sol index 5e1ad8b1b..98ffab80f 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/external_call_semantic_this_1.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_semantic_this_1.sol @@ -13,4 +13,4 @@ contract C { // SMTExtCalls: trusted // SMTTargets: assert // ---- -// 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. diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_semantic_this_2.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_semantic_this_2.sol index 40e918862..0f05a8b73 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/external_call_semantic_this_2.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_semantic_this_2.sol @@ -13,4 +13,4 @@ contract C { // SMTExtCalls: trusted // SMTTargets: assert // ---- -// Warning 6328: (151-165): CHC: Assertion violation happens here. +// Warning 6328: (151-165): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f()\n C.i() -- trusted external call diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_this_with_value_1.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_this_with_value_1.sol index c52e0773f..06390b12c 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/external_call_this_with_value_1.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_this_with_value_1.sol @@ -11,4 +11,4 @@ contract C { // ==== // SMTEngine: all // ---- -// Warning 6328: (157-192): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g()\n C.h() -- trusted external call +// Warning 6328: (157-192): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_this_with_value_2.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_this_with_value_2.sol index fc2d844d9..f804078cd 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/external_call_this_with_value_2.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_this_with_value_2.sol @@ -1,7 +1,11 @@ contract C { function g(uint i) public { require(address(this).balance == 100); + // if called address is same as this, don't do anything with the value stuff + // or fix the receiving end this.h{value: i}(); + uint x = address(this).balance; + assert(x == 100); // should hold assert(address(this).balance == 100); // should hold assert(address(this).balance == 90); // should fail } @@ -12,4 +16,4 @@ contract C { // SMTEngine: all // SMTIgnoreCex: yes // ---- -// Warning 6328: (162-197): CHC: Assertion violation happens here. +// Warning 6328: (340-375): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_1.sol b/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_1.sol index 5683a5248..adde1eb61 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_1.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_1.sol @@ -16,6 +16,4 @@ contract C { // ==== // SMTEngine: all // ---- -// Warning 1218: (206-220): CHC: Error trying to invoke SMT solver. -// Warning 6328: (206-220): CHC: Assertion violation might happen here. -// Warning 4661: (206-220): BMC: Assertion violation happens here. +// Warning 6328: (206-220): CHC: Assertion violation happens here.\nCounterexample:\nlocked = false\ntarget = 0x0\n\nTransaction trace:\nC.constructor()\nState: locked = true\nC.call(0x0)\n D(target).e() -- untrusted external call, synthesized as:\n C.broken() -- reentrant call diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_2.sol b/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_2.sol index 1e8ce8816..19ff2bbad 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_2.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_2.sol @@ -13,6 +13,4 @@ contract C { // ==== // SMTEngine: all // ---- -// Warning 1218: (117-131): CHC: Error trying to invoke SMT solver. -// Warning 6328: (117-131): CHC: Assertion violation might happen here. -// Warning 4661: (117-131): BMC: Assertion violation happens here. +// Warning 6328: (117-131): CHC: Assertion violation happens here.\nCounterexample:\nlocked = false\ntarget = 0x0\n\nTransaction trace:\nC.constructor()\nState: locked = true\nC.call(0x0)\n D(target).e() -- untrusted external call, synthesized as:\n C.call(0x0) -- reentrant call diff --git a/test/libsolidity/smtCheckerTests/file_level/new_operator.sol b/test/libsolidity/smtCheckerTests/file_level/new_operator.sol index 8a0f118ae..925f53bc9 100644 --- a/test/libsolidity/smtCheckerTests/file_level/new_operator.sol +++ b/test/libsolidity/smtCheckerTests/file_level/new_operator.sol @@ -14,5 +14,5 @@ contract D { // ==== // SMTEngine: all // ---- -// Warning 4588: (78-85): Assertion checker does not yet implement this type of function call. +// Warning 8729: (78-85): Contract deployment is only supported in the trusted mode for external calls with the CHC engine. // Warning 6328: (133-152): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nD.constructor()\nD.f()\n test() -- internal call\n (new C()).x() -- untrusted external call diff --git a/test/libsolidity/smtCheckerTests/functions/functions_external_2.sol b/test/libsolidity/smtCheckerTests/functions/functions_external_2.sol index 5efcb2da1..3a3b295e4 100644 --- a/test/libsolidity/smtCheckerTests/functions/functions_external_2.sol +++ b/test/libsolidity/smtCheckerTests/functions/functions_external_2.sol @@ -25,4 +25,4 @@ contract C // SMTIgnoreOS: macos // ---- // Warning 6328: (234-253): CHC: Assertion violation happens here. -// Info 1180: Reentrancy property(ies) for :C:\n!( = 1)\n((!((map[1] + ((- 1) * map[0])) <= 0) || ((map'[1] + ((- 1) * map'[0])) <= 0)) && !( = 2) && (!((map[1] + ((- 1) * map[0])) >= 0) || ((map'[0] + ((- 1) * map'[1])) <= 0)))\n = 0 -> no errors\n = 1 -> Assertion failed at assert(map[0] == map[1])\n = 2 -> Assertion failed at assert(map[0] == map[1])\n = 3 -> Assertion failed at assert(map[0] == 0)\n +// Info 1180: Reentrancy property(ies) for :C:\n!( = 1)\n((!((map[1] + ((- 1) * map[0])) >= 0) || ((map'[0] + ((- 1) * map'[1])) <= 0)) && !( = 2) && (!((map[1] + ((- 1) * map[0])) <= 0) || ((map'[1] + ((- 1) * map'[0])) <= 0)))\n = 0 -> no errors\n = 1 -> Assertion failed at assert(map[0] == map[1])\n = 2 -> Assertion failed at assert(map[0] == map[1])\n = 3 -> Assertion failed at assert(map[0] == 0)\n diff --git a/test/libsolidity/smtCheckerTests/functions/virtual_function_called_by_constructor.sol b/test/libsolidity/smtCheckerTests/functions/virtual_function_called_by_constructor.sol index 0117f9b49..e30a5e743 100644 --- a/test/libsolidity/smtCheckerTests/functions/virtual_function_called_by_constructor.sol +++ b/test/libsolidity/smtCheckerTests/functions/virtual_function_called_by_constructor.sol @@ -27,4 +27,4 @@ contract C is A { // ---- // Warning 6328: (199-214): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n\nTransaction trace:\nA.constructor()\nState: x = 2\nA.i() // Warning 6328: (387-401): CHC: Assertion violation happens here.\nCounterexample:\nx = 10\n\nTransaction trace:\nC.constructor()\nState: x = 10\nC.i() -// Info 1180: Contract invariant(s) for :A:\n(!(x <= 1) && !(x >= 3))\nContract invariant(s) for :C:\n(!(x >= 11) && !(x <= 9))\n +// Info 1180: Contract invariant(s) for :A:\n(!(x <= 1) && !(x >= 3))\nContract invariant(s) for :C:\n(!(x <= 9) && !(x >= 11))\n diff --git a/test/libsolidity/smtCheckerTests/imports/ExtCall.sol b/test/libsolidity/smtCheckerTests/imports/ExtCall.sol index 047148a90..7675bc42e 100644 --- a/test/libsolidity/smtCheckerTests/imports/ExtCall.sol +++ b/test/libsolidity/smtCheckerTests/imports/ExtCall.sol @@ -39,4 +39,4 @@ contract ExtCallTest { // SMTIgnoreCex: yes // ---- // Warning 6328: (ExtCall.sol:362-381): CHC: Assertion violation happens here. -// Warning 4588: (ExtCall.t.sol:110-123): Assertion checker does not yet implement this type of function call. +// Warning 8729: (ExtCall.t.sol:110-123): Contract deployment is only supported in the trusted mode for external calls with the CHC engine. diff --git a/test/libsolidity/smtCheckerTests/modifiers/modifier_same_local_variables.sol b/test/libsolidity/smtCheckerTests/modifiers/modifier_same_local_variables.sol index 1d86c0fea..89d67b53e 100644 --- a/test/libsolidity/smtCheckerTests/modifiers/modifier_same_local_variables.sol +++ b/test/libsolidity/smtCheckerTests/modifiers/modifier_same_local_variables.sol @@ -12,4 +12,4 @@ contract C // ==== // SMTEngine: all // ---- -// Warning 6328: (88-102): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\nx = 2\n\nTransaction trace:\nC.constructor()\nC.f(0) +// Warning 6328: (88-102): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 3\nx = 2\n\nTransaction trace:\nC.constructor()\nC.f(3) diff --git a/test/libsolidity/smtCheckerTests/operators/compound_add_array_index.sol b/test/libsolidity/smtCheckerTests/operators/compound_add_array_index.sol index 4186f39fe..1c6e205d3 100644 --- a/test/libsolidity/smtCheckerTests/operators/compound_add_array_index.sol +++ b/test/libsolidity/smtCheckerTests/operators/compound_add_array_index.sol @@ -20,4 +20,4 @@ contract C // SMTEngine: all // SMTIgnoreOS: macos // ---- -// Warning 6328: (262-284): CHC: Assertion violation happens here.\nCounterexample:\narray = [200, 0]\nx = 0\np = 0\n\nTransaction trace:\nC.constructor()\nState: array = [0, 0]\nC.f(0, 0) +// Warning 6328: (262-284): CHC: Assertion violation happens here.\nCounterexample:\narray = [299, 0]\nx = 99\np = 0\n\nTransaction trace:\nC.constructor()\nState: array = [0, 0]\nC.f(99, 0) diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_int_1.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_int_1.sol index fdd8c55cc..252cad51f 100644 --- a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_int_1.sol +++ b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_int_1.sol @@ -12,7 +12,6 @@ contract C { // SMTIgnoreOS: macos // ---- // Warning 6368: (76-81): CHC: Out of bounds access might happen here. -// Warning 6368: (76-84): CHC: Out of bounds access might happen here. // Warning 6368: (119-124): CHC: Out of bounds access might happen here. // Warning 6368: (119-127): CHC: Out of bounds access might happen here. // Warning 6368: (149-154): CHC: Out of bounds access might happen here. diff --git a/test/libsolidity/smtCheckerTests/operators/conditional_assignment_5.sol b/test/libsolidity/smtCheckerTests/operators/conditional_assignment_5.sol index 24be3cd8e..dd467f853 100644 --- a/test/libsolidity/smtCheckerTests/operators/conditional_assignment_5.sol +++ b/test/libsolidity/smtCheckerTests/operators/conditional_assignment_5.sol @@ -25,4 +25,6 @@ contract C { // SMTIgnoreCex: yes // ---- // Warning 2072: (249-255): Unused local variable. -// Warning 6328: (271-295): CHC: Assertion violation happens here. +// Warning 1218: (271-295): CHC: Error trying to invoke SMT solver. +// Warning 6328: (271-295): CHC: Assertion violation might happen here. +// Warning 4661: (271-295): BMC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/operators/conditional_assignment_6.sol b/test/libsolidity/smtCheckerTests/operators/conditional_assignment_6.sol index b26fcbd93..923147d49 100644 --- a/test/libsolidity/smtCheckerTests/operators/conditional_assignment_6.sol +++ b/test/libsolidity/smtCheckerTests/operators/conditional_assignment_6.sol @@ -25,4 +25,4 @@ contract C { // SMTIgnoreOS: macos // ---- // Warning 2072: (255-261): Unused local variable. -// Info 1180: Reentrancy property(ies) for :C:\n((!(x' >= 3) || (a' = a)) && ( <= 0) && (!(x' <= 0) || !(x >= 2)) && (!(x <= 2) || !(x' >= 3)))\n = 0 -> no errors\n = 1 -> Assertion failed at assert(x == 2 || x == 1)\n +// Info 1180: Reentrancy property(ies) for :C:\n((!(x <= 2) || !(x' >= 3)) && ( <= 0) && (!(x' <= 0) || !(x >= 2)))\n = 0 -> no errors\n = 1 -> Assertion failed at assert(x == 2 || x == 1)\n diff --git a/test/libsolidity/smtCheckerTests/special/tx_vars_chc_internal.sol b/test/libsolidity/smtCheckerTests/special/tx_vars_chc_internal.sol index 95e3390b4..6e876daf3 100644 --- a/test/libsolidity/smtCheckerTests/special/tx_vars_chc_internal.sol +++ b/test/libsolidity/smtCheckerTests/special/tx_vars_chc_internal.sol @@ -21,4 +21,4 @@ contract C { // SMTEngine: chc // SMTIgnoreOS: macos // ---- -// Warning 6328: (343-377): CHC: Assertion violation happens here.\nCounterexample:\ngas = 0, origin = 0x52f7\n\nTransaction trace:\nC.constructor()\nState: gas = 0, origin = 0x0\nC.f(){ tx.gasprice: 0, tx.origin: 0x52f7 }\n C.g() -- internal call +// Warning 6328: (343-377): CHC: Assertion violation happens here.\nCounterexample:\ngas = 0, origin = 0x0\n\nTransaction trace:\nC.constructor()\nState: gas = 0, origin = 0x0\nC.f(){ tx.gasprice: 0, tx.origin: 0x0 }\n C.g() -- internal call diff --git a/test/libsolidity/smtCheckerTests/special/tx_vars_reentrancy_1.sol b/test/libsolidity/smtCheckerTests/special/tx_vars_reentrancy_1.sol index f1fed73c0..fd2aad6f9 100644 --- a/test/libsolidity/smtCheckerTests/special/tx_vars_reentrancy_1.sol +++ b/test/libsolidity/smtCheckerTests/special/tx_vars_reentrancy_1.sol @@ -11,6 +11,7 @@ contract C { } // ==== // SMTEngine: all +// SMTIgnoreCex: yes // SMTIgnoreOS: macos // ---- // Warning 6328: (135-169): CHC: Assertion violation happens here.\nCounterexample:\n\n_i = 0\nx = 9726\n\nTransaction trace:\nC.constructor()\nC.g(0){ msg.value: 2070 }\n _i.f() -- untrusted external call, synthesized as:\n C.g(0){ msg.value: 0 } -- reentrant call\n _i.f() -- untrusted external call diff --git a/test/libsolidity/smtCheckerTests/try_catch/try_new.sol b/test/libsolidity/smtCheckerTests/try_catch/try_new.sol index e7075e076..5c98c279d 100644 --- a/test/libsolidity/smtCheckerTests/try_catch/try_new.sol +++ b/test/libsolidity/smtCheckerTests/try_catch/try_new.sol @@ -28,5 +28,5 @@ contract C { // ==== // SMTEngine: all // ---- -// Warning 4588: (231-245): Assertion checker does not yet implement this type of function call. -// Warning 4588: (492-507): Assertion checker does not yet implement this type of function call. +// Warning 8729: (231-245): Contract deployment is only supported in the trusted mode for external calls with the CHC engine. +// Warning 8729: (492-507): Contract deployment is only supported in the trusted mode for external calls with the CHC engine. diff --git a/test/libsolidity/smtCheckerTests/try_catch/try_public_var_mapping.sol b/test/libsolidity/smtCheckerTests/try_catch/try_public_var_mapping.sol index 0854dedd1..454f339e5 100644 --- a/test/libsolidity/smtCheckerTests/try_catch/try_public_var_mapping.sol +++ b/test/libsolidity/smtCheckerTests/try_catch/try_public_var_mapping.sol @@ -22,4 +22,4 @@ contract C { // SMTIgnoreOS: macos // ---- // Warning 6328: (280-300): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() -// Info 1180: Contract invariant(s) for :C:\n!(m[0].length <= 1)\n(!(m[0][1] >= 43) && !(m[0][1] <= 41))\n +// Info 1180: Contract invariant(s) for :C:\n!(m[0].length <= 1)\n(!(m[0][1] <= 41) && !(m[0][1] >= 43))\n diff --git a/test/libsolidity/smtCheckerTests/types/fixed_bytes_access_3.sol b/test/libsolidity/smtCheckerTests/types/fixed_bytes_access_3.sol index 320d7dd10..b55293231 100644 --- a/test/libsolidity/smtCheckerTests/types/fixed_bytes_access_3.sol +++ b/test/libsolidity/smtCheckerTests/types/fixed_bytes_access_3.sol @@ -32,5 +32,6 @@ contract C { // SMTEngine: all // SMTIgnoreOS: macos // ---- +// Warning 6368: (374-381): CHC: Out of bounds access might happen here. // Warning 6368: (456-462): CHC: Out of bounds access happens here. -// Info 1180: Contract invariant(s) for :C:\n!(a.length <= 4)\n!(a[2].length <= 2)\n +// Info 1180: Contract invariant(s) for :C:\n!(a.length <= 4)\n