Merge remote-tracking branch 'origin/develop' into HEAD

test/EVMHost.cpp

@@ -123,6 +123,22 @@ EVMHost::EVMHost(langutil::EVMVersion _evmVersion, evmc::VM& _vm):
 	else
 		assertThrow(false, Exception, "Unsupported EVM version");
 
+	tx_context.block_difficulty = evmc::uint256be{200000000};
+	tx_context.block_gas_limit = 20000000;
+	tx_context.block_coinbase = 0x7878787878787878787878787878787878787878_address;
+	tx_context.tx_gas_price = evmc::uint256be{3000000000};
+	tx_context.tx_origin = 0x9292929292929292929292929292929292929292_address;
+	// Mainnet according to EIP-155
+	tx_context.chain_id = evmc::uint256be{1};
+
+	reset();
+}
+
+void EVMHost::reset()
+{
+	accounts.clear();
+	m_currentAddress = {};
+
 	// Mark all precompiled contracts as existing. Existing here means to have a balance (as per EIP-161).
 	// NOTE: keep this in sync with `EVMHost::call` below.
 	//
@@ -131,19 +147,13 @@ EVMHost::EVMHost(langutil::EVMVersion _evmVersion, evmc::VM& _vm):
 	// roughly 22 days before the update went live.
 	for (unsigned precompiledAddress = 1; precompiledAddress <= 8; precompiledAddress++)
 	{
-		evmc::address address{};
-		address.bytes[19] = precompiledAddress;
+		evmc::address address{precompiledAddress};
 		// 1wei
 		accounts[address].balance = evmc::uint256be{1};
+		// Set according to EIP-1052.
+		if (precompiledAddress < 5 || m_evmVersion >= langutil::EVMVersion::byzantium())
+			accounts[address].codehash = 0xc5d2460186f7233c927e7db2dcc703c0e500b653ca82273b7bfad8045d85a470_bytes32;
 	}
-
-	tx_context.block_difficulty = evmc::uint256be{200000000};
-	tx_context.block_gas_limit = 20000000;
-	tx_context.block_coinbase = 0x7878787878787878787878787878787878787878_address;
-	tx_context.tx_gas_price = evmc::uint256be{3000000000};
-	tx_context.tx_origin = 0x9292929292929292929292929292929292929292_address;
-	// Mainnet according to EIP-155
-	tx_context.chain_id = evmc::uint256be{1};
 }
 
 void EVMHost::selfdestruct(const evmc::address& _addr, const evmc::address& _beneficiary) noexcept

test/EVMHost.h

@@ -54,7 +54,7 @@ public:
 
 	explicit EVMHost(langutil::EVMVersion _evmVersion, evmc::VM& _vm);
 
-	void reset() { accounts.clear(); m_currentAddress = {}; }
+	void reset();
 	void newBlock()
 	{
 		tx_context.block_number++;

test/libsolidity/SolidityParser.cpp

@@ -599,42 +599,6 @@ BOOST_AUTO_TEST_CASE(complex_import)
 	BOOST_CHECK(successParse(text));
 }
 
-BOOST_AUTO_TEST_CASE(recursion_depth1)
-{
-	string text("contract C { bytes");
-	for (size_t i = 0; i < 30000; i++)
-		text += "[";
-	CHECK_PARSE_ERROR(text.c_str(), "Maximum recursion depth reached during parsing");
-}
-
-BOOST_AUTO_TEST_CASE(recursion_depth2)
-{
-	string text("contract C { function f() {");
-	for (size_t i = 0; i < 30000; i++)
-		text += "{";
-	CHECK_PARSE_ERROR(text, "Maximum recursion depth reached during parsing");
-}
-
-BOOST_AUTO_TEST_CASE(recursion_depth3)
-{
-	string text("contract C { function f() { uint x = f(");
-	for (size_t i = 0; i < 30000; i++)
-		text += "(";
-	CHECK_PARSE_ERROR(text, "Maximum recursion depth reached during parsing");
-}
-
-BOOST_AUTO_TEST_CASE(recursion_depth4)
-{
-	string text("contract C { function f() { uint a;");
-	for (size_t i = 0; i < 30000; i++)
-		text += "(";
-	text += "a";
-	for (size_t i = 0; i < 30000; i++)
-		text += "++)";
-	text += "}}";
-	CHECK_PARSE_ERROR(text, "Maximum recursion depth reached during parsing");
-}
-
 BOOST_AUTO_TEST_CASE(inline_asm_end_location)
 {
 	auto sourceCode = std::string(R"(

test/libsolidity/semanticTests/freeFunctions/free_namesake_contract_function.sol

@@ -0,0 +1,10 @@
+function f() pure returns (uint) { return 1337; }
+contract C {
+  function f() public pure returns (uint) {
+    return f();
+  }
+}
+// ====
+// compileViaYul: also
+// ----
+// f() -> FAILURE

test/libsolidity/semanticTests/multiSource/circular_import.sol

@@ -0,0 +1,15 @@
+==== Source: s1.sol ====
+import {f as g} from "s2.sol";
+function f() pure returns (uint) { return 1; }
+==== Source: s2.sol ====
+import {f as g} from "s1.sol";
+function f() pure returns (uint) { return 2; }
+contract C {
+  function foo() public pure returns (uint) {
+    return f() - g();
+  }
+}
+// ====
+// compileViaYul: also
+// ----
+// foo() -> 1

test/libsolidity/semanticTests/multiSource/circular_import_2.sol

@@ -0,0 +1,14 @@
+==== Source: s1.sol ====
+import {f as g, g as h} from "s2.sol";
+function f() pure returns (uint) { return h() - g(); }
+==== Source: s2.sol ====
+import {f as h} from "s1.sol";
+function f() pure returns (uint) { return 2; }
+function g() pure returns (uint) { return 4; }
+contract C {
+  function foo() public pure returns (uint) {
+    return h() - f() - g();
+  }
+}
+// ----
+// foo() -> -4

test/libsolidity/semanticTests/multiSource/circular_reimport.sol

@@ -0,0 +1,16 @@
+==== Source: s1.sol ====
+import {f as g, g as h} from "s2.sol";
+function f() pure returns (uint) { return h() - g(); }
+==== Source: s2.sol ====
+import {f as h} from "s1.sol";
+function f() pure returns (uint) { return 2; }
+function g() pure returns (uint) { return 4; }
+==== Source: s3.sol ====
+import "s1.sol";
+contract C {
+  function foo() public pure returns (uint) {
+    return f() - g() - h();
+  }
+}
+// ----
+// foo() -> -4

test/libsolidity/semanticTests/multiSource/circular_reimport_2.sol

@@ -0,0 +1,16 @@
+==== Source: s1.sol ====
+import {f as g, g as h} from "s2.sol";
+function f() pure returns (uint) { return h() - g(); }
+==== Source: s2.sol ====
+import {f as h} from "s1.sol";
+function f() pure returns (uint) { return 2; }
+function g() pure returns (uint) { return 4; }
+==== Source: s3.sol ====
+import "s2.sol";
+contract C {
+  function foo() public pure returns (uint) {
+    return f() - g() - h();
+  }
+}
+// ----
+// foo() -> -4

test/libsolidity/semanticTests/multiSource/free_different_interger_types.sol

@@ -0,0 +1,14 @@
+==== Source: s1.sol ====
+function f(uint24) pure returns (uint) { return 24; }
+function g(bool) pure returns (bool) { return true; }
+==== Source: s2.sol ====
+import {f as g, g as g} from "s1.sol";
+contract C {
+  function foo() public pure returns (uint, bool) {
+    return (g(2), g(false));
+  }
+}
+// ====
+// compileViaYul: also
+// ----
+// foo() -> 24, true

test/libsolidity/semanticTests/multiSource/free_function_resolution_base_contract.sol

@@ -0,0 +1,18 @@
+==== Source: s1.sol ====
+function f() pure returns (uint) { return 1337; }
+contract C {
+  function g() public pure returns (uint) {
+    return f();
+  }
+}
+==== Source: s2.sol ====
+import "s1.sol";
+contract D is C {
+  function h() public pure returns (uint) {
+    return g();
+  }
+}
+// ====
+// compileViaYul: also
+// ----
+// h() -> 1337

test/libsolidity/semanticTests/multiSource/free_function_resolution_override_virtual.sol

@@ -0,0 +1,18 @@
+==== Source: s1.sol ====
+function f() pure returns (uint) { return 1337; }
+contract C {
+  function g() public pure virtual returns (uint) {
+    return f() + 1;
+  }
+}
+==== Source: s2.sol ====
+import "s1.sol";
+contract D is C {
+  function g() public pure override returns (uint) {
+    return f();
+  }
+}
+// ====
+// compileViaYul: also
+// ----
+// g() -> 1337

test/libsolidity/semanticTests/multiSource/free_function_resolution_override_virtual_super.sol

@@ -0,0 +1,18 @@
+==== Source: s1.sol ====
+function f() pure returns (uint) { return 1337; }
+contract C {
+  function g() public pure virtual returns (uint) {
+    return f();
+  }
+}
+==== Source: s2.sol ====
+import "s1.sol";
+contract D is C {
+  function g() public pure override returns (uint) {
+    return super.g();
+  }
+}
+// ====
+// compileViaYul: also
+// ----
+// g() -> 1337

test/libsolidity/semanticTests/multiSource/free_function_resolution_override_virtual_transitive.sol

@@ -0,0 +1,25 @@
+==== Source: s1.sol ====
+function f() pure returns (uint) { return 1337; }
+contract C {
+  function g() public pure virtual returns (uint) {
+    return f();
+  }
+}
+==== Source: s2.sol ====
+import "s1.sol";
+contract D is C {
+  function g() public pure virtual override returns (uint) {
+    return super.g() + 1;
+  }
+}
+==== Source: s3.sol ====
+import "s2.sol";
+contract E is D {
+  function g() public pure override returns (uint) {
+    return super.g() + 1;
+  }
+}
+// ====
+// compileViaYul: also
+// ----
+// g() -> 1339

test/libsolidity/semanticTests/multiSource/free_function_transitive_import.sol

@@ -0,0 +1,27 @@
+==== Source: s1.sol ====
+function f() pure returns (uint) { return 1337; }
+contract C {
+  function g() public pure returns (uint) {
+    return f();
+  }
+}
+==== Source: s2.sol ====
+import "s1.sol";
+contract D is C {
+  function h() public pure returns (uint) {
+    return g();
+  }
+}
+==== Source: s3.sol ====
+import "s2.sol";
+import {f as f} from "s2.sol";
+contract E is D {
+  function i() public pure returns (uint) {
+    return f();
+  }
+}
+
+// ====
+// compileViaYul: also
+// ----
+// i() -> 1337

test/libsolidity/semanticTests/multiSource/imported_free_function_via_alias.sol

@@ -0,0 +1,19 @@
+==== Source: s1.sol ====
+function f() pure returns (uint) { return 1337; }
+contract C {
+  function g() public pure virtual returns (uint) {
+    return f();
+  }
+}
+==== Source: s2.sol ====
+import "s1.sol" as M;
+function f() pure returns (uint) { return 6; }
+contract D is M.C {
+  function g() public pure override returns (uint) {
+    return super.g() + f() * 10000;
+  }
+}
+// ====
+// compileViaYul: also
+// ----
+// g() -> 61337

test/libsolidity/semanticTests/multiSource/imported_free_function_via_alias_direct_call.sol

@@ -0,0 +1,14 @@
+==== Source: s1.sol ====
+function f() pure returns (uint) { return 1337; }
+==== Source: s2.sol ====
+import {f as g} from "s1.sol";
+function f() pure returns (uint) { return 6; }
+contract D {
+  function h() public pure returns (uint) {
+    return g() + f() * 10000;
+  }
+}
+// ====
+// compileViaYul: also
+// ----
+// h() -> 61337

test/libsolidity/semanticTests/multiSource/reimport_imported_function.sol

@@ -0,0 +1,15 @@
+==== Source: s1.sol ====
+function f() pure returns (uint) { return 1337; }
+==== Source: s2.sol ====
+import {f as g} from "s1.sol";
+==== Source: s3.sol ====
+import {g as h} from "s2.sol";
+contract C {
+  function foo() public pure returns (uint) {
+    return h();
+  }
+}
+// ====
+// compileViaYul: also
+// ----
+// foo() -> 1337

test/libsolidity/semanticTests/various/codebalance_assembly.sol

@@ -0,0 +1,28 @@
+contract C {
+    constructor() payable {}
+
+    function f() public returns (uint256 ret) {
+        assembly {
+            ret := balance(0)
+        }
+    }
+    function g() public returns (uint256 ret) {
+        assembly {
+            ret := balance(1)
+        }
+    }
+    function h() public returns (uint256 ret) {
+        assembly {
+            ret := balance(address())
+        }
+    }
+}
+
+// ====
+// EVMVersion: >=constantinople
+// compileViaYul: also
+// ----
+// constructor(), 23 wei ->
+// f() -> 0
+// g() -> 1
+// h() -> 23

test/libsolidity/semanticTests/various/codehash_assembly.sol

@@ -0,0 +1,25 @@
+contract C {
+    function f() public returns (bytes32 ret) {
+        assembly {
+            ret := extcodehash(0)
+        }
+    }
+    function g() public returns (bytes32 ret) {
+        assembly {
+            ret := extcodehash(1)
+        }
+    }
+    function h() public returns (bool ret) {
+        assembly {
+            ret := iszero(iszero(extcodehash(address())))
+        }
+    }
+}
+
+// ====
+// EVMVersion: >=constantinople
+// compileViaYul: also
+// ----
+// f() -> 0
+// g() -> 0xc5d2460186f7233c927e7db2dcc703c0e500b653ca82273b7bfad8045d85a470
+// h() -> true

test/libsolidity/smtCheckerTests/array_members/array_pop_length_1.sol

@@ -8,4 +8,4 @@ contract C {
 	}
 }
 // ----
-// Warning 2529: (82-89): Empty array "pop" detected here.
+// Warning 2529: (82-89): CHC: Empty array "pop" detected here.

test/libsolidity/smtCheckerTests/array_members/array_pop_length_2.sol

@@ -8,4 +8,4 @@ contract C {
 	}
 }
 // ----
-// Warning 2529: (82-89): Empty array "pop" detected here.
+// Warning 2529: (82-89): CHC: Empty array "pop" detected here.

test/libsolidity/smtCheckerTests/array_members/array_pop_length_3.sol

@@ -8,5 +8,5 @@ contract C {
 	}
 }
 // ----
-// Warning 2529: (82-89): Empty array "pop" detected here.
-// Warning 2529: (93-100): Empty array "pop" detected here.
+// Warning 2529: (82-89): CHC: Empty array "pop" detected here.
+// Warning 2529: (93-100): CHC: Empty array "pop" detected here.

test/libsolidity/smtCheckerTests/array_members/array_pop_length_4.sol

@@ -8,4 +8,4 @@ contract C {
 	}
 }
 // ----
-// Warning 2529: (94-101): Empty array "pop" detected here.
+// Warning 2529: (94-101): CHC: Empty array "pop" detected here.

test/libsolidity/smtCheckerTests/array_members/array_pop_length_5.sol

@@ -11,4 +11,4 @@ contract C {
 	}
 }
 // ----
-// Warning 2529: (122-129): Empty array "pop" detected here.
+// Warning 2529: (122-129): CHC: Empty array "pop" detected here.

test/libsolidity/smtCheckerTests/array_members/array_pop_length_6.sol

@@ -11,4 +11,4 @@ contract C {
 	}
 }
 // ----
-// Warning 2529: (127-134): Empty array "pop" detected here.
+// Warning 2529: (127-134): CHC: Empty array "pop" detected here.

test/libsolidity/smtCheckerTests/array_members/array_pop_length_8.sol

@@ -13,4 +13,4 @@ contract C {
 	}
 }
 // ----
-// Warning 2529: (82-89): Empty array "pop" detected here.
+// Warning 2529: (82-89): CHC: Empty array "pop" detected here.

test/libsolidity/smtCheckerTests/array_members/length_basic.sol

@@ -10,4 +10,4 @@ contract C {
 	}
 }
 // ----
-// Warning 6328: (153-176): Assertion violation happens here.
+// Warning 6328: (153-176): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment_2_fail.sol

@@ -14,6 +14,6 @@ contract C {
 	}
 }
 // ----
-// Warning 6328: (198-224): Assertion violation happens here.
-// Warning 6328: (228-254): Assertion violation happens here.
-// Warning 6328: (258-281): Assertion violation happens here.
+// Warning 6328: (198-224): CHC: Assertion violation happens here.
+// Warning 6328: (228-254): CHC: Assertion violation happens here.
+// Warning 6328: (258-281): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment_3_fail.sol

@@ -16,7 +16,7 @@ contract C {
 	}
 }
 // ----
-// Warning 6328: (222-248): Assertion violation happens here.
-// Warning 6328: (252-278): Assertion violation happens here.
-// Warning 6328: (282-305): Assertion violation happens here.
-// Warning 6328: (309-335): Assertion violation happens here.
+// Warning 6328: (222-248): CHC: Assertion violation happens here.
+// Warning 6328: (252-278): CHC: Assertion violation happens here.
+// Warning 6328: (282-305): CHC: Assertion violation happens here.
+// Warning 6328: (309-335): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/array_members/pop_1_unsafe.sol

@@ -7,4 +7,4 @@ contract C {
 	}
 }
 // ----
-// Warning 2529: (82-89): Empty array "pop" detected here.
+// Warning 2529: (82-89): CHC: Empty array "pop" detected here.

test/libsolidity/smtCheckerTests/array_members/pop_2d_unsafe.sol

@@ -9,4 +9,4 @@ contract C {
 	}
 }
 // ----
-// Warning 2529: (111-121): Empty array "pop" detected here.
+// Warning 2529: (111-121): CHC: Empty array "pop" detected here.

test/libsolidity/smtCheckerTests/array_members/pop_constructor_unsafe.sol

@@ -7,4 +7,4 @@ contract C {
 	}
 }
 // ----
-// Warning 2529: (76-83): Empty array "pop" detected here.
+// Warning 2529: (76-83): CHC: Empty array "pop" detected here.

test/libsolidity/smtCheckerTests/array_members/pop_loop_unsafe.sol

@@ -11,4 +11,4 @@ contract C {
 	}
 }
 // ----
-// Warning 2529: (150-157): Empty array "pop" detected here.
+// Warning 2529: (150-157): CHC: Empty array "pop" detected here.

test/libsolidity/smtCheckerTests/array_members/push_2d_arg_1_unsafe.sol

@@ -10,5 +10,5 @@ contract C {
 	}
 }
 // ----
-// Warning 3944: (162-177): Underflow (resulting value less than 0) happens here.
-// Warning 6328: (150-184): Assertion violation happens here.
+// Warning 3944: (162-177): CHC: Underflow (resulting value less than 0) happens here.
+// Warning 6328: (150-184): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/array_members/push_push_no_args_1_fail.sol

@@ -8,5 +8,5 @@ contract C {
 	}
 }
 // ----
-// Warning 6328: (113-139): Assertion violation happens here.
-// Warning 6328: (143-189): Assertion violation happens here.
+// Warning 6328: (113-139): CHC: Assertion violation happens here.
+// Warning 6328: (143-189): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/array_members/push_push_no_args_2_fail.sol

@@ -10,6 +10,6 @@ contract C {
 	}
 }
 // ----
-// Warning 6328: (122-148): Assertion violation happens here.
-// Warning 6328: (202-218): Assertion violation happens here.
-// Warning 6328: (222-278): Assertion violation happens here.
+// Warning 6328: (122-148): CHC: Assertion violation happens here.
+// Warning 6328: (202-218): CHC: Assertion violation happens here.
+// Warning 6328: (222-278): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/array_members/push_storage_ref_safe_aliasing.sol

@@ -12,5 +12,5 @@ contract C {
 	}
 }
 // ----
-// Warning 3944: (217-232): Underflow (resulting value less than 0) happens here.
-// Warning 6328: (205-239): Assertion violation happens here.
+// Warning 3944: (217-232): CHC: Underflow (resulting value less than 0) happens here.
+// Warning 6328: (205-239): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/array_members/push_storage_ref_unsafe_aliasing.sol

@@ -12,4 +12,4 @@ contract C {
 	}
 }
 // ----
-// Warning 6328: (167-188): Assertion violation happens here.
+// Warning 6328: (167-188): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/array_members/push_storage_ref_unsafe_length.sol

@@ -18,6 +18,6 @@ contract C {
 	}
 }
 // ----
-// Warning 6328: (193-217): Assertion violation happens here.
-// Warning 6328: (309-333): Assertion violation happens here.
-// Warning 6328: (419-436): Assertion violation happens here.
+// Warning 6328: (193-217): CHC: Assertion violation happens here.
+// Warning 6328: (309-333): CHC: Assertion violation happens here.
+// Warning 6328: (419-436): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/array_members/push_zero_2d_unsafe.sol

@@ -9,4 +9,4 @@ contract C {
 	}
 }
 // ----
-// Warning 6328: (111-144): Assertion violation happens here.
+// Warning 6328: (111-144): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/array_members/push_zero_unsafe.sol

@@ -8,4 +8,4 @@ contract C {
 	}
 }
 // ----
-// Warning 6328: (94-124): Assertion violation happens here.
+// Warning 6328: (94-124): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/array_members/storage_pointer_push_1.sol

@@ -15,4 +15,4 @@ contract C {
 	}
 }
 // ----
-// Warning 6328: (184-213): Assertion violation happens here.
+// Warning 6328: (184-213): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/complex/slither/const_state_variables.sol

@@ -53,4 +53,4 @@ contract MyConc{
 // ----
 // Warning 2519: (773-792): This declaration shadows an existing declaration.
 // Warning 2018: (1009-1086): Function state mutability can be restricted to view
-// Warning 4984: (985-1002): Overflow (resulting value larger than 2**256 - 1) happens here.
+// Warning 4984: (985-1002): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.

test/libsolidity/smtCheckerTests/control_flow/require.sol

@@ -30,4 +30,4 @@ contract C {
 	}
 }
 // ----
-// Warning 6328: (448-465): Assertion violation happens here.
+// Warning 6328: (448-465): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/control_flow/revert.sol

@@ -32,4 +32,4 @@ contract C {
 // ----
 // Warning 5740: (116-129): Unreachable code.
 // Warning 5740: (221-234): Unreachable code.
-// Warning 6328: (427-444): Assertion violation happens here.
+// Warning 6328: (427-444): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/control_flow/revert_complex_flow.sol

@@ -14,5 +14,5 @@ contract C {
 	}
 }
 // ----
-// Warning 6328: (183-197): Assertion violation happens here.
-// Warning 6838: (155-156): Condition is always false.
+// Warning 6328: (183-197): CHC: Assertion violation happens here.
+// Warning 6838: (155-156): BMC: Condition is always false.

test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_fail.sol

@@ -15,4 +15,4 @@ contract c {
 	}
 }
 // ----
-// Warning 6328: (227-236): Assertion violation happens here.
+// Warning 6328: (227-236): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_inside_branch.sol

@@ -17,5 +17,5 @@ contract c {
 	}
 }
 // ----
-// Warning 6328: (202-218): Assertion violation happens here.
-// Warning 6328: (242-252): Assertion violation happens here.
+// Warning 6328: (202-218): CHC: Assertion violation happens here.
+// Warning 6328: (242-252): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_need_both_fail.sol

@@ -15,4 +15,4 @@ contract c {
 	}
 }
 // ----
-// Warning 6328: (225-235): Assertion violation happens here.
+// Warning 6328: (225-235): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_touched.sol

@@ -12,8 +12,8 @@ contract C
 	}
 }
 // ----
-// Warning 6838: (84-110): Condition is always false.
-// Warning 6838: (121-147): Condition is always true.
-// Warning 6838: (158-183): Condition is always false.
-// Warning 6838: (194-221): Condition is always false.
-// Warning 6838: (232-247): Condition is always true.
+// Warning 6838: (84-110): BMC: Condition is always false.
+// Warning 6838: (121-147): BMC: Condition is always true.
+// Warning 6838: (158-183): BMC: Condition is always false.
+// Warning 6838: (194-221): BMC: Condition is always false.
+// Warning 6838: (232-247): BMC: Condition is always true.

test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_touched_function.sol

@@ -16,8 +16,8 @@ contract C
 	}
 }
 // ----
-// Warning 6838: (156-179): Condition is always false.
-// Warning 6838: (190-213): Condition is always true.
-// Warning 6838: (224-243): Condition is always false.
-// Warning 6838: (254-277): Condition is always false.
-// Warning 6838: (288-300): Condition is always true.
+// Warning 6838: (156-179): BMC: Condition is always false.
+// Warning 6838: (190-213): BMC: Condition is always true.
+// Warning 6838: (224-243): BMC: Condition is always false.
+// Warning 6838: (254-277): BMC: Condition is always false.
+// Warning 6838: (288-300): BMC: Condition is always true.

test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_fail.sol

@@ -15,4 +15,4 @@ contract c {
 	}
 }
 // ----
-// Warning 6328: (225-235): Assertion violation happens here.
+// Warning 6328: (225-235): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_inside_branch.sol

@@ -24,4 +24,4 @@ contract c {
 	}
 }
 // ----
-// Warning 6328: (360-370): Assertion violation happens here.
+// Warning 6328: (360-370): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_need_both_fail.sol

@@ -15,4 +15,4 @@ contract c {
 	}
 }
 // ----
-// Warning 6328: (225-235): Assertion violation happens here.
+// Warning 6328: (225-235): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_touched.sol

@@ -12,8 +12,8 @@ contract C
 	}
 }
 // ----
-// Warning 6838: (84-110): Condition is always true.
-// Warning 6838: (121-147): Condition is always true.
-// Warning 6838: (158-183): Condition is always true.
-// Warning 6838: (194-221): Condition is always true.
-// Warning 6838: (232-248): Condition is always false.
+// Warning 6838: (84-110): BMC: Condition is always true.
+// Warning 6838: (121-147): BMC: Condition is always true.
+// Warning 6838: (158-183): BMC: Condition is always true.
+// Warning 6838: (194-221): BMC: Condition is always true.
+// Warning 6838: (232-248): BMC: Condition is always false.

test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_touched_function.sol

@@ -16,8 +16,8 @@ contract C
 	}
 }
 // ----
-// Warning 6838: (156-179): Condition is always true.
-// Warning 6838: (190-213): Condition is always true.
-// Warning 6838: (224-243): Condition is always true.
-// Warning 6838: (254-277): Condition is always true.
-// Warning 6838: (288-301): Condition is always false.
+// Warning 6838: (156-179): BMC: Condition is always true.
+// Warning 6838: (190-213): BMC: Condition is always true.
+// Warning 6838: (224-243): BMC: Condition is always true.
+// Warning 6838: (254-277): BMC: Condition is always true.
+// Warning 6838: (288-301): BMC: Condition is always false.

test/libsolidity/smtCheckerTests/control_flow/ways_to_merge_variables_1.sol

@@ -9,4 +9,4 @@ contract C {
     }
 }
 // ----
-// Warning 6328: (159-173): Assertion violation happens here.
+// Warning 6328: (159-173): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/control_flow/ways_to_merge_variables_2.sol

@@ -9,4 +9,4 @@ contract C {
     }
 }
 // ----
-// Warning 6328: (159-173): Assertion violation happens here.
+// Warning 6328: (159-173): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/control_flow/ways_to_merge_variables_3.sol

@@ -9,4 +9,4 @@ contract C {
     }
 }
 // ----
-// Warning 6328: (161-175): Assertion violation happens here.
+// Warning 6328: (161-175): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/external_calls/external.sol

@@ -17,4 +17,4 @@ contract C {
 	}
 }
 // ----
-// Warning 6328: (200-214): Assertion violation happens here.
+// Warning 6328: (200-214): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/external_calls/external_hash.sol

@@ -26,4 +26,4 @@ contract C {
 	}
 }
 // ----
-// Warning 6328: (423-445): Assertion violation happens here.
+// Warning 6328: (423-445): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_pure.sol

@@ -28,4 +28,4 @@ contract C {
 	}
 }
 // ----
-// Warning 6328: (431-453): Assertion violation happens here.
+// Warning 6328: (431-453): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state.sol

@@ -34,4 +34,4 @@ contract C {
 	}
 }
 // ----
-// Warning 6328: (528-565): Assertion violation happens here.
+// Warning 6328: (528-565): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy.sol

@@ -29,4 +29,4 @@ contract C {
 	}
 }
 // ----
-// Warning 6328: (299-313): Assertion violation happens here.
+// Warning 6328: (299-313): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_indirect.sol

@@ -42,5 +42,5 @@ contract C {
 	}
 }
 // ----
-// Warning 6328: (452-466): Assertion violation happens here.
-// Warning 6328: (470-496): Assertion violation happens here.
+// Warning 6328: (452-466): CHC: Assertion violation happens here.
+// Warning 6328: (470-496): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_unsafe.sol

@@ -34,5 +34,5 @@ contract C {
 	}
 }
 // ----
-// Warning 6328: (381-395): Assertion violation happens here.
-// Warning 6328: (399-425): Assertion violation happens here.
+// Warning 6328: (381-395): CHC: Assertion violation happens here.
+// Warning 6328: (399-425): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_unsafe.sol

@@ -38,5 +38,5 @@ contract C {
 	}
 }
 // ----
-// Warning 6328: (435-461): Assertion violation happens here.
-// Warning 6328: (594-631): Assertion violation happens here.
+// Warning 6328: (435-461): CHC: Assertion violation happens here.
+// Warning 6328: (594-631): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/external_calls/external_inc.sol

@@ -18,5 +18,5 @@ contract C {
 	}
 }
 // ----
-// Warning 6328: (189-203): Assertion violation happens here.
-// Warning 2661: (146-149): Overflow (resulting value larger than 2**256 - 1) happens here.
+// Warning 6328: (189-203): CHC: Assertion violation happens here.
+// Warning 2661: (146-149): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.

test/libsolidity/smtCheckerTests/external_calls/external_inc1_inc2.sol

@@ -25,4 +25,4 @@ contract C {
 	}
 }
 // ----
-// Warning 6328: (286-303): Assertion violation happens here.
+// Warning 6328: (286-303): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/external_calls/external_single_inc.sol

@@ -23,4 +23,4 @@ contract C {
 	}
 }
 // ----
-// Warning 6328: (256-273): Assertion violation happens here.
+// Warning 6328: (256-273): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/external_calls/mutex_f_no_guard.sol

@@ -27,4 +27,4 @@ contract C {
 	}
 }
 // ----
-// Warning 6328: (307-321): Assertion violation happens here.
+// Warning 6328: (307-321): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy.sol

@@ -13,4 +13,4 @@ contract A is C {
 	}
 }
 // ----
-// Warning 6328: (152-166): Assertion violation happens here.
+// Warning 6328: (152-166): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_2.sol

@@ -4,4 +4,4 @@ contract A is C { constructor() C(2) { assert(a == 2); } }
 contract B is C { constructor() C(3) { assert(a == 3); } }
 contract J is C { constructor() C(3) { assert(a == 4); } }
 // ----
-// Warning 6328: (243-257): Assertion violation happens here.
+// Warning 6328: (243-257): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_3.sol

@@ -19,6 +19,6 @@ contract A is B {
 	}
 }
 // ----
-// Warning 4984: (203-208): Overflow (resulting value larger than 2**256 - 1) happens here.
-// Warning 4984: (244-249): Overflow (resulting value larger than 2**256 - 1) happens here.
-// Warning 6328: (232-250): Assertion violation happens here.
+// Warning 4984: (203-208): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
+// Warning 4984: (244-249): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
+// Warning 6328: (232-250): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_4.sol

@@ -18,6 +18,6 @@ contract A is B {
 	}
 }
 // ----
-// Warning 4984: (198-203): Overflow (resulting value larger than 2**256 - 1) happens here.
-// Warning 4984: (207-212): Overflow (resulting value larger than 2**256 - 1) happens here.
-// Warning 4984: (230-235): Overflow (resulting value larger than 2**256 - 1) happens here.
+// Warning 4984: (198-203): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
+// Warning 4984: (207-212): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
+// Warning 4984: (230-235): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond.sol

@@ -25,6 +25,6 @@ contract A is B2, B1 {
 	}
 }
 // ----
-// Warning 4984: (200-205): Overflow (resulting value larger than 2**256 - 1) happens here.
-// Warning 4984: (314-319): Overflow (resulting value larger than 2**256 - 1) happens here.
-// Warning 6328: (302-320): Assertion violation happens here.
+// Warning 4984: (200-205): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
+// Warning 4984: (314-319): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
+// Warning 6328: (302-320): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond_2.sol

@@ -25,6 +25,6 @@ contract A is B2, B1 {
 	}
 }
 // ----
-// Warning 4984: (200-205): Overflow (resulting value larger than 2**256 - 1) happens here.
-// Warning 4984: (314-319): Overflow (resulting value larger than 2**256 - 1) happens here.
-// Warning 6328: (302-320): Assertion violation happens here.
+// Warning 4984: (200-205): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
+// Warning 4984: (314-319): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
+// Warning 6328: (302-320): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond_3.sol

@@ -27,7 +27,7 @@ contract A is B2, B1 {
 	}
 }
 // ----
-// Warning 4984: (160-165): Overflow (resulting value larger than 2**256 - 1) happens here.
-// Warning 4984: (225-230): Overflow (resulting value larger than 2**256 - 1) happens here.
-// Warning 4984: (241-246): Overflow (resulting value larger than 2**256 - 1) happens here.
-// Warning 6328: (334-350): Assertion violation happens here.
+// Warning 4984: (160-165): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
+// Warning 4984: (225-230): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
+// Warning 4984: (241-246): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
+// Warning 6328: (334-350): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond_empty_middle.sol

@@ -20,4 +20,4 @@ contract A is B, B2 {
 }
 // ----
 // Warning 5667: (164-170): Unused function parameter. Remove or comment out the variable name to silence this warning.
-// Warning 6328: (194-208): Assertion violation happens here.
+// Warning 6328: (194-208): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_empty_chain.sol

@@ -19,4 +19,4 @@ contract A is B {
 }
 // ----
 // Warning 5667: (194-200): Unused function parameter. Remove or comment out the variable name to silence this warning.
-// Warning 6328: (224-238): Assertion violation happens here.
+// Warning 6328: (224-238): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_empty_middle.sol

@@ -17,4 +17,4 @@ contract A is B {
 }
 // ----
 // Warning 5667: (138-144): Unused function parameter. Remove or comment out the variable name to silence this warning.
-// Warning 6328: (172-186): Assertion violation happens here.
+// Warning 6328: (172-186): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_empty_middle_no_invocation.sol

@@ -16,4 +16,4 @@ contract A is B {
 }
 // ----
 // Warning 5667: (138-144): Unused function parameter. Remove or comment out the variable name to silence this warning.
-// Warning 6328: (150-164): Assertion violation happens here.
+// Warning 6328: (150-164): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_mixed_chain.sol

@@ -27,4 +27,4 @@ contract A is B {
 }
 // ----
 // Warning 5667: (254-260): Unused function parameter. Remove or comment out the variable name to silence this warning.
-// Warning 6328: (284-298): Assertion violation happens here.
+// Warning 6328: (284-298): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_mixed_chain_local_vars.sol

@@ -32,4 +32,4 @@ contract A is B {
 }
 // ----
 // Warning 5667: (296-302): Unused function parameter. Remove or comment out the variable name to silence this warning.
-// Warning 6328: (357-372): Assertion violation happens here.
+// Warning 6328: (357-372): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_mixed_chain_with_params.sol

@@ -25,5 +25,5 @@ contract A is B {
 	}
 }
 // ----
-// Warning 4984: (247-252): Overflow (resulting value larger than 2**256 - 1) happens here.
-// Warning 6328: (328-342): Assertion violation happens here.
+// Warning 4984: (247-252): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
+// Warning 6328: (328-342): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_mixed_chain_with_params_2.sol

@@ -23,4 +23,4 @@ contract B is C {
 contract A is B {
 }
 // ----
-// Warning 6328: (266-280): Assertion violation happens here.
+// Warning 6328: (266-280): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_modifier.sol

@@ -14,4 +14,4 @@ contract A is C {
 	}
 }
 // ----
-// Warning 6328: (188-202): Assertion violation happens here.
+// Warning 6328: (188-202): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_same_var.sol

@@ -13,5 +13,5 @@ contract A is C {
 	}
 }
 // ----
-// Warning 6328: (134-148): Assertion violation happens here.
-// Warning 6328: (152-168): Assertion violation happens here.
+// Warning 6328: (134-148): CHC: Assertion violation happens here.
+// Warning 6328: (152-168): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/functions/constructor_simple.sol

@@ -13,4 +13,4 @@ contract C {
 	}
 }
 // ----
-// Warning 6328: (141-155): Assertion violation happens here.
+// Warning 6328: (141-155): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/functions/constructor_state_value.sol

@@ -13,4 +13,4 @@ contract C {
 	}
 }
 // ----
-// Warning 6328: (145-159): Assertion violation happens here.
+// Warning 6328: (145-159): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/functions/constructor_state_value_inherited.sol

@@ -15,4 +15,4 @@ contract C is B {
 	}
 }
 // ----
-// Warning 6328: (165-179): Assertion violation happens here.
+// Warning 6328: (165-179): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/functions/constructor_state_value_parameter.sol

@@ -13,5 +13,5 @@ contract C {
 	}
 }
 // ----
-// Warning 4984: (115-120): Overflow (resulting value larger than 2**256 - 1) happens here.
-// Warning 6328: (162-176): Assertion violation happens here.
+// Warning 4984: (115-120): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
+// Warning 6328: (162-176): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/functions/function_call_state_var_init.sol

@@ -9,4 +9,4 @@ contract C {
 	}
 }
 // ----
-// Warning 6328: (116-132): Assertion violation happens here.
+// Warning 6328: (116-132): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/functions/function_inside_branch_modify_state_var.sol

@@ -16,4 +16,4 @@ contract C
 	}
 }
 // ----
-// Warning 6328: (209-223): Assertion violation happens here.
+// Warning 6328: (209-223): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/functions/function_inside_branch_modify_state_var_3.sol

@@ -24,5 +24,5 @@ contract C
 
 }
 // ----
-// Warning 6328: (209-223): Assertion violation happens here.
-// Warning 6328: (321-335): Assertion violation happens here.
+// Warning 6328: (209-223): CHC: Assertion violation happens here.
+// Warning 6328: (321-335): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/functions/functions_bound_1_fail.sol

@@ -18,4 +18,4 @@ contract C
 	}
 }
 // ----
-// Warning 6328: (261-277): Assertion violation happens here.
+// Warning 6328: (261-277): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/functions/functions_external_2.sol

@@ -17,5 +17,4 @@ contract C
 	}
 }
 // ----
-// Warning 1218: (297-321): Error trying to invoke SMT solver.
-// Warning 4661: (297-321): Assertion violation happens here.
+// Warning 4661: (297-321): BMC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/functions/functions_external_4.sol

@@ -16,4 +16,4 @@ contract D
 	}
 }
 // ----
-// Warning 6328: (191-206): Assertion violation happens here.
+// Warning 6328: (191-206): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/functions/functions_identity_1_fail.sol

@@ -12,4 +12,4 @@ contract C
 }
 
 // ----
-// Warning 6328: (161-174): Assertion violation happens here.
+// Warning 6328: (161-174): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/functions/functions_identity_2_fail.sol

@@ -16,4 +16,4 @@ contract C
 }
 
 // ----
-// Warning 6328: (229-242): Assertion violation happens here.
+// Warning 6328: (229-242): CHC: Assertion violation happens here.