Merge branch 'develop' into develop_060

.circleci/config.yml

@@ -431,12 +431,12 @@ jobs:
       - checkout
       - restore_cache:
           keys:
-            - dependencies-osx-{{ .Branch }}-{{ checksum ".circleci/config.yml" }}
+            - dependencies-osx-{{ .Branch }}-{{ checksum ".circleci/config.yml" }}-{{ checksum ".circleci/osx_install_dependencies.sh" }}
       - run:
           name: Install build dependencies
           command: ./.circleci/osx_install_dependencies.sh
       - save_cache:
-          key: dependencies-osx-{{ .Branch }}-{{ checksum ".circleci/config.yml" }}
+          key: dependencies-osx-{{ .Branch }}-{{ checksum ".circleci/config.yml" }}-{{ checksum ".circleci/osx_install_dependencies.sh" }}
           paths:
             - /usr/local/bin
             - /usr/local/sbin
@@ -459,7 +459,7 @@ jobs:
       - checkout
       - restore_cache:
           keys:
-            - dependencies-osx-{{ .Branch }}-{{ checksum ".circleci/config.yml" }}
+            - dependencies-osx-{{ .Branch }}-{{ checksum ".circleci/config.yml" }}-{{ checksum ".circleci/osx_install_dependencies.sh" }}
       - attach_workspace:
           at: build
       - run: *run_soltest
@@ -475,7 +475,7 @@ jobs:
       - checkout
       - restore_cache:
           keys:
-            - dependencies-osx-{{ .Branch }}-{{ checksum ".circleci/config.yml" }}
+            - dependencies-osx-{{ .Branch }}-{{ checksum ".circleci/config.yml" }}-{{ checksum ".circleci/osx_install_dependencies.sh" }}
       - attach_workspace:
           at: build
       - run: *run_cmdline_tests

.circleci/docker/Dockerfile.clang.ubuntu1904

@@ -62,7 +62,7 @@ RUN git clone --recursive -b boost-1.69.0 https://github.com/boostorg/boost.git
     rm -rf /usr/src/boost
 
 # Z3
-RUN git clone --depth 1 -b Z3-4.8.5 https://github.com/Z3Prover/z3.git \
+RUN git clone --depth 1 -b z3-4.8.6 https://github.com/Z3Prover/z3.git \
     /usr/src/z3; \
     cd /usr/src/z3; \
     python scripts/mk_make.py --prefix=/usr ; \

.circleci/osx_install_dependencies.sh

@@ -43,13 +43,13 @@ then
   ./scripts/install_obsolete_jsoncpp_1_7_4.sh
 
   # z3
-  wget https://github.com/Z3Prover/z3/releases/download/Z3-4.8.5/z3-4.8.5-x64-osx-10.14.2.zip
+  wget https://github.com/Z3Prover/z3/releases/download/z3-4.8.6/z3-4.8.6-x64-osx-10.14.6.zip
-  unzip z3-4.8.5-x64-osx-10.14.2.zip
+  unzip z3-4.8.6-x64-osx-10.14.6.zip
-  rm -f z3-4.8.5-x64-osx-10.14.2.zip
+  rm -f z3-4.8.6-x64-osx-10.14.6.zip
-  cp z3-4.8.5-x64-osx-10.14.2/bin/libz3.a /usr/local/lib
+  cp z3-4.8.6-x64-osx-10.14.6/bin/libz3.a /usr/local/lib
-  cp z3-4.8.5-x64-osx-10.14.2/bin/z3 /usr/local/bin
+  cp z3-4.8.6-x64-osx-10.14.6/bin/z3 /usr/local/bin
-  cp z3-4.8.5-x64-osx-10.14.2/include/* /usr/local/include
+  cp z3-4.8.6-x64-osx-10.14.6/include/* /usr/local/include
-  rm -rf z3-4.8.5-x64-osx-10.14.2
+  rm -rf z3-4.8.6-x64-osx-10.14.6
 
   # evmone
   wget https://github.com/ethereum/evmone/releases/download/v0.1.0/evmone-0.1.0-darwin-x86_64.tar.gz

liblangutil/Exceptions.cpp

@@ -29,7 +29,7 @@ using namespace langutil;
 Error::Error(Type _type, SourceLocation const& _location, string const& _description):
 	m_type(_type)
 {
-	switch(m_type)
+	switch (m_type)
 	{
 	case Type::DeclarationError:
 		m_typeName = "DeclarationError";

libsolidity/analysis/ControlFlowBuilder.cpp

@@ -49,7 +49,7 @@ bool ControlFlowBuilder::visit(BinaryOperation const& _operation)
 {
 	solAssert(!!m_currentNode, "");
 
-	switch(_operation.getOperator())
+	switch (_operation.getOperator())
 	{
 		case Token::Or:
 		case Token::And:

libsolidity/analysis/ReferencesResolver.cpp

@@ -126,7 +126,7 @@ bool ReferencesResolver::visit(ElementaryTypeName const& _typeName)
 		{
 			// for non-address types this was already caught by the parser
 			solAssert(_typeName.annotation().type->category() == Type::Category::Address, "");
-			switch(*_typeName.stateMutability())
+			switch (*_typeName.stateMutability())
 			{
 				case StateMutability::Payable:
 					_typeName.annotation().type = TypeProvider::payableAddress();

libsolidity/analysis/StaticAnalyzer.cpp

@@ -229,7 +229,7 @@ bool StaticAnalyzer::visit(MemberAccess const& _memberAccess)
 	if (m_constructor)
 	{
 		auto const* expr = &_memberAccess.expression();
-		while(expr)
+		while (expr)
 		{
 			if (auto id = dynamic_cast<Identifier const*>(expr))
 			{

libsolidity/ast/AST.h

@@ -187,7 +187,7 @@ public:
 
 	static std::string visibilityToString(Declaration::Visibility _visibility)
 	{
-		switch(_visibility)
+		switch (_visibility)
 		{
 		case Declaration::Visibility::Public:
 			return "public";

libsolidity/ast/ASTEnums.h

@@ -36,7 +36,7 @@ enum class StateMutability { Pure, View, NonPayable, Payable };
 
 inline std::string stateMutabilityToString(StateMutability const& _stateMutability)
 {
-	switch(_stateMutability)
+	switch (_stateMutability)
 	{
 	case StateMutability::Pure:
 		return "pure";

libsolidity/ast/Types.cpp

@@ -663,7 +663,7 @@ BoolResult FixedPointType::isExplicitlyConvertibleTo(Type const& _convertTo) con
 
 TypeResult FixedPointType::unaryOperatorResult(Token _operator) const
 {
-	switch(_operator)
+	switch (_operator)
 	{
 	case Token::Delete:
 		// "delete" is ok for all fixed types
@@ -2881,7 +2881,7 @@ unsigned FunctionType::sizeOnStack() const
 
 	unsigned size = 0;
 
-	switch(kind)
+	switch (kind)
 	{
 	case Kind::External:
 	case Kind::DelegateCall:

libsolidity/parsing/Parser.cpp

@@ -254,7 +254,7 @@ std::pair<ContractDefinition::ContractKind, bool> Parser::parseContractKind()
 		abstract = true;
 		m_scanner->next();
 	}
-	switch(m_scanner->currentToken())
+	switch (m_scanner->currentToken())
 	{
 	case Token::Interface:
 		kind = ContractDefinition::ContractKind::Interface;
@@ -436,7 +436,7 @@ StateMutability Parser::parseStateMutability()
 {
 	StateMutability stateMutability(StateMutability::NonPayable);
 	Token token = m_scanner->currentToken();
-	switch(token)
+	switch (token)
 	{
 		case Token::Payable:
 			stateMutability = StateMutability::Payable;

libyul/Utilities.cpp

@@ -113,7 +113,7 @@ u256 yul::valueOfBoolLiteral(Literal const& _literal)
 
 u256 yul::valueOfLiteral(Literal const& _literal)
 {
-	switch(_literal.kind)
+	switch (_literal.kind)
 	{
 		case LiteralKind::Number:
 			return valueOfNumberLiteral(_literal);

scripts/check_style.sh

@@ -17,7 +17,7 @@ fi
 
 FORMATERROR=$(
 (
-	git grep -nIE "\<(if|for)\(" -- '*.h' '*.cpp' # no space after "if" or "for"
+	git grep -nIE "\<(if|for|while|switch)\(" -- '*.h' '*.cpp' # no space after "if", "for", "while" or "switch"
 	git grep -nIE "\<for\>\s*\([^=]*\>\s:\s.*\)" -- '*.h' '*.cpp' # no space before range based for-loop
 	git grep -nIE "\<if\>\s*\(.*\)\s*\{\s*$" -- '*.h' '*.cpp' # "{\n" on same line as "if" / "for"
 	git grep -nIE "[,\(<]\s*const " -- '*.h' '*.cpp' # const on left side of type

scripts/deps-ppa/static_z3.sh

@@ -25,9 +25,9 @@ set -ev
 keyid=70D110489D66E2F6
 email=builds@ethereum.org
 packagename=libz3-static-dev
-version=4.8.5
+version=4.8.6
 
-DISTRIBUTIONS="bionic disco"
+DISTRIBUTIONS="bionic disco eoan"
 
 for distribution in $DISTRIBUTIONS
 do
@@ -40,7 +40,7 @@ pparepo=cpp-build-deps
 ppafilesurl=https://launchpad.net/~ethereum/+archive/ubuntu/${pparepo}/+files
 
 # Fetch source
-git clone --depth 1 --branch Z3-${version} https://github.com/Z3Prover/z3.git
+git clone --depth 1 --branch z3-${version} https://github.com/Z3Prover/z3.git
 cd z3
 debversion="$version"
 

scripts/release_ppa.sh

@@ -57,7 +57,7 @@ packagename=solc
 
 static_build_distribution=disco
 
-DISTRIBUTIONS="bionic disco"
+DISTRIBUTIONS="bionic disco eoan"
 
 if is_release
 then

test/libsolidity/smtCheckerTests/invariants/loop_array_for.sol

@@ -7,10 +7,11 @@ contract Simple {
 		for (i = 0; i < n; ++i)
 			a[i] = i;
 		require(n > 1);
-		// Assertion is safe but current solver version cannot solve it.
+		// Assertion is safe but current solver version times out.
 		// Keep test for next solver release.
 		assert(a[n-1] > a[n-2]);
 	}
 }
 // ----
-// Warning: (267-290): Assertion violation happens here
+// Warning: (261-284): Error trying to invoke SMT solver.
+// Warning: (261-284): Assertion violation happens here

test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_memory.sol

@@ -1,23 +0,0 @@
-pragma experimental SMTChecker;
-
-contract LoopFor2 {
-	uint[] b;
-	uint[] c;
-
-	function testUnboundedForLoop(uint n) public {
-		b[0] = 900;
-		uint[] memory a = b;
-		require(n > 0 && n < 100);
-		uint i;
-		while (i < n) {
-			b[i] = i + 1;
-			c[i] = b[i];
-			++i;
-		}
-		assert(b[0] == c[0]);
-		assert(a[0] == 900);
-		assert(b[0] == 900);
-	}
-}
-// ----
-// Warning: (312-331): Assertion violation happens here

test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_storage.sol

@@ -14,11 +14,13 @@ contract LoopFor2 {
 			c[i] = b[i];
 			++i;
 		}
+		// Fails as false positive.
 		assert(b[0] == c[0]);
 		assert(a[0] == 900);
 		assert(b[0] == 900);
 	}
 }
 // ----
-// Warning: (290-309): Assertion violation happens here
+// Warning: (296-316): Assertion violation happens here
-// Warning: (313-332): Assertion violation happens here
+// Warning: (320-339): Assertion violation happens here
+// Warning: (343-362): Assertion violation happens here