macos nondeterminism

Leo Alt · Leo Alt · commit 22ec5444d950 · 2021-11-24T11:38:22.000+01:00
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
@@ -20,5 +20,6 @@ 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
diff --git a/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_1d.sol b/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_1d.sol
@@ -17,5 +17,6 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreOS: macos
 // ----
 // Warning 6328: (199-229): CHC: Assertion violation happens here.\nCounterexample:\nb = [1]\n\nTransaction trace:\nC.constructor()\nState: b = []\nC.g()
diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_4.sol b/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_4.sol
@@ -11,6 +11,7 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreOS: macos
 // ----
 // Warning 4984: (82-85): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
 // Warning 4984: (154-160): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_ext_calls.sol b/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_ext_calls.sol
@@ -12,6 +12,7 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreOS: macos
 // ----
 // Warning 1218: (131-165): CHC: Error trying to invoke SMT solver.
 // Warning 6328: (131-165): CHC: Assertion violation might happen here.
diff --git a/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/branches_in_modifiers_2.sol b/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/branches_in_modifiers_2.sol
@@ -42,6 +42,7 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreOS: macos
 // ----
 // Warning 6328: (255-269): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.test()\n    C.reset_if_overflow() -- internal call
 // Warning 6328: (502-519): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\noldx = 1\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.set(1)\nState: x = 1\nC.test()\n    C.reset_if_overflow() -- internal call
diff --git a/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/triple_nested_if.sol b/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/triple_nested_if.sol
@@ -17,5 +17,6 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreOS: macos
 // ----
 // Info 1180: Contract invariant(s) for :C:\n((c <= 0) && (a <= 0) && (b <= 0))\n
diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_with_value_3.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_with_value_3.sol
@@ -12,6 +12,7 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreOS: macos
 // ----
 // Warning 6328: (150-183): CHC: Assertion violation might happen here.
 // Warning 6328: (202-236): CHC: Assertion violation happens here.\nCounterexample:\n\ni = 0\n\nTransaction trace:\nC.constructor()\nC.g(0)\n    i.f{value: 20}() -- untrusted external call
diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_unsafe.sol b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_unsafe.sol
@@ -34,6 +34,7 @@ contract C {
 // ====
 // SMTEngine: all
 // SMTIgnoreCex: yes
+// SMTIgnoreOS: macos
 // ----
 // Warning 6328: (348-362): CHC: Assertion violation happens here.
 // Warning 6328: (366-392): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/operators/assignment_module_contract_member_variable.sol b/test/libsolidity/smtCheckerTests/operators/assignment_module_contract_member_variable.sol
@@ -27,6 +27,7 @@ contract A {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreOS: macos
 // ----
 // Warning 6328: (AASource:159-178): CHC: Assertion violation happens here.\nCounterexample:\nx = (- 1), y = (- 2)\n\nTransaction trace:\nA.constructor()\nState: x = 0, y = 0\nA.a()\nState: x = (- 2), y = (- 2)\nA.a()
 // Warning 6328: (AASource:370-386): CHC: Assertion violation happens here.\nCounterexample:\nx = 8, y = (- 2)\n\nTransaction trace:\nA.constructor()\nState: x = 0, y = 0\nA.a()
diff --git a/test/libsolidity/smtCheckerTests/operators/compound_add_array_index.sol b/test/libsolidity/smtCheckerTests/operators/compound_add_array_index.sol
@@ -18,5 +18,6 @@ contract C
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreOS: macos
 // ----
 // 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_add_mapping.sol b/test/libsolidity/smtCheckerTests/operators/compound_add_mapping.sol
@@ -11,5 +11,6 @@ contract C
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreOS: macos
 // ----
 // Warning 6328: (165-185): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\np = 0\n\nTransaction trace:\nC.constructor()\nC.f(0, 0)
diff --git a/test/libsolidity/smtCheckerTests/operators/compound_assignment_division_3.sol b/test/libsolidity/smtCheckerTests/operators/compound_assignment_division_3.sol
@@ -10,5 +10,6 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreOS: macos
 // ----
 // Warning 6328: (162-181): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 2\np = 0\n\nTransaction trace:\nC.constructor()\nC.f(2, 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
@@ -9,6 +9,7 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// 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.
diff --git a/test/libsolidity/smtCheckerTests/special/tx_vars_chc_internal.sol b/test/libsolidity/smtCheckerTests/special/tx_vars_chc_internal.sol
@@ -19,5 +19,6 @@ 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
diff --git a/test/libsolidity/smtCheckerTests/userTypes/multisource_module.sol b/test/libsolidity/smtCheckerTests/userTypes/multisource_module.sol
@@ -15,6 +15,7 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreOS: macos
 // ----
 // Warning 6328: (s2.sol:259-292): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.h()\n    C.f(5) -- internal call\n    C.f(5) -- internal call
 // Warning 6328: (s2.sol:346-377): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.h()\n    C.f(5) -- internal call\n    C.f(5) -- internal call\n    C.g(1) -- internal call\n    C.g(1) -- internal call

Original file line number	Diff line number	Diff line change
`@@ -20,5 +20,6 @@ contract C {`
`20`	`20`	`}`
`21`	`21`	`// ====`
`22`	`22`	`// SMTEngine: all`
	`23`	`+// SMTIgnoreOS: macos`
`23`	`24`	`// ----`
`24`	`25`	`// 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`
Original file line number	Diff line number	Diff line change
`@@ -17,5 +17,6 @@ contract C {`
`17`	`17`	`}`
`18`	`18`	`// ====`
`19`	`19`	`// SMTEngine: all`
	`20`	`+// SMTIgnoreOS: macos`
`20`	`21`	`// ----`
`21`	`22`	`// Warning 6328: (199-229): CHC: Assertion violation happens here.\nCounterexample:\nb = [1]\n\nTransaction trace:\nC.constructor()\nState: b = []\nC.g()`
Original file line number	Diff line number	Diff line change
`@@ -11,6 +11,7 @@ contract C {`
`11`	`11`	`}`
`12`	`12`	`// ====`
`13`	`13`	`// SMTEngine: all`
	`14`	`+// SMTIgnoreOS: macos`
`14`	`15`	`// ----`
`15`	`16`	`// Warning 4984: (82-85): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.`
`16`	`17`	`// Warning 4984: (154-160): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.`
Original file line number	Diff line number	Diff line change
`@@ -12,6 +12,7 @@ contract C {`
`12`	`12`	`}`
`13`	`13`	`// ====`
`14`	`14`	`// SMTEngine: all`
	`15`	`+// SMTIgnoreOS: macos`
`15`	`16`	`// ----`
`16`	`17`	`// Warning 1218: (131-165): CHC: Error trying to invoke SMT solver.`
`17`	`18`	`// Warning 6328: (131-165): CHC: Assertion violation might happen here.`
Original file line number	Diff line number	Diff line change
`@@ -42,6 +42,7 @@ contract C {`
`42`	`42`	`}`
`43`	`43`	`// ====`
`44`	`44`	`// SMTEngine: all`
	`45`	`+// SMTIgnoreOS: macos`
`45`	`46`	`// ----`
`46`	`47`	`// Warning 6328: (255-269): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.test()\n C.reset_if_overflow() -- internal call`
`47`	`48`	`// Warning 6328: (502-519): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\noldx = 1\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.set(1)\nState: x = 1\nC.test()\n C.reset_if_overflow() -- internal call`
Original file line number	Diff line number	Diff line change
`@@ -27,6 +27,7 @@ contract A {`
`27`	`27`	`}`
`28`	`28`	`// ====`
`29`	`29`	`// SMTEngine: all`
	`30`	`+// SMTIgnoreOS: macos`
`30`	`31`	`// ----`
`31`	`32`	`// Warning 6328: (AASource:159-178): CHC: Assertion violation happens here.\nCounterexample:\nx = (- 1), y = (- 2)\n\nTransaction trace:\nA.constructor()\nState: x = 0, y = 0\nA.a()\nState: x = (- 2), y = (- 2)\nA.a()`
`32`	`33`	`// Warning 6328: (AASource:370-386): CHC: Assertion violation happens here.\nCounterexample:\nx = 8, y = (- 2)\n\nTransaction trace:\nA.constructor()\nState: x = 0, y = 0\nA.a()`
Original file line number	Diff line number	Diff line change
`@@ -18,5 +18,6 @@ contract C`
`18`	`18`	`}`
`19`	`19`	`// ====`
`20`	`20`	`// SMTEngine: all`
	`21`	`+// SMTIgnoreOS: macos`
`21`	`22`	`// ----`
`22`	`23`	`// 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)`