Merge commit 'a7d481fb9' into develop_060

.circleci/config.yml

@@ -476,7 +476,7 @@ jobs:
 
   b_ems:
     docker:
-      - image: trzeci/emscripten:sdk-tag-1.38.22-64bit
+      - image: trzeci/emscripten:sdk-tag-1.39.3-64bit
     environment:
       TERM: xterm
     steps:

.travis.yml

@@ -110,7 +110,7 @@ matrix:
           before_install:
               - nvm install 8
               - nvm use 8
-              - docker pull trzeci/emscripten:sdk-tag-1.38.22-64bit
+              - docker pull trzeci/emscripten:sdk-tag-1.39.3-64bit
           env:
               - SOLC_EMSCRIPTEN=On
               - SOLC_INSTALL_DEPS_TRAVIS=Off
@@ -127,7 +127,7 @@ matrix:
               #
               # This key here has no significant on anything, apart from caching. Please keep
               # it in sync with the version above.
-              - EMSCRIPTEN_VERSION_KEY="1.38.22"
+              - EMSCRIPTEN_VERSION_KEY="1.39.3"
 
         # OS X Mavericks (10.9)
         # https://en.wikipedia.org/wiki/OS_X_Mavericks

Changelog.md

@@ -46,12 +46,18 @@ Language Features:
 
 
 Compiler Features:
+ * SMTChecker: Add support to constructors including constructor inheritance.
  * Yul: When compiling via Yul, string literals from the Solidity code are kept as string literals if every character is safely printable.
  * Yul Optimizer: Perform loop-invariant code motion.
 
 
+Build System:
+ * Update to emscripten version 1.39.3.
+
+
 Bugfixes:
  * SMTChecker: Fix internal error when using ``abi.decode``.
+ * SMTChecker: Fix internal error when using arrays or mappings of functions.
 
 
 

cmake/EthCompilerSettings.cmake

@@ -86,7 +86,7 @@ if (("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU") OR ("${CMAKE_CXX_COMPILER_ID}" MA
 		elseif(EMSCRIPTEN)
 			set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} --memory-init-file 0")
 			# Leave only exported symbols as public and aggressively remove others
-			set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -fdata-sections -ffunction-sections -Wl,--gc-sections -fvisibility=hidden")
+			set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -fdata-sections -ffunction-sections -fvisibility=hidden")
 			# Optimisation level
 			set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -O3")
 			# Re-enable exception catching (optimisations above -O1 disable it)
@@ -110,9 +110,12 @@ if (("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU") OR ("${CMAKE_CXX_COMPILER_ID}" MA
 			set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -s STRICT=1")
 			# Export the Emscripten-generated auxiliary methods which are needed by solc-js.
 			# Which methods of libsolc itself are exported is specified in libsolc/CMakeLists.txt.
-			set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -s EXTRA_EXPORTED_RUNTIME_METHODS=['cwrap','addFunction','removeFunction','Pointer_stringify','lengthBytesUTF8','_malloc','stringToUTF8','setValue']")
+			set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -s EXTRA_EXPORTED_RUNTIME_METHODS=['cwrap','addFunction','removeFunction','UTF8ToString','lengthBytesUTF8','_malloc','stringToUTF8','setValue']")
 			# Do not build as a WebAssembly target - we need an asm.js output.
 			set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -s WASM=0")
+
+			# Disable warnings about not being pure asm.js due to memory growth.
+			set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wno-almost-asm")
 		endif()
 	endif()
 

cmake/jsoncpp.cmake

@@ -37,9 +37,9 @@ endif()
 ExternalProject_Add(jsoncpp-project
     PREFIX "${prefix}"
     DOWNLOAD_DIR "${CMAKE_SOURCE_DIR}/deps/downloads"
-    DOWNLOAD_NAME jsoncpp-1.8.4.tar.gz
+    DOWNLOAD_NAME jsoncpp-1.9.2.tar.gz
-    URL https://github.com/open-source-parsers/jsoncpp/archive/1.8.4.tar.gz
+    URL https://github.com/open-source-parsers/jsoncpp/archive/1.9.2.tar.gz
-    URL_HASH SHA256=c49deac9e0933bcb7044f08516861a2d560988540b23de2ac1ad443b219afdb6
+    URL_HASH SHA256=77a402fb577b2e0e5d0bdc1cf9c65278915cdb25171e3452c68b6da8a561f8f0
     CMAKE_COMMAND ${JSONCPP_CMAKE_COMMAND}
     CMAKE_ARGS -DCMAKE_INSTALL_PREFIX=<INSTALL_DIR>
                -DCMAKE_CXX_COMPILER=${CMAKE_CXX_COMPILER}

libdevcore/CommonData.cpp

@@ -179,11 +179,10 @@ bool dev::isValidDecimal(string const& _string)
 	return true;
 }
 
-// Returns a quoted string if all characters are printable ASCII chars,
+string dev::formatAsStringOrNumber(string const& _value)
-// or its hex representation otherwise.
-std::string dev::formatAsStringOrNumber(std::string const& _value)
 {
-	if (_value.length() <= 32)
+	assertThrow(_value.length() <= 32, StringTooLong, "String to be formatted longer than 32 bytes.");
+
 	for (auto const& c: _value)
 		if (c <= 0x1f || c >= 0x7f || c == '"')
 			return "0x" + h256(_value, h256::AlignLeft).hex();

libdevcore/CommonData.h

@@ -401,6 +401,7 @@ bool isValidDecimal(std::string const& _string);
 
 /// @returns a quoted string if all characters are printable ASCII chars,
 /// or its hex representation otherwise.
+/// _value cannot be longer than 32 bytes.
 std::string formatAsStringOrNumber(std::string const& _value);
 
 template<typename Container, typename Compare>

libdevcore/Exceptions.h

@@ -49,6 +49,7 @@ DEV_SIMPLE_EXCEPTION(BadHexCharacter);
 DEV_SIMPLE_EXCEPTION(BadHexCase);
 DEV_SIMPLE_EXCEPTION(FileError);
 DEV_SIMPLE_EXCEPTION(DataTooLong);
+DEV_SIMPLE_EXCEPTION(StringTooLong);
 
 // error information to be added to exceptions
 using errinfo_comment = boost::error_info<struct tag_comment, std::string>;

libdevcore/JSON.cpp

@@ -32,8 +32,8 @@
 using namespace std;
 
 static_assert(
-	(JSONCPP_VERSION_MAJOR == 1) && (JSONCPP_VERSION_MINOR == 8) && (JSONCPP_VERSION_PATCH == 4),
+	(JSONCPP_VERSION_MAJOR == 1) && (JSONCPP_VERSION_MINOR == 9) && (JSONCPP_VERSION_PATCH == 2),
-	"Unexpected jsoncpp version: " JSONCPP_VERSION_STRING ". Expecting 1.8.4."
+	"Unexpected jsoncpp version: " JSONCPP_VERSION_STRING ". Expecting 1.9.2."
 );
 
 namespace dev

libsolidity/formal/BMC.cpp

@@ -114,11 +114,6 @@ bool BMC::visit(ContractDefinition const& _contract)
 {
 	initContract(_contract);
 
-	/// Check targets created by state variable initialization.
-	smt::Expression constraints = m_context.assertions();
-	checkVerificationTargets(constraints);
-	m_verificationTargets.clear();
-
 	SMTEncoder::visit(_contract);
 
 	return false;
@@ -126,6 +121,17 @@ bool BMC::visit(ContractDefinition const& _contract)
 
 void BMC::endVisit(ContractDefinition const& _contract)
 {
+	if (auto constructor = _contract.constructor())
+		constructor->accept(*this);
+	else
+	{
+		inlineConstructorHierarchy(_contract);
+		/// Check targets created by state variable initialization.
+		smt::Expression constraints = m_context.assertions();
+		checkVerificationTargets(constraints);
+		m_verificationTargets.clear();
+	}
+
 	SMTEncoder::endVisit(_contract);
 }
 
@@ -136,10 +142,14 @@ bool BMC::visit(FunctionDefinition const& _function)
 	solAssert(m_currentContract, "");
 	auto const& hierarchy = m_currentContract->annotation().linearizedBaseContracts;
 	if (find(hierarchy.begin(), hierarchy.end(), contract) == hierarchy.end())
-		initializeStateVariables(*contract);
+		createStateVariables(*contract);
 
 	if (m_callStack.empty())
+	{
 		reset();
+		initFunction(_function);
+		resetStateVariables();
+	}
 
 	/// Already visits the children.
 	SMTEncoder::visit(_function);
@@ -451,10 +461,6 @@ void BMC::inlineFunctionCall(FunctionCall const& _funCall)
 		// The reason why we need to pushCallStack here instead of visit(FunctionDefinition)
 		// is that there we don't have `_funCall`.
 		pushCallStack({funDef, &_funCall});
-		// If an internal function is called to initialize
-		// a state variable.
-		if (m_callStack.empty())
-			initFunction(*funDef);
 		funDef->accept(*this);
 	}
 

libsolidity/formal/CHC.cpp

@@ -67,6 +67,15 @@ void CHC::analyze(SourceUnit const& _source)
 	m_context.setAssertionAccumulation(false);
 	m_variableUsage.setFunctionInlining(false);
 
+	auto boolSort = make_shared<smt::Sort>(smt::Kind::Bool);
+	auto genesisSort = make_shared<smt::FunctionSort>(
+		vector<smt::SortPointer>(),
+		boolSort
+	);
+	m_genesisPredicate = createSymbolicBlock(genesisSort, "genesis");
+	auto genesis = (*m_genesisPredicate)({});
+	addRule(genesis, genesis.name);
+
 	_source.accept(*this);
 }
 
@@ -96,10 +105,10 @@ bool CHC::visit(ContractDefinition const& _contract)
 		else
 			m_stateSorts.push_back(smt::smtSort(*var->type()));
 
-	clearIndices();
+	clearIndices(&_contract);
 
-	string interfaceName = "interface_" + _contract.name() + "_" + to_string(_contract.id());
+	string suffix = _contract.name() + "_" + to_string(_contract.id());
-	m_interfacePredicate = createSymbolicBlock(interfaceSort(), interfaceName);
+	m_interfacePredicate = createSymbolicBlock(interfaceSort(), "interface_" + suffix);
 
 	// TODO create static instances for Bool/Int sorts in SolverInterface.
 	auto boolSort = make_shared<smt::Sort>(smt::Kind::Bool);
@@ -107,27 +116,11 @@ bool CHC::visit(ContractDefinition const& _contract)
 		vector<smt::SortPointer>(),
 		boolSort
 	);
-	m_errorPredicate = createSymbolicBlock(errorFunctionSort, "error");
 
-	// If the contract has a constructor it is handled as a function.
+	m_errorPredicate = createSymbolicBlock(errorFunctionSort, "error_" + suffix);
-	// Otherwise we zero-initialize all state vars.
+	m_constructorPredicate = createSymbolicBlock(constructorSort(), "implicit_constructor_" + to_string(_contract.id()));
-	if (!_contract.constructor())
+	auto stateExprs = currentStateVariables();
-	{
+	setCurrentBlock(*m_interfacePredicate, &stateExprs);
-		string constructorName = "constructor_" + _contract.name() + "_" + to_string(_contract.id());
-		m_constructorPredicate = createSymbolicBlock(constructorSort(), constructorName);
-		smt::Expression constructorPred = (*m_constructorPredicate)({});
-		addRule(constructorPred, constructorName);
-
-		for (auto const& var: m_stateVariables)
-		{
-			auto const& symbVar = m_context.variable(*var);
-			symbVar->increaseIndex();
-			m_interface->declareVariable(symbVar->currentName(), symbVar->sort());
-			m_context.setZeroValue(*symbVar);
-		}
-
-		connectBlocks(constructorPred, interface());
-	}
 
 	SMTEncoder::visit(_contract);
 	return false;
@@ -138,6 +131,23 @@ void CHC::endVisit(ContractDefinition const& _contract)
 	if (!shouldVisit(_contract))
 		return;
 
+	for (auto const& var: m_stateVariables)
+	{
+		solAssert(m_context.knownVariable(*var), "");
+		m_context.setZeroValue(*var);
+	}
+	auto genesisPred = (*m_genesisPredicate)({});
+	auto implicitConstructor = (*m_constructorPredicate)(currentStateVariables());
+	connectBlocks(genesisPred, implicitConstructor);
+	m_currentBlock = implicitConstructor;
+
+	if (auto constructor = _contract.constructor())
+		constructor->accept(*this);
+	else
+		inlineConstructorHierarchy(_contract);
+
+	connectBlocks(m_currentBlock, interface());
+
 	for (unsigned i = 0; i < m_verificationTargets.size(); ++i)
 	{
 		auto const& target = m_verificationTargets.at(i);
@@ -154,6 +164,16 @@ bool CHC::visit(FunctionDefinition const& _function)
 	if (!shouldVisit(_function))
 		return false;
 
+	// This is the case for base constructor inlining.
+	if (m_currentFunction)
+	{
+		solAssert(m_currentFunction->isConstructor(), "");
+		solAssert(_function.isConstructor(), "");
+		solAssert(_function.scope() != m_currentContract, "");
+		SMTEncoder::visit(_function);
+		return false;
+	}
+
 	solAssert(!m_currentFunction, "Inlining internal function calls not yet implemented");
 	m_currentFunction = &_function;
 
@@ -165,20 +185,11 @@ bool CHC::visit(FunctionDefinition const& _function)
 	auto functionPred = predicate(*functionEntryBlock, currentFunctionVariables());
 	auto bodyPred = predicate(*bodyBlock);
 
-	// Store the constraints related to variable initialization.
+	connectBlocks(m_currentBlock, functionPred);
-	smt::Expression const& initAssertions = m_context.assertions();
-	m_context.pushSolver();
-
-	connectBlocks(interface(), functionPred);
 	connectBlocks(functionPred, bodyPred);
 
-	m_context.popSolver();
-
 	setCurrentBlock(*bodyBlock);
 
-	// We need to re-add the constraints that were created for initialization of variables.
-	m_context.addAssertion(initAssertions);
-
 	SMTEncoder::visit(*m_currentFunction);
 
 	return false;
@@ -189,10 +200,39 @@ void CHC::endVisit(FunctionDefinition const& _function)
 	if (!shouldVisit(_function))
 		return;
 
+	// This is the case for base constructor inlining.
+	if (m_currentFunction != &_function)
+	{
+		solAssert(m_currentFunction && m_currentFunction->isConstructor(), "");
+		solAssert(_function.isConstructor(), "");
+		solAssert(_function.scope() != m_currentContract, "");
+	}
+	else
+	{
+		// We create an extra exit block for constructors that simply
+		// connects to the interface in case an explicit constructor
+		// exists in the hierarchy.
+		// It is not connected directly here, as normal functions are,
+		// because of the case where there are only implicit constructors.
+		// This is done in endVisit(ContractDefinition).
+		if (_function.isConstructor())
+		{
+			auto constructorExit = createSymbolicBlock(interfaceSort(), "constructor_exit_" + to_string(_function.id()));
+			connectBlocks(m_currentBlock, predicate(*constructorExit, currentStateVariables()));
+			clearIndices(m_currentContract, m_currentFunction);
+			auto stateExprs = currentStateVariables();
+			setCurrentBlock(*constructorExit, &stateExprs);
+		}
+		else
+		{
 			connectBlocks(m_currentBlock, interface());
-
+			clearIndices(m_currentContract, m_currentFunction);
-	solAssert(&_function == m_currentFunction, "");
+			auto stateExprs = currentStateVariables();
+			setCurrentBlock(*m_interfacePredicate, &stateExprs);
+		}
 		m_currentFunction = nullptr;
+	}
+
 	SMTEncoder::endVisit(_function);
 }
 
@@ -447,7 +487,6 @@ void CHC::reset()
 	m_verificationTargets.clear();
 	m_safeAssertions.clear();
 	m_unknownFunctionCallSeen = false;
-	m_blockCounter = 0;
 	m_breakDest = nullptr;
 	m_continueDest = nullptr;
 }
@@ -472,28 +511,31 @@ bool CHC::shouldVisit(FunctionDefinition const& _function) const
 {
 	if (
 		_function.isPublic() &&
-		_function.isImplemented() &&
+		_function.isImplemented()
-		!_function.isConstructor()
 	)
 		return true;
 	return false;
 }
 
-void CHC::setCurrentBlock(smt::SymbolicFunctionVariable const& _block)
+void CHC::setCurrentBlock(
+	smt::SymbolicFunctionVariable const& _block,
+	vector<smt::Expression> const* _arguments
+)
 {
 	m_context.popSolver();
-	clearIndices();
+	solAssert(m_currentContract, "");
+	clearIndices(m_currentContract, m_currentFunction);
 	m_context.pushSolver();
+	if (_arguments)
+		m_currentBlock = predicate(_block, *_arguments);
+	else
 		m_currentBlock = predicate(_block);
 }
 
 smt::SortPointer CHC::constructorSort()
 {
-	solAssert(m_currentContract, "");
+	// TODO this will change once we support function calls.
-	auto boolSort = make_shared<smt::Sort>(smt::Kind::Bool);
+	return interfaceSort();
-	if (!m_currentContract->constructor())
-		return make_shared<smt::FunctionSort>(vector<smt::SortPointer>{}, boolSort);
-	return sort(*m_currentContract->constructor());
 }
 
 smt::SortPointer CHC::interfaceSort()
@@ -558,19 +600,6 @@ unique_ptr<smt::SymbolicFunctionVariable> CHC::createSymbolicBlock(smt::SortPoin
 	return block;
 }
 
-smt::Expression CHC::constructor()
-{
-	solAssert(m_currentContract, "");
-
-	if (!m_currentContract->constructor())
-		return (*m_constructorPredicate)({});
-
-	vector<smt::Expression> paramExprs;
-	for (auto const& var: m_currentContract->constructor()->parameters())
-		paramExprs.push_back(m_context.variable(*var)->currentValue());
-	return (*m_constructorPredicate)(paramExprs);
-}
-
 smt::Expression CHC::interface()
 {
 	vector<smt::Expression> paramExprs;
@@ -615,39 +644,33 @@ void CHC::connectBlocks(smt::Expression const& _from, smt::Expression const& _to
 	addRule(edge, _from.name + "_to_" + _to.name);
 }
 
+vector<smt::Expression> CHC::currentStateVariables()
+{
+	solAssert(m_currentContract, "");
+	vector<smt::Expression> exprs;
+	for (auto const& var: m_stateVariables)
+		exprs.push_back(m_context.variable(*var)->currentValue());
+	return exprs;
+}
+
 vector<smt::Expression> CHC::currentFunctionVariables()
 {
-	solAssert(m_currentFunction, "");
 	vector<smt::Expression> paramExprs;
-	for (auto const& var: m_stateVariables)
+	if (m_currentFunction)
-		paramExprs.push_back(m_context.variable(*var)->currentValue());
 		for (auto const& var: m_currentFunction->parameters() + m_currentFunction->returnParameters())
 			paramExprs.push_back(m_context.variable(*var)->currentValue());
-	return paramExprs;
+	return currentStateVariables() + paramExprs;
 }
 
 vector<smt::Expression> CHC::currentBlockVariables()
 {
-	solAssert(m_currentFunction, "");
 	vector<smt::Expression> paramExprs;
+	if (m_currentFunction)
 		for (auto const& var: m_currentFunction->localVariables())
 			paramExprs.push_back(m_context.variable(*var)->currentValue());
 	return currentFunctionVariables() + paramExprs;
 }
 
-void CHC::clearIndices()
-{
-	for (auto const& var: m_stateVariables)
-		m_context.variable(*var)->resetIndex();
-	if (m_currentFunction)
-	{
-		for (auto const& var: m_currentFunction->parameters() + m_currentFunction->returnParameters())
-			m_context.variable(*var)->resetIndex();
-		for (auto const& var: m_currentFunction->localVariables())
-			m_context.variable(*var)->resetIndex();
-	}
-}
-
 string CHC::predicateName(ASTNode const* _node)
 {
 	string prefix;
@@ -673,7 +696,6 @@ smt::Expression CHC::predicate(
 	return _block(_arguments);
 }
 
-
 void CHC::addRule(smt::Expression const& _rule, string const& _ruleName)
 {
 	m_interface->addRule(_rule, _ruleName);

libsolidity/formal/CHC.h

@@ -86,7 +86,7 @@ private:
 	void eraseKnowledge();
 	bool shouldVisit(ContractDefinition const& _contract) const;
 	bool shouldVisit(FunctionDefinition const& _function) const;
-	void setCurrentBlock(smt::SymbolicFunctionVariable const& _block);
+	void setCurrentBlock(smt::SymbolicFunctionVariable const& _block, std::vector<smt::Expression> const* _arguments = nullptr);
 	//@}
 
 	/// Sort helpers.
@@ -102,8 +102,6 @@ private:
 	/// @returns a new block of given _sort and _name.
 	std::unique_ptr<smt::SymbolicFunctionVariable> createSymbolicBlock(smt::SortPointer _sort, std::string const& _name);
 
-	/// Constructor predicate over current variables.
-	smt::Expression constructor();
 	/// Interface predicate over current variables.
 	smt::Expression interface();
 	/// Error predicate over current variables.
@@ -119,17 +117,16 @@ private:
 
 	void connectBlocks(smt::Expression const& _from, smt::Expression const& _to, smt::Expression const& _constraints = smt::Expression(true));
 
+	/// @returns the current symbolic values of the current state variables.
+	std::vector<smt::Expression> currentStateVariables();
+
 	/// @returns the current symbolic values of the current function's
 	/// input and output parameters.
 	std::vector<smt::Expression> currentFunctionVariables();
-	/// @returns the samve as currentFunctionVariables plus
+	/// @returns the same as currentFunctionVariables plus
 	/// local variables.
 	std::vector<smt::Expression> currentBlockVariables();
 
-	/// Sets the SSA indices of the variables in scope to 0.
-	/// Used when starting a new block.
-	void clearIndices();
-
 	/// @returns the predicate name for a given node.
 	std::string predicateName(ASTNode const* _node);
 	/// @returns a predicate application over the current scoped variables.
@@ -155,8 +152,11 @@ private:
 
 	/// Predicates.
 	//@{
-	/// Constructor predicate.
+	/// Genesis predicate.
-	/// Default constructor sets state vars to 0.
+	std::unique_ptr<smt::SymbolicFunctionVariable> m_genesisPredicate;
+
+	/// Implicit constructor predicate.
+	/// Explicit constructors are handled as functions.
 	std::unique_ptr<smt::SymbolicFunctionVariable> m_constructorPredicate;
 
 	/// Artificial Interface predicate.

libsolidity/formal/SMTEncoder.cpp

@@ -22,6 +22,7 @@
 #include <libsolidity/formal/SymbolicTypes.h>
 
 #include <boost/range/adaptors.hpp>
+#include <boost/range/adaptor/reversed.hpp>
 
 using namespace std;
 using namespace dev;
@@ -39,11 +40,28 @@ bool SMTEncoder::visit(ContractDefinition const& _contract)
 	solAssert(m_currentContract, "");
 
 	for (auto const& node: _contract.subNodes())
-		if (!dynamic_pointer_cast<FunctionDefinition>(node))
+		if (
+			!dynamic_pointer_cast<FunctionDefinition>(node) &&
+			!dynamic_pointer_cast<VariableDeclaration>(node)
+		)
 			node->accept(*this);
 
 	vector<FunctionDefinition const*> resolvedFunctions = _contract.definedFunctions();
 	for (auto const& base: _contract.annotation().linearizedBaseContracts)
+	{
+		// Look for all the constructor invocations bottom up.
+		if (auto const& constructor =  base->constructor())
+			for (auto const& invocation: constructor->modifiers())
+			{
+				auto refDecl = invocation->name()->annotation().referencedDeclaration;
+				if (auto const& baseContract = dynamic_cast<ContractDefinition const*>(refDecl))
+				{
+					solAssert(!m_baseConstructorCalls.count(baseContract), "");
+					m_baseConstructorCalls[baseContract] = invocation.get();
+				}
+			}
+
+		// Check for function overrides.
 		for (auto const& baseFunction: base->definedFunctions())
 		{
 			if (baseFunction->isConstructor())
@@ -63,10 +81,19 @@ bool SMTEncoder::visit(ContractDefinition const& _contract)
 			if (!overridden)
 				resolvedFunctions.push_back(baseFunction);
 		}
+	}
 
+	// Functions are visited first since they might be used
+	// for state variable initialization which is part of
+	// the constructor.
+	// Constructors are visited as part of the constructor
+	// hierarchy inlining.
 	for (auto const& function: resolvedFunctions)
+		if (!function->isConstructor())
 			function->accept(*this);
 
+	// Constructors need to be handled by the engines separately.
+
 	return false;
 }
 
@@ -74,13 +101,16 @@ void SMTEncoder::endVisit(ContractDefinition const& _contract)
 {
 	m_context.resetAllVariables();
 
+	m_baseConstructorCalls.clear();
+
 	solAssert(m_currentContract == &_contract, "");
 	m_currentContract = nullptr;
 }
 
 void SMTEncoder::endVisit(VariableDeclaration const& _varDecl)
 {
-	if (_varDecl.isLocalVariable() && _varDecl.type()->isValueType() &&_varDecl.value())
+	// State variables are handled by the constructor.
+	if (_varDecl.isLocalVariable() &&_varDecl.value())
 		assignment(_varDecl, *_varDecl.value());
 }
 
@@ -91,25 +121,22 @@ bool SMTEncoder::visit(ModifierDefinition const&)
 
 bool SMTEncoder::visit(FunctionDefinition const& _function)
 {
-	// Not visited by a function call
-	if (m_callStack.empty())
-		initFunction(_function);
-
 	m_modifierDepthStack.push_back(-1);
+
 	if (_function.isConstructor())
-	{
+		inlineConstructorHierarchy(dynamic_cast<ContractDefinition const&>(*_function.scope()));
-		m_errorReporter.warning(
+
-			_function.location(),
+	// Base constructors' parameters should be set by explicit calls,
-			"Assertion checker does not yet support constructors."
+	// but the most derived one needs to be initialized.
-		);
+	if (_function.scope() == m_currentContract)
-	}
+		initializeLocalVariables(_function);
-	else
+
-	{
 	_function.parameterList().accept(*this);
 	if (_function.returnParameterList())
 		_function.returnParameterList()->accept(*this);
+
 	visitFunctionOrModifier();
-	}
+
 	return false;
 }
 
@@ -131,27 +158,87 @@ void SMTEncoder::visitFunctionOrModifier()
 		solAssert(m_modifierDepthStack.back() < int(function.modifiers().size()), "");
 		ASTPointer<ModifierInvocation> const& modifierInvocation = function.modifiers()[m_modifierDepthStack.back()];
 		solAssert(modifierInvocation, "");
-		modifierInvocation->accept(*this);
+		auto refDecl = modifierInvocation->name()->annotation().referencedDeclaration;
-		auto const& modifierDef = dynamic_cast<ModifierDefinition const&>(
+		if (dynamic_cast<ContractDefinition const*>(refDecl))
-			*modifierInvocation->name()->annotation().referencedDeclaration
+			visitFunctionOrModifier();
-		);
+		else if (auto modifierDef = dynamic_cast<ModifierDefinition const*>(refDecl))
-		vector<smt::Expression> modifierArgsExpr;
+			inlineModifierInvocation(modifierInvocation.get(), modifierDef);
-		if (auto const* arguments = modifierInvocation->arguments())
+		else
-		{
+			solAssert(false, "");
-			auto const& modifierParams = modifierDef.parameters();
-			solAssert(modifierParams.size() == arguments->size(), "");
-			for (unsigned i = 0; i < arguments->size(); ++i)
-				modifierArgsExpr.push_back(expr(*arguments->at(i), modifierParams.at(i)->type()));
-		}
-		initializeFunctionCallParameters(modifierDef, modifierArgsExpr);
-		pushCallStack({&modifierDef, modifierInvocation.get()});
-		modifierDef.body().accept(*this);
-		popCallStack();
 	}
 
 	--m_modifierDepthStack.back();
 }
 
+void SMTEncoder::inlineModifierInvocation(ModifierInvocation const* _invocation, CallableDeclaration const* _definition)
+{
+	solAssert(_invocation, "");
+	_invocation->accept(*this);
+
+	vector<smt::Expression> args;
+	if (auto const* arguments = _invocation->arguments())
+	{
+		auto const& modifierParams = _definition->parameters();
+		solAssert(modifierParams.size() == arguments->size(), "");
+		for (unsigned i = 0; i < arguments->size(); ++i)
+			args.push_back(expr(*arguments->at(i), modifierParams.at(i)->type()));
+	}
+
+	initializeFunctionCallParameters(*_definition, args);
+
+	pushCallStack({_definition, _invocation});
+	if (auto modifier = dynamic_cast<ModifierDefinition const*>(_definition))
+	{
+		modifier->body().accept(*this);
+		popCallStack();
+	}
+	else if (auto function = dynamic_cast<FunctionDefinition const*>(_definition))
+	{
+		if (function->isImplemented())
+			function->accept(*this);
+		// Functions are popped from the callstack in endVisit(FunctionDefinition)
+	}
+}
+
+void SMTEncoder::inlineConstructorHierarchy(ContractDefinition const& _contract)
+{
+	auto const& hierarchy = m_currentContract->annotation().linearizedBaseContracts;
+	auto it = find(begin(hierarchy), end(hierarchy), &_contract);
+	solAssert(it != end(hierarchy), "");
+
+	auto nextBase = it + 1;
+	// Initialize the base contracts here as long as their constructors are implicit,
+	// stop when the first explicit constructor is found.
+	while (nextBase != end(hierarchy))
+	{
+		if (auto baseConstructor = (*nextBase)->constructor())
+		{
+			createLocalVariables(*baseConstructor);
+			// If any subcontract explicitly called baseConstructor, use those arguments.
+			if (m_baseConstructorCalls.count(*nextBase))
+				inlineModifierInvocation(m_baseConstructorCalls.at(*nextBase), baseConstructor);
+			else if (baseConstructor->isImplemented())
+			{
+				// The first constructor found is handled like a function
+				// and its pushed into the callstack there.
+				// This if avoids duplication in the callstack.
+				if (!m_callStack.empty())
+					pushCallStack({baseConstructor, nullptr});
+				baseConstructor->accept(*this);
+				// popped by endVisit(FunctionDefinition)
+			}
+			break;
+		}
+		else
+		{
+			initializeStateVariables(**nextBase);
+			++nextBase;
+		}
+	}
+
+	initializeStateVariables(_contract);
+}
+
 bool SMTEncoder::visit(PlaceholderStatement const&)
 {
 	solAssert(!m_callStack.empty(), "");
@@ -552,20 +639,25 @@ void SMTEncoder::initContract(ContractDefinition const& _contract)
 	solAssert(m_currentContract == nullptr, "");
 	m_currentContract = &_contract;
 
-	initializeStateVariables(_contract);
+	m_context.reset();
+	m_context.pushSolver();
+	createStateVariables(_contract);
+	clearIndices(m_currentContract, nullptr);
 }
 
 void SMTEncoder::initFunction(FunctionDefinition const& _function)
 {
 	solAssert(m_callStack.empty(), "");
+	solAssert(m_currentContract, "");
 	m_context.reset();
 	m_context.pushSolver();
 	m_pathConditions.clear();
 	pushCallStack({&_function, nullptr});
 	m_uninterpretedTerms.clear();
-	resetStateVariables();
+	createStateVariables(*m_currentContract);
-	initializeLocalVariables(_function);
+	createLocalVariables(_function);
 	m_arrayAssignmentHappened = false;
+	clearIndices(m_currentContract, &_function);
 }
 
 void SMTEncoder::visitAssert(FunctionCall const& _funCall)
@@ -808,11 +900,8 @@ void SMTEncoder::endVisit(IndexAccess const& _indexAccess)
 		return;
 	}
 
-	if (!_indexAccess.indexExpression())
+	if (_indexAccess.annotation().type->category() == Type::Category::TypeType)
-	{
-		solAssert(_indexAccess.annotation().type->category() == Type::Category::TypeType, "");
 		return;
-	}
 
 	solAssert(array, "");
 	defineExpr(_indexAccess, smt::Expression::select(
@@ -1249,27 +1338,62 @@ void SMTEncoder::initializeFunctionCallParameters(CallableDeclaration const& _fu
 			}
 }
 
-void SMTEncoder::initializeStateVariables(ContractDefinition const& _contract)
+void SMTEncoder::createStateVariables(ContractDefinition const& _contract)
 {
 	for (auto var: _contract.stateVariablesIncludingInherited())
 		createVariable(*var);
 }
 
-void SMTEncoder::initializeLocalVariables(FunctionDefinition const& _function)
+void SMTEncoder::initializeStateVariables(ContractDefinition const& _contract)
+{
+	for (auto var: _contract.stateVariables())
+	{
+		solAssert(m_context.knownVariable(*var), "");
+		m_context.setZeroValue(*var);
+	}
+
+	for (auto var: _contract.stateVariables())
+		if (var->value())
+		{
+			var->value()->accept(*this);
+			assignment(*var, *var->value());
+		}
+}
+
+void SMTEncoder::createLocalVariables(FunctionDefinition const& _function)
 {
 	for (auto const& variable: _function.localVariables())
-		if (createVariable(*variable))
+		createVariable(*variable);
-			m_context.setZeroValue(*variable);
 
 	for (auto const& param: _function.parameters())
-		if (createVariable(*param))
+		createVariable(*param);
-			m_context.setUnknownValue(*param);
 
 	if (_function.returnParameterList())
 		for (auto const& retParam: _function.returnParameters())
-			if (createVariable(*retParam))
+			createVariable(*retParam);
+}
+
+void SMTEncoder::initializeLocalVariables(FunctionDefinition const& _function)
+{
+	for (auto const& variable: _function.localVariables())
+	{
+		solAssert(m_context.knownVariable(*variable), "");
+		m_context.setZeroValue(*variable);
+	}
+
+	for (auto const& param: _function.parameters())
+	{
+		solAssert(m_context.knownVariable(*param), "");
+		m_context.setUnknownValue(*param);
+	}
+
+	if (_function.returnParameterList())
+		for (auto const& retParam: _function.returnParameters())
+		{
+			solAssert(m_context.knownVariable(*retParam), "");
 			m_context.setZeroValue(*retParam);
 		}
+}
 
 void SMTEncoder::resetStateVariables()
 {
@@ -1448,6 +1572,20 @@ void SMTEncoder::resetVariableIndices(VariableIndices const& _indices)
 		m_context.variable(*var.first)->index() = var.second;
 }
 
+void SMTEncoder::clearIndices(ContractDefinition const* _contract, FunctionDefinition const* _function)
+{
+	solAssert(_contract, "");
+	for (auto var: _contract->stateVariablesIncludingInherited())
+		m_context.variable(*var)->resetIndex();
+	if (_function)
+	{
+		for (auto const& var: _function->parameters() + _function->returnParameters())
+			m_context.variable(*var)->resetIndex();
+		for (auto const& var: _function->localVariables())
+			m_context.variable(*var)->resetIndex();
+	}
+}
+
 Expression const* SMTEncoder::leftmostBase(IndexAccess const& _indexAccess)
 {
 	Expression const* base = &_indexAccess.baseExpression();

libsolidity/formal/SMTEncoder.h

@@ -123,6 +123,12 @@ protected:
 	/// visit depth.
 	void visitFunctionOrModifier();
 
+	/// Inlines a modifier or base constructor call.
+	void inlineModifierInvocation(ModifierInvocation const* _invocation, CallableDeclaration const* _definition);
+
+	/// Inlines the constructor hierarchy into a single constructor.
+	void inlineConstructorHierarchy(ContractDefinition const& _contract);
+
 	/// Defines a new global variable or function.
 	void defineGlobalVariable(std::string const& _name, Expression const& _expr, bool _increaseIndex = false);
 
@@ -162,7 +168,9 @@ protected:
 
 	using CallStackEntry = std::pair<CallableDeclaration const*, ASTNode const*>;
 
+	void createStateVariables(ContractDefinition const& _contract);
 	void initializeStateVariables(ContractDefinition const& _contract);
+	void createLocalVariables(FunctionDefinition const& _function);
 	void initializeLocalVariables(FunctionDefinition const& _function);
 	void initializeFunctionCallParameters(CallableDeclaration const& _function, std::vector<smt::Expression> const& _callArgs);
 	void resetStateVariables();
@@ -210,6 +218,9 @@ protected:
 	VariableIndices copyVariableIndices();
 	/// Resets the variable indices.
 	void resetVariableIndices(VariableIndices const& _indices);
+	/// Used when starting a new block.
+	void clearIndices(ContractDefinition const* _contract, FunctionDefinition const* _function = nullptr);
+
 
 	/// @returns variables that are touched in _node's subtree.
 	std::set<VariableDeclaration const*> touchedVariables(ASTNode const& _node);
@@ -254,6 +265,8 @@ protected:
 	/// Needs to be a stack because of function calls.
 	std::vector<int> m_modifierDepthStack;
 
+	std::map<ContractDefinition const*, ModifierInvocation const*> m_baseConstructorCalls;
+
 	ContractDefinition const* m_currentContract = nullptr;
 
 	/// Stores the context of the encoding.

libsolidity/formal/SymbolicTypes.cpp

@@ -63,7 +63,7 @@ SortPointer smtSort(solidity::Type const& _type)
 		{
 			auto mapType = dynamic_cast<solidity::MappingType const*>(&_type);
 			solAssert(mapType, "");
-			return make_shared<ArraySort>(smtSort(*mapType->keyType()), smtSort(*mapType->valueType()));
+			return make_shared<ArraySort>(smtSortAbstractFunction(*mapType->keyType()), smtSortAbstractFunction(*mapType->valueType()));
 		}
 		else if (isStringLiteral(_type.category()))
 		{
@@ -77,7 +77,7 @@ SortPointer smtSort(solidity::Type const& _type)
 			solAssert(isArray(_type.category()), "");
 			auto arrayType = dynamic_cast<solidity::ArrayType const*>(&_type);
 			solAssert(arrayType, "");
-			return make_shared<ArraySort>(make_shared<Sort>(Kind::Int), smtSort(*arrayType->baseType()));
+			return make_shared<ArraySort>(make_shared<Sort>(Kind::Int), smtSortAbstractFunction(*arrayType->baseType()));
 		}
 	}
 	default:
@@ -94,6 +94,13 @@ vector<SortPointer> smtSort(vector<solidity::TypePointer> const& _types)
 	return sorts;
 }
 
+SortPointer smtSortAbstractFunction(solidity::Type const& _type)
+{
+	if (isFunction(_type.category()))
+		return make_shared<Sort>(Kind::Int);
+	return smtSort(_type);
+}
+
 Kind smtKind(solidity::Type::Category _category)
 {
 	if (isNumber(_category))

libsolidity/formal/SymbolicTypes.h

@@ -32,6 +32,9 @@ namespace smt
 /// Returns the SMT sort that models the Solidity type _type.
 SortPointer smtSort(solidity::Type const& _type);
 std::vector<SortPointer> smtSort(std::vector<solidity::TypePointer> const& _types);
+/// If _type has type Function, abstract it to Integer.
+/// Otherwise return smtSort(_type).
+SortPointer smtSortAbstractFunction(solidity::Type const& _type);
 /// Returns the SMT kind that models the Solidity type type category _category.
 Kind smtKind(solidity::Type::Category _category);
 

scripts/build_emscripten.sh

@@ -34,7 +34,7 @@ else
 	BUILD_DIR="$1"
 fi
 
-docker run -v $(pwd):/root/project -w /root/project trzeci/emscripten:sdk-tag-1.38.22-64bit \
+docker run -v $(pwd):/root/project -w /root/project trzeci/emscripten:sdk-tag-1.39.3-64bit \
     ./scripts/travis-emscripten/install_deps.sh
-docker run -v $(pwd):/root/project -w /root/project trzeci/emscripten:sdk-tag-1.38.22-64bit \
+docker run -v $(pwd):/root/project -w /root/project trzeci/emscripten:sdk-tag-1.39.3-64bit \
     ./scripts/travis-emscripten/build_emscripten.sh $BUILD_DIR

scripts/travis-emscripten/build_emscripten.sh

@@ -55,11 +55,11 @@ fi
 WORKSPACE=/root/project
 
 # Increase nodejs stack size
-if ! [ -e /emsdk_portable/node/bin/node_orig ]
+if ! [ -e /emsdk_portable/node/current/bin/node_orig ]
 then
-  mv /emsdk_portable/node/bin/node /emsdk_portable/node/bin/node_orig
+  mv /emsdk_portable/node/current/bin/node /emsdk_portable/node/current/bin/node_orig
-  echo -e '#!/bin/sh\nexec /emsdk_portable/node/bin/node_orig --stack-size=8192 $@' > /emsdk_portable/node/bin/node
+  echo -e '#!/bin/sh\nexec /emsdk_portable/node/current/bin/node_orig --stack-size=8192 $@' > /emsdk_portable/node/current/bin/node
-  chmod 755 /emsdk_portable/node/bin/node
+  chmod 755 /emsdk_portable/node/current/bin/node
 fi
 
 # Boost
@@ -70,8 +70,8 @@ cd "$WORKSPACE"/boost_1_70_0
        --with-system --with-filesystem --with-test --with-program_options cxxflags="-Wno-unused-local-typedef -Wno-variadic-macros -Wno-c99-extensions -Wno-all" \
        --prefix="$WORKSPACE"/boost_1_70_0_install install
 )
-ln -sf "$WORKSPACE"/boost_1_70_0_install/lib/* /emsdk_portable/sdk/system/lib
+ln -sf "$WORKSPACE"/boost_1_70_0_install/lib/* /emsdk_portable/emscripten/sdk/system/lib
-ln -sf "$WORKSPACE"/boost_1_70_0_install/include/* /emsdk_portable/sdk/system/include
+ln -sf "$WORKSPACE"/boost_1_70_0_install/include/* /emsdk_portable/emscripten/sdk/system/include
 echo -en 'travis_fold:end:compiling_boost\\r'
 
 echo -en 'travis_fold:start:install_cmake.sh\\r'
@@ -94,8 +94,6 @@ make -j 4
 
 cd ..
 mkdir -p upload
-# Patch soljson.js to provide backwards-compatibility with older emscripten versions
-echo ";/* backwards compatibility */ Module['Runtime'] = Module;" >> $BUILD_DIR/libsolc/soljson.js
 cp $BUILD_DIR/libsolc/soljson.js upload/
 cp $BUILD_DIR/libsolc/soljson.js ./
 

scripts/travis-emscripten/emscripten.jam

@@ -0,0 +1,186 @@
+# Modified version of emscripten.jam from https://github.com/tee3/boost-build-emscripten
+# which is released under the following license:
+#
+# Boost Software License - Version 1.0 - August 17th, 2003
+#
+# Permission is hereby granted, free of charge, to any person or organization
+# obtaining a copy of the software and accompanying documentation covered by
+# this license (the "Software") to use, reproduce, display, distribute,
+# execute, and transmit the Software, and to prepare derivative works of the
+# Software, and to permit third-parties to whom the Software is furnished to
+# do so, all subject to the following:
+#
+# The copyright notices in the Software and this entire statement, including
+# the above license grant, this restriction and the following disclaimer,
+# must be included in all copies of the Software, in whole or in part, and
+# all derivative works of the Software, unless such copies or derivative
+# works are solely in the form of machine-executable object code generated by
+# a source language processor.
+#
+# THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+# IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+# FITNESS FOR A PARTICULAR PURPOSE, TITLE AND NON-INFRINGEMENT. IN NO EVENT
+# SHALL THE COPYRIGHT HOLDERS OR ANYONE DISTRIBUTING THE SOFTWARE BE LIABLE
+# FOR ANY DAMAGES OR OTHER LIABILITY, WHETHER IN CONTRACT, TORT OR OTHERWISE,
+# ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER
+# DEALINGS IN THE SOFTWARE.
+#
+# Boost.Build support for Emscipten.
+#
+# @todo add support for dynamic linking
+# @todo add support for --js-library, --pre-js, and --post-js options
+
+import generators ;
+import type ;
+import toolset ;
+import feature ;
+import common ;
+import errors ;
+
+if [ MATCH (--debug-configuration) : [ modules.peek : ARGV ] ]
+{
+  .debug-configuration = true ;
+}
+
+# add an emscripten toolset
+feature.extend toolset : emscripten ;
+
+# extend the target-os list to include emscripten
+feature.extend target-os : emscripten ;
+# make emscripten the default target-os when compiling with the emscripten toolset
+feature.set-default target-os : emscripten ;
+
+# initialize the emscripten toolset
+rule init ( version ? : command * : options * )
+{
+  command = [ common.get-invocation-command emscripten : em++ : $(command) ] ;
+
+  if $(command)
+  {
+    version ?= [ MATCH "^([0-9.]+)" : [ SHELL \""$(command)\" --version" ] ] ;
+    if $(version)
+    {
+      local actual_version = [ MATCH "^([0-9.]+)" : [ SHELL \""$(command)\" --version" ] ] ;
+      if $(actual_version) != $(version)
+      {
+        errors.user-error "emscripten: detected version $(actual_version) does not match desired $(version)" ;
+      }
+    }
+  }
+  else
+  {
+    errors.user-error "emscripten: em++ not found" ;
+  }
+
+  local condition = [ common.check-init-parameters emscripten : version $(version) ] ;
+
+  common.handle-options emscripten : $(condition) : $(command) : $(options) ;
+
+  # @todo this seems to be the right way, but this is a list somehow
+  toolset.add-requirements <toolset>emscripten:<testing.launcher>node ;
+
+  toolset.flags emscripten.compile STDHDRS $(condition) : /emsdk_portable/emscripten/sdk/system/include ;
+  toolset.flags emscripten.link STDLIBPATH $(condition) : /emsdk_portable/emscripten/sdk/system/lib ;
+  toolset.flags emscripten AR $(condition) : /emsdk_portable/emscripten/sdk/emar ;
+  toolset.flags emscripten RANLIB $(condition) : /emsdk_portable/emscripten/sdk/emranlib ;
+}
+
+type.set-generated-target-suffix EXE : <toolset>emscripten : js ;
+#type.set-generated-target-suffix STATIC_LIB : <toolset>emscripten : bc ;
+#type.set-generated-target-suffix SHARED_LIB : <toolset>emscripten : bc ;
+#type.set-generated-target-suffix OBJ : <toolset>emscripten : bc ;
+
+generators.register-linker emscripten.link : OBJ STATIC_LIB : EXE : <toolset>emscripten ;
+
+generators.register-archiver emscripten.archive : OBJ : STATIC_LIB : <toolset>emscripten ;
+
+generators.register-c-compiler emscripten.compile.c++.preprocess : CPP : PREPROCESSED_CPP : <toolset>emscripten ;
+generators.register-c-compiler emscripten.compile.c.preprocess   : C   : PREPROCESSED_C   : <toolset>emscripten ;
+generators.register-c-compiler emscripten.compile.c++ : CPP : OBJ : <toolset>emscripten ;
+generators.register-c-compiler emscripten.compile.c : C : OBJ : <toolset>emscripten ;
+
+# Declare flags
+
+toolset.flags emscripten.compile OPTIONS <optimization>off   : -O0 ;
+toolset.flags emscripten.compile OPTIONS <optimization>speed : -O3 ;
+toolset.flags emscripten.compile OPTIONS <optimization>space : -Os ;
+
+toolset.flags emscripten.compile OPTIONS <inlining>off  : -fno-inline ;
+toolset.flags emscripten.compile OPTIONS <inlining>on   : -Wno-inline ;
+toolset.flags emscripten.compile OPTIONS <inlining>full : -finline-functions -Wno-inline ;
+
+toolset.flags emscripten.compile OPTIONS <warnings>off : -w ;
+toolset.flags emscripten.compile OPTIONS <warnings>on  : -Wall ;
+toolset.flags emscripten.compile OPTIONS <warnings>all : -Wall -pedantic ;
+toolset.flags emscripten.compile OPTIONS <warnings-as-errors>on : -Werror ;
+
+toolset.flags emscripten.compile OPTIONS <debug-symbols>on : -g ;
+toolset.flags emscripten.compile OPTIONS <profiling>on : -pg ;
+
+toolset.flags emscripten.compile.c++ OPTIONS <rtti>off : -fno-rtti ;
+toolset.flags emscripten.compile.c++ OPTIONS <exception-handling>off : -fno-exceptions ;
+
+toolset.flags emscripten.compile USER_OPTIONS <cflags> ;
+toolset.flags emscripten.compile.c++ USER_OPTIONS <cxxflags> ;
+toolset.flags emscripten.compile DEFINES <define> ;
+toolset.flags emscripten.compile INCLUDES <include> ;
+toolset.flags emscripten.compile.c++ TEMPLATE_DEPTH <c++-template-depth> ;
+toolset.flags emscripten.compile.fortran USER_OPTIONS <fflags> ;
+
+toolset.flags emscripten.link DEFAULTS : -Wno-warn-absolute-paths ;
+
+toolset.flags emscripten.link LIBRARY_PATH <library-path> ;
+toolset.flags emscripten.link FINDLIBS_ST <find-static-library> ;
+toolset.flags emscripten.link FINDLIBS_SA <find-shared-library> ;
+toolset.flags emscripten.link LIBRARIES <library-file> ;
+
+toolset.flags emscripten.link OPTIONS <linkflags> ;
+
+toolset.flags emscripten.archive AROPTIONS <archiveflags> ;
+
+rule compile.c++ ( targets * : sources * : properties * )
+{
+    # Some extensions are compiled as C++ by default. For others, we need to
+    # pass -x c++. We could always pass -x c++ but distcc does not work with it.
+    if ! $(>:S) in .cc .cp .cxx .cpp .c++ .C
+    {
+        LANG on $(<) = "-x c++" ;
+    }
+}
+
+rule compile.c ( targets * : sources * : properties * )
+{
+    LANG on $(<) = "-x c" ;
+}
+
+actions compile.c++
+{
+    "$(CONFIG_COMMAND)" $(LANG) $(OPTIONS) $(USER_OPTIONS) -D$(DEFINES) -I"$(INCLUDES)" -c -o "$(<:W)" "$(>:W)"
+}
+
+actions compile.c
+{
+    "$(CONFIG_COMMAND)" $(LANG) $(OPTIONS) $(USER_OPTIONS) -D$(DEFINES) -I"$(INCLUDES)" -c -o "$(<)" "$(>)"
+}
+
+actions compile.c++.preprocess
+{
+    "$(CONFIG_COMMAND)" $(LANG) $(OPTIONS) $(USER_OPTIONS) -D$(DEFINES) -I"$(INCLUDES)" "$(>:W)" -E >"$(<:W)"
+}
+
+actions compile.c.preprocess
+{
+    "$(CONFIG_COMMAND)" $(LANG) $(OPTIONS) $(USER_OPTIONS) -D$(DEFINES) -I"$(INCLUDES)" "$(>)" -E >$(<)
+}
+
+actions link
+{
+  "$(CONFIG_COMMAND)" $(DEFAULTS) $(OPTIONS) -L"$(LIBRARY_PATH:W)" -L"$(STDLIBPATH:W)" -o "$(<:W)" "$(>:W)" -l"$(LIBRARIES:W)" -l"$(STDLIBRARIES:W)"
+}
+
+RM = [ common.rm-command ] ;
+actions piecemeal archive
+{
+  $(RM) "$(<)"
+  $(AR) $(AROPTIONS) rc "$(<:W)" "$(>:W)"
+}

scripts/travis-emscripten/install_deps.sh

@@ -29,6 +29,8 @@
 
 set -ev
 
+SCRIPT_DIR="$(realpath $(dirname $0))"
+
 echo -en 'travis_fold:start:installing_dependencies\\r'
 test -e boost_1_70_0_install/include/boost/version.hpp || (
 rm -rf boost_1_70_0
@@ -40,8 +42,7 @@ tar -xzf boost.tar.gz
 rm boost.tar.gz
 cd boost_1_70_0
 ./bootstrap.sh
-wget -q 'https://raw.githubusercontent.com/tee3/boost-build-emscripten/master/emscripten.jam'
+cp "${SCRIPT_DIR}/emscripten.jam" .
-test "$(shasum emscripten.jam)" = "a7e13fc2c1e53b0e079ef440622f879aa6da3049  emscripten.jam"
 echo "using emscripten : : em++ ;" >> project-config.jam
 )
 cd ..

test/externalTests/zeppelin.sh

@@ -36,7 +36,6 @@ function zeppelin_test
     truffle_setup https://github.com/erak/openzeppelin-contracts.git master_060
     run_install install_fn
 
-
     truffle_run_test compile_fn test_fn
 }
 

test/liblll/Compiler.cpp

@@ -193,6 +193,8 @@ BOOST_AUTO_TEST_CASE(valid_opcodes_functional)
 		"4300",
 		"4400",
 		"4500",
+		"4600",
+		"4700",
 		"60005000",
 		"60005100",
 		"600060005200",
@@ -420,6 +422,8 @@ BOOST_AUTO_TEST_CASE(valid_opcodes_asm)
 		"4300",
 		"4400",
 		"4500",
+		"4600",
+		"4700",
 		"60005000",
 		"60005100",
 		"600060005200",
@@ -559,6 +563,8 @@ BOOST_AUTO_TEST_CASE(valid_opcodes_asm)
 		"(asm NUMBER)",
 		"(asm DIFFICULTY)",
 		"(asm GASLIMIT)",
+		"(asm CHAINID)",
+		"(asm SELFBALANCE)",
 		"(asm 0 POP)",
 		"(asm 0 MLOAD)",
 		"(asm 0 0 MSTORE)",

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

@@ -53,6 +53,5 @@ contract MyConc{
 // ----
 // Warning: (773-792): This declaration shadows an existing declaration.
 // Warning: (1009-1086): Function state mutability can be restricted to view
-// Warning: (874-879): Underflow (resulting value less than 0) happens here.
+// Warning: (985-1002): Underflow (resulting value less than 0) happens here.
-// Warning: (874-879): Overflow (resulting value larger than 2**256 - 1) happens here.
 // Warning: (985-1002): Overflow (resulting value larger than 2**256 - 1) happens here.

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

@@ -137,4 +137,3 @@ contract PropagateThroughReturnValue {
 // Warning: (748-755): Assertion checker does not yet support this expression.
 // Warning: (748-751): Assertion checker does not yet implement type struct Reference.St storage pointer
 // Warning: (748-770): Assertion checker does not yet implement such assignments.
-// Warning: (849-905): Assertion checker does not yet support constructors.

test/libsolidity/smtCheckerTests/functions/constructor_base_basic.sol

@@ -13,5 +13,3 @@ contract B is A {
 	}
 }
 // ----
-// Warning: (56-90): Assertion checker does not yet support constructors.
-// Warning: (113-151): Assertion checker does not yet support constructors.

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy.sol

@@ -1,6 +1,16 @@
 pragma experimental SMTChecker;
-contract C { constructor(uint) public {} }
+contract C {
-contract A is C { constructor() C(2) public {} }
+	uint a;
+	constructor(uint x) public {
+		a = x;
+	}
+}
+
+contract A is C {
+	constructor() C(2) public {
+		assert(a == 2);
+		assert(a == 3);
+	}
+}
 // ----
-// Warning: (45-72): Assertion checker does not yet support constructors.
+// Warning: (166-180): Assertion violation happens here
-// Warning: (93-121): Assertion checker does not yet support constructors.

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_2.sol

@@ -1,10 +1,7 @@
 pragma experimental SMTChecker;
-contract C { constructor(uint) public {} }
+contract C { uint a; constructor(uint x) public { a = x; } }
-contract A is C { constructor() C(2) public {} }
+contract A is C { constructor() C(2) public { assert(a == 2); } }
-contract B is C { constructor() C(3) public {} }
+contract B is C { constructor() C(3) public { assert(a == 3); } }
-contract J is C { constructor() C(3) public {} }
+contract J is C { constructor() C(3) public { assert(a == 4); } }
 // ----
-// Warning: (45-72): Assertion checker does not yet support constructors.
+// Warning: (271-285): Assertion violation happens here
-// Warning: (93-121): Assertion checker does not yet support constructors.
-// Warning: (142-170): Assertion checker does not yet support constructors.
-// Warning: (191-219): Assertion checker does not yet support constructors.

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_3.sol

@@ -0,0 +1,22 @@
+pragma experimental SMTChecker;
+contract C {
+	uint a;
+	constructor(uint x) public {
+		a = x;
+	}
+}
+
+contract B is C {
+	constructor(uint x) public {
+		a = x;
+	}
+}
+
+contract A is B {
+	constructor(uint x) B(x) C(x + 2) public {
+		assert(a == x);
+		assert(a == x + 1);
+	}
+}
+// ----
+// Warning: (244-262): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_4.sol

@@ -0,0 +1,23 @@
+pragma experimental SMTChecker;
+contract C {
+	uint a;
+	constructor(uint x) public {
+		a = x;
+	}
+}
+
+contract B is C {
+	constructor(uint x) public {
+		a = x;
+	}
+}
+
+contract A is B {
+	constructor(uint x) C(x + 2) B(x + 1) public {
+		assert(a == x + 1);
+	}
+}
+// ----
+// Warning: (212-217): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning: (203-208): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning: (242-247): Overflow (resulting value larger than 2**256 - 1) happens here

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond.sol

@@ -0,0 +1,29 @@
+pragma experimental SMTChecker;
+contract C {
+	uint a;
+	constructor(uint x) public {
+		a = x;
+	}
+}
+
+contract B1 is C {
+	constructor(uint x) public {
+		a = x;
+	}
+}
+
+contract B2 is C {
+	constructor(uint x) C(x + 2) public {
+		a = x;
+	}
+}
+
+contract A is B2, B1 {
+	constructor(uint x) B2(x) B1(x) public {
+		assert(a == x);
+		assert(a == x + 1);
+	}
+}
+// ----
+// Warning: (205-210): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning: (321-339): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond_2.sol

@@ -0,0 +1,29 @@
+pragma experimental SMTChecker;
+contract C {
+	uint a;
+	constructor(uint x) public {
+		a = x;
+	}
+}
+
+contract B1 is C {
+	constructor(uint x) public {
+		a = x;
+	}
+}
+
+contract B2 is C {
+	constructor(uint x) C(x + 2) public {
+		a = x;
+	}
+}
+
+contract A is B2, B1 {
+	constructor(uint x) B1(x) B2(x) public {
+		assert(a == x);
+		assert(a == x + 1);
+	}
+}
+// ----
+// Warning: (205-210): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning: (321-339): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond_3.sol

@@ -0,0 +1,34 @@
+pragma experimental SMTChecker;
+contract C {
+	uint a;
+	constructor(uint x) public {
+		a = x;
+	}
+}
+
+contract B1 is C {
+	uint b1;
+	constructor(uint x) public {
+		b1 = x + a;
+	}
+}
+
+contract B2 is C {
+	uint b2;
+	constructor(uint x) C(x + 2) public {
+		b2 = x + a;
+	}
+}
+
+contract A is B2, B1 {
+	constructor(uint x) B2(x) B1(x) public {
+		assert(b1 == b2);
+		assert(b1 != b2);
+	}
+}
+// ----
+// Warning: (165-170): Underflow (resulting value less than 0) happens here
+// Warning: (165-170): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning: (230-235): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning: (253-258): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning: (353-369): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond_empty_middle.sol

@@ -0,0 +1,23 @@
+pragma experimental SMTChecker;
+contract C {
+	uint a;
+	constructor() public {
+		a = 2;
+	}
+}
+
+contract B is C {
+}
+
+contract B2 is C {
+}
+
+contract A is B, B2 {
+	constructor(uint x) public {
+		assert(a == 2);
+		assert(a == 3);
+	}
+}
+// ----
+// Warning: (171-177): Unused function parameter. Remove or comment out the variable name to silence this warning.
+// Warning: (208-222): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond_empty_middle_empty_base.sol

@@ -0,0 +1,19 @@
+pragma experimental SMTChecker;
+contract C {
+	uint a;
+	constructor() public {
+		a = 2;
+	}
+}
+
+contract B is C {
+}
+
+contract B2 is C {
+	constructor() public {
+		assert(a == 2);
+	}
+}
+
+contract A is B, B2 {
+}

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_empty_chain.sol

@@ -0,0 +1,22 @@
+pragma experimental SMTChecker;
+contract F {
+	uint a;
+	constructor() public {
+		a = 2;
+	}
+}
+
+contract E is F {}
+contract D is E {}
+contract C is D {}
+contract B is C {}
+
+contract A is B {
+	constructor(uint x) public {
+		assert(a == 2);
+		assert(a == 3);
+	}
+}
+// ----
+// Warning: (201-207): Unused function parameter. Remove or comment out the variable name to silence this warning.
+// Warning: (238-252): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_empty_middle.sol

@@ -0,0 +1,20 @@
+pragma experimental SMTChecker;
+contract C {
+	uint a;
+	constructor() public {
+		a = 2;
+	}
+}
+
+contract B is C {
+}
+
+contract A is B {
+	constructor(uint x) B() public {
+		assert(a == 2);
+		assert(a == 3);
+	}
+}
+// ----
+// Warning: (145-151): Unused function parameter. Remove or comment out the variable name to silence this warning.
+// Warning: (186-200): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_empty_middle_no_invocation.sol

@@ -0,0 +1,19 @@
+pragma experimental SMTChecker;
+contract C {
+	uint a;
+	constructor() public {
+		a = 2;
+	}
+}
+
+contract B is C {
+}
+
+contract A is B {
+	constructor(uint x) public {
+		assert(a == 3);
+	}
+}
+// ----
+// Warning: (145-151): Unused function parameter. Remove or comment out the variable name to silence this warning.
+// Warning: (164-178): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_mixed_chain.sol

@@ -0,0 +1,30 @@
+pragma experimental SMTChecker;
+contract F {
+	uint a;
+	constructor() public {
+		a = 2;
+	}
+}
+
+contract E is F {}
+contract D is E {
+	constructor() public {
+		a = 3;
+	}
+}
+contract C is D {}
+contract B is C {
+	constructor() public {
+		a = 4;
+	}
+}
+
+contract A is B {
+	constructor(uint x) public {
+		assert(a == 4);
+		assert(a == 5);
+	}
+}
+// ----
+// Warning: (275-281): Unused function parameter. Remove or comment out the variable name to silence this warning.
+// Warning: (312-326): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_mixed_chain_empty_base.sol

@@ -0,0 +1,24 @@
+pragma experimental SMTChecker;
+contract F {
+	uint a;
+	constructor() public {
+		a = 2;
+	}
+}
+
+contract E is F {}
+contract D is E {
+	constructor() public {
+		a = 3;
+	}
+}
+contract C is D {}
+contract B is C {
+	constructor() public {
+		assert(a == 3);
+		a = 4;
+	}
+}
+
+contract A is B {
+}

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_mixed_chain_local_vars.sol

@@ -0,0 +1,35 @@
+pragma experimental SMTChecker;
+contract F {
+	uint a;
+	constructor() public {
+		uint f = 2;
+		a = f;
+	}
+}
+
+contract E is F {}
+contract D is E {
+	constructor() public {
+		uint d = 3;
+		a = d;
+	}
+}
+contract C is D {}
+contract B is C {
+	constructor() public {
+		uint b = 4;
+		a = b;
+	}
+}
+
+contract A is B {
+	constructor(uint x) public {
+		uint a1 = 4;
+		uint a2 = 5;
+		assert(a == a1);
+		assert(a == a2);
+	}
+}
+// ----
+// Warning: (317-323): Unused function parameter. Remove or comment out the variable name to silence this warning.
+// Warning: (385-400): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_mixed_chain_with_params.sol

@@ -0,0 +1,29 @@
+pragma experimental SMTChecker;
+contract F {
+	uint a;
+	constructor(uint x) public {
+		a = x;
+	}
+}
+
+contract E is F {}
+contract D is E {
+	constructor() public {
+		a = 3;
+	}
+}
+contract C is D {}
+contract B is C {
+	constructor(uint x) F(x + 1) public {
+	}
+}
+
+contract A is B {
+	constructor(uint x) B(x) public {
+		assert(a == 3);
+		assert(a == 4);
+	}
+}
+// ----
+// Warning: (234-239): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning: (329-343): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_mixed_chain_with_params_2.sol

@@ -0,0 +1,27 @@
+pragma experimental SMTChecker;
+contract F {
+	uint a;
+	constructor(uint x) public {
+		a = x;
+	}
+}
+
+contract E is F {}
+contract D is E {
+	constructor() public {
+		a = 3;
+	}
+}
+contract C is D {}
+contract B is C {
+	constructor() F(1) public {
+		assert(a == 3);
+		assert(a == 2);
+	}
+}
+
+contract A is B {
+}
+// ----
+// Warning: (260-274): Assertion violation happens here
+// Warning: (260-274): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_modifier.sol

@@ -0,0 +1,17 @@
+pragma experimental SMTChecker;
+contract C {
+	uint a;
+	modifier n { _; a = 7; }
+	constructor(uint x) n public {
+		a = x;
+	}
+}
+
+contract A is C {
+	modifier m { a = 5; _; }
+	constructor() C(2) public {
+		assert(a == 4);
+	}
+}
+// ----
+// Warning: (202-216): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_same_var.sol

@@ -0,0 +1,16 @@
+pragma experimental SMTChecker;
+contract C {
+	uint a;
+	constructor(uint x) public {
+		a = x;
+	}
+}
+
+contract A is C {
+	constructor() C(2) public {
+		assert(a == 0);
+		assert(C.a == 0);
+	}
+}
+// ----
+// Warning: (148-162): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/constructor_simple.sol

@@ -0,0 +1,16 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint x;
+
+	constructor() public {
+		assert(x == 0);
+		x = 10;
+	}
+
+	function f(uint y) public view {
+		assert(y == x);
+	}
+}
+// ----
+// Warning: (148-162): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/constructor_state_value.sol

@@ -0,0 +1,16 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint x = 5;
+
+	constructor() public {
+		assert(x == 5);
+		x = 10;
+	}
+
+	function f(uint y) public view {
+		assert(y == x);
+	}
+}
+// ----
+// Warning: (152-166): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/constructor_state_value_inherited.sol

@@ -0,0 +1,18 @@
+pragma experimental SMTChecker;
+
+contract B {
+	uint x = 5;
+}
+
+contract C is B {
+	constructor() public {
+		assert(x == 5);
+		x = 10;
+	}
+
+	function f(uint y) public view {
+		assert(y == x);
+	}
+}
+// ----
+// Warning: (172-186): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/constructor_state_value_parameter.sol

@@ -0,0 +1,17 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint x = 5;
+
+	constructor(uint a, uint b) public {
+		assert(x == 5);
+		x = a + b;
+	}
+
+	function f(uint y) public view {
+		assert(y == x);
+	}
+}
+// ----
+// Warning: (169-183): Assertion violation happens here
+// Warning: (122-127): Overflow (resulting value larger than 2**256 - 1) happens here

test/libsolidity/smtCheckerTests/functions/constructor_this.sol

@@ -0,0 +1,13 @@
+pragma experimental SMTChecker;
+contract C {
+    function f() public pure {}
+    constructor() public {
+        C c = this;
+        c.f(); // this does not warn now, but should warn in the future
+        this.f();
+        (this).f();
+    }
+}
+// ----
+// Warning: (204-208): "this" used in constructor. Note that external functions of a contract cannot be called while it is being constructed.
+// Warning: (223-227): "this" used in constructor. Note that external functions of a contract cannot be called while it is being constructed.

test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_mixed_chain_with_params.sol

@@ -0,0 +1,29 @@
+pragma experimental SMTChecker;
+contract F {
+	uint a;
+	constructor(uint x) public {
+		a = x;
+	}
+}
+
+contract E is F {}
+contract D is E {
+	constructor() public {
+		a = 3;
+	}
+}
+contract C is D {}
+contract B is C {
+	constructor(uint x) F(x + 1) public {
+	}
+}
+
+contract A is B {
+	constructor(uint x) B(x) public {
+		assert(a == 3);
+		assert(a == 4);
+	}
+}
+// ----
+// Warning: (234-239): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning: (329-343): Assertion violation happens here

test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init.sol

@@ -0,0 +1,11 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint x = 2;
+	constructor () public {
+		assert(x == 2);
+		assert(x == 3);
+	}
+}
+// ----
+// Warning: (104-118): Assertion violation happens here

test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_base.sol

@@ -0,0 +1,14 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint x = 2;
+}
+
+contract D is C {
+	constructor() public {
+		assert(x == 2);
+		assert(x == 3);
+	}
+}
+// ----
+// Warning: (124-138): Assertion violation happens here

test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain.sol

@@ -0,0 +1,22 @@
+pragma experimental SMTChecker;
+
+contract A {
+	uint x = 1;
+}
+
+contract B is A {
+	constructor() public { x = 2; }
+}
+
+contract C is B {
+	constructor() public { x = 3; }
+}
+
+contract D is C {
+	constructor() public {
+		assert(x == 3);
+		assert(x == 2);
+	}
+}
+// ----
+// Warning: (232-246): Assertion violation happens here

test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain_alternate.sol

@@ -0,0 +1,21 @@
+pragma experimental SMTChecker;
+
+contract A {
+	uint x = 1;
+}
+
+contract B is A {
+	constructor() public { x = 2; }
+}
+
+contract C is B {
+}
+
+contract D is C {
+	constructor() public {
+		assert(x == 2);
+		assert(x == 3);
+	}
+}
+// ----
+// Warning: (199-213): Assertion violation happens here

test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain_run_all.sol

@@ -0,0 +1,27 @@
+pragma experimental SMTChecker;
+contract C {
+	uint a;
+	constructor(uint x) public {
+		a = x;
+	}
+}
+
+contract B is C {
+	uint b;
+	constructor(uint x) public {
+		b = a + x;
+	}
+}
+
+contract A is B {
+	constructor(uint x) B(x) C(x + 2) public {
+		assert(a == x + 2);
+		assert(b == x + x + 2);
+		assert(a == x + 5);
+	}
+}
+
+// ----
+// Warning: (162-167): Underflow (resulting value less than 0) happens here
+// Warning: (162-167): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning: (287-305): Assertion violation happens here

test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain_run_all_2.sol

@@ -0,0 +1,26 @@
+pragma experimental SMTChecker;
+contract C {
+	uint a;
+	constructor(uint x) public {
+		a = x;
+	}
+}
+
+contract B is C {
+	uint b;
+	constructor(uint x) public {
+		b = x + 10;
+	}
+}
+
+contract A is B {
+	constructor(uint x) B(x) C(x + 2) public {
+		assert(a == x + 2);
+		assert(b == x + 10);
+		assert(b == x + 5);
+	}
+}
+
+// ----
+// Warning: (162-168): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning: (285-303): Assertion violation happens here

test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_diamond.sol

@@ -0,0 +1,20 @@
+pragma experimental SMTChecker;
+
+contract A {
+	uint x = 2;
+}
+
+contract B is A {
+}
+
+contract C is A {
+}
+
+contract D is B, C {
+	constructor() public {
+		assert(x == 2);
+		assert(x == 3);
+	}
+}
+// ----
+// Warning: (169-183): Assertion violation happens here

test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_diamond_middle.sol

@@ -0,0 +1,22 @@
+pragma experimental SMTChecker;
+
+contract A {
+	uint x = 1;
+}
+
+contract B is A {
+	constructor() public { x = 2; }
+}
+
+contract C is A {
+	constructor() public { x = 3; }
+}
+
+contract D is B, C {
+	constructor() public {
+		assert(x == 3);
+		assert(x == 4);
+	}
+}
+// ----
+// Warning: (235-249): Assertion violation happens here

test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_function_call.sol

@@ -0,0 +1,17 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint x = f(2);
+	constructor () public {
+		assert(x == 2);
+	}
+
+	function f(uint y) internal view returns (uint) {
+		assert(y > 0);
+		assert(x == 0);
+		return y;
+	}
+}
+// ----
+// Warning: (162-175): Assertion violation happens here
+// Warning: (179-193): Assertion violation happens here

test/libsolidity/smtCheckerTests/inheritance/functions_1.sol

@@ -15,7 +15,7 @@ contract A {
 // 2 warnings, B.f and A.g
 contract B is A {
 	function f() public view override {
-		assert(x == 0);
+		assert(x == 1);
 	}
 }
 // ----

test/libsolidity/smtCheckerTests/inheritance/functions_2.sol

@@ -17,7 +17,7 @@ contract B is A {
 	uint y;
 
 	function f() public view override {
-		assert(x == 0);
+		assert(x == 1);
 	}
 }
 // ----

test/libsolidity/smtCheckerTests/inheritance/functions_3.sol

@@ -17,10 +17,10 @@ contract B is A {
 	uint y;
 
 	function f() public view virtual override {
-		assert(x == 0);
+		assert(x == 1);
 	}
 	function h() public view {
-		assert(x == 2);
+		assert(x == 1);
 	}
 }
 
@@ -29,10 +29,10 @@ contract C is B {
 	uint z;
 
 	function f() public view override {
-		assert(x == 0);
+		assert(x == 1);
 	}
 	function i() public view {
-		assert(x == 0);
+		assert(x == 1);
 	}
 }
 // ----

test/libsolidity/smtCheckerTests/inheritance/implicit_constructor_hierarchy.sol

@@ -0,0 +1,16 @@
+pragma experimental SMTChecker;
+
+contract A {
+	uint x;
+	constructor (uint y) public { assert(x == 0); x = y; }
+}
+
+contract B is A {
+	constructor () A(2) public { assert(x == 2); }
+}
+
+contract C is B {
+	function f() public view {
+		assert(x == 2);
+	}
+}

test/libsolidity/smtCheckerTests/inheritance/implicit_only_constructor_hierarchy.sol

@@ -0,0 +1,20 @@
+pragma experimental SMTChecker;
+
+contract A {
+	uint x;
+	function h() public view {
+		assert(x == 0);
+	}
+}
+
+contract B is A {
+	function g() public view {
+		assert(x == 0);
+	}
+}
+
+contract C is B {
+	function f() public view {
+		assert(x == 0);
+	}
+}

test/libsolidity/smtCheckerTests/special/abi_decode_memory_v2.sol

@@ -3,12 +3,15 @@ pragma experimental "ABIEncoderV2";
 
 contract C {
   struct S { uint x; uint[] b; }
-  function f() public pure returns (S memory, bytes memory) {
+  function f() public pure returns (S memory, bytes memory, uint[][2] memory) {
-    return abi.decode("abc", (S, bytes));
+    return abi.decode("abc", (S, bytes, uint[][2]));
   }
 }
 // ----
 // Warning: (151-159): Assertion checker does not yet support the type of this variable.
-// Warning: (188-191): Assertion checker does not yet implement type abi
+// Warning: (206-209): Assertion checker does not yet implement type abi
-// Warning: (207-208): Assertion checker does not yet implement type type(struct C.S storage pointer)
+// Warning: (225-226): Assertion checker does not yet implement type type(struct C.S storage pointer)
-// Warning: (188-217): Assertion checker does not yet implement this type of function call.
+// Warning: (235-241): Assertion checker does not yet implement type type(uint256[] memory)
+// Warning: (235-241): Assertion checker does not yet implement this expression.
+// Warning: (235-244): Assertion checker does not yet implement type type(uint256[] memory[2] memory)
+// Warning: (206-246): Assertion checker does not yet implement this type of function call.

test/libsolidity/smtCheckerTests/types/data_location_in_function_type.sol

@@ -0,0 +1,5 @@
+pragma experimental SMTChecker;
+library L {
+    struct Nested { uint y; }
+    function c(function(Nested memory) external returns (uint)[] storage) external pure {}
+}

test/libsolidity/smtCheckerTests/types/function_type_array_as_reference_type.sol

@@ -0,0 +1,9 @@
+pragma experimental SMTChecker;
+contract C {
+    struct Nested { uint y; }
+    // ensure that we consider array of function pointers as reference type
+    function b(function(Nested memory) external returns (uint)[] storage) internal pure {}
+    function c(function(Nested memory) external returns (uint)[] memory) public pure {}
+    function d(function(Nested memory) external returns (uint)[] calldata) external pure {}
+}
+// ----

test/libsolidity/smtCheckerTests/types/function_type_arrays.sol

@@ -0,0 +1,14 @@
+pragma experimental SMTChecker;
+contract C {
+    function(uint) external returns (uint)[] public x;
+    function(uint) internal returns (uint)[10] y;
+    function f() view public {
+        function(uint) returns (uint)[10] memory a;
+        function(uint) returns (uint)[10] storage b = y;
+        function(uint) external returns (uint)[] memory c;
+        c = new function(uint) external returns (uint)[](200);
+        a; b;
+    }
+}
+// ----
+// Warning: (361-410): Assertion checker does not yet implement this type of function call.

test/libsolidity/smtCheckerTests/types/mapping_and_array_of_functions.sol

@@ -0,0 +1,7 @@
+pragma experimental SMTChecker;
+contract test {
+    mapping (address => function() internal returns (uint)) a;
+    mapping (address => function() external) b;
+    mapping (address => function() external[]) c;
+    function() external[] d;
+}