Do not analyze unecessary contracts

libsolidity/formal/CHC.cpp

@@ -78,6 +78,9 @@ CHC::CHC(
 
 void CHC::analyze(SourceUnit const& _source)
 {
+	if (!shouldAnalyze(_source))
+		return;
+
 	if (!m_settings.solvers.z3 && !m_settings.solvers.smtlib2)
 	{
 		if (!m_noSolverWarning)
@@ -137,6 +140,9 @@ vector<string> CHC::unhandledQueries() const
 
 bool CHC::visit(ContractDefinition const& _contract)
 {
+	if (!shouldAnalyze(_contract))
+		return false;
+
 	resetContractAnalysis();
 	initContract(_contract);
 	clearIndices(&_contract);
@@ -152,6 +158,9 @@ bool CHC::visit(ContractDefinition const& _contract)
 
 void CHC::endVisit(ContractDefinition const& _contract)
 {
+	if (!shouldAnalyze(_contract))
+		return;
+
 	for (auto base: _contract.annotation().linearizedBaseContracts)
 	{
 		if (auto constructor = base->constructor())

libsolidity/formal/SMTEncoder.cpp

@@ -1035,6 +1035,12 @@ void SMTEncoder::visitPublicGetter(FunctionCall const& _funCall)
 	}
 }
 
+bool SMTEncoder::shouldAnalyze(SourceUnit const& _source) const
+{
+	return m_settings.contracts.isDefault() ||
+		m_settings.contracts.has(*_source.annotation().path);
+}
+
 bool SMTEncoder::shouldAnalyze(ContractDefinition const& _contract) const
 {
 	if (!_contract.canBeDeployed())

libsolidity/formal/SMTEncoder.h

@@ -223,6 +223,8 @@ protected:
 	/// @returns true if @param _contract is set for analysis in the settings
 	/// and it is not abstract.
 	bool shouldAnalyze(ContractDefinition const& _contract) const;
+	/// @returns true if @param _source is set for analysis in the settings.
+	bool shouldAnalyze(SourceUnit const& _source) const;
 
 	bool isPublicGetter(Expression const& _expr);
 

test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_ext_calls.sol

@@ -16,5 +16,5 @@ contract C {
 // ----
 // Warning 1218: (131-165): CHC: Error trying to invoke SMT solver.
 // Warning 6328: (131-165): CHC: Assertion violation might happen here.
-// Info 1180: Reentrancy property(ies) for :C:\n(!(<errorCode> >= 2) && (((:var 1).balances[address(this)] + ((- 1) * (:var 0).balances[address(this)])) <= 0))\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(address(this).balance == x)\n<errorCode> = 2 -> Assertion failed at assert(address(this).balance >= x)\n
+// Info 1180: Reentrancy property(ies) for :C:\n(!(<errorCode> >= 2) && (((:var 0).balances[address(this)] + ((- 1) * (:var 1).balances[address(this)])) >= 0))\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(address(this).balance == x)\n<errorCode> = 2 -> Assertion failed at assert(address(this).balance >= x)\n
 // Warning 4661: (131-165): BMC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/blockchain_state/this_does_not_change_external_call.sol

@@ -17,5 +17,4 @@ contract C {
 // ====
 // SMTEngine: all
 // SMTIgnoreOS: macos
-// ----
+// SMTIgnoreInv: yes
-// Info 1180: Contract invariant(s) for :C:\n(((address(this) + ((- 1) * t)) <= 0) && ((address(this) + ((- 1) * t)) >= 0))\nReentrancy property(ies) for :C:\n((!((t + ((- 1) * address(this))) = 0) || (<errorCode> <= 0)) && (!((t + ((- 1) * address(this))) <= 0) || ((t' + ((- 1) * address(this))) <= 0)) && (!((t + ((- 1) * address(this))) >= 0) || ((address(this) + ((- 1) * t')) <= 0)))\n((!(<errorCode> >= 2) || !((t + ((- 1) * address(this))) = 0)) && (!((t + ((- 1) * address(this))) <= 0) || ((t' + ((- 1) * address(this))) <= 0)) && (!((t + ((- 1) * address(this))) >= 0) || ((address(this) + ((- 1) * t')) <= 0)))\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(address(this) == t)\n<errorCode> = 2 -> Assertion failed at assert(a == t)\n

test/libsolidity/smtCheckerTests/control_flow/branches_with_return/constructor_state_variable_init_chain_alternate.sol

@@ -24,5 +24,6 @@ contract D is C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: yes
 // ----
-// Warning 6328: (286-300): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\na = 1\n\nTransaction trace:\nD.constructor(1)
+// Warning 6328: (286-300): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/external_calls/external_call_with_value_2.sol

@@ -14,5 +14,5 @@ contract C {
 // SMTEngine: all
 // ----
 // Warning 6328: (150-186): CHC: Assertion violation might happen here.
-// Warning 6328: (205-240): CHC: Assertion violation happens here.
+// Warning 6328: (205-240): CHC: Assertion violation happens here.\nCounterexample:\n\ni = 0\n\nTransaction trace:\nC.constructor()\nC.g(0)\n    i.f{value: 0}() -- untrusted external call
 // Warning 4661: (150-186): BMC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/functions/functions_external_2.sol

@@ -25,4 +25,4 @@ contract C
 // SMTIgnoreOS: macos
 // ----
 // Warning 6328: (234-253): CHC: Assertion violation happens here.
-// Info 1180: Reentrancy property(ies) for :C:\n!(<errorCode> = 1)\n((!((map[1] + ((- 1) * map[0])) >= 0) || ((map'[0] + ((- 1) * map'[1])) <= 0)) && !(<errorCode> = 2) && (!((map[1] + ((- 1) * map[0])) <= 0) || ((map'[1] + ((- 1) * map'[0])) <= 0)))\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(map[0] == map[1])\n<errorCode> = 2 -> Assertion failed at assert(map[0] == map[1])\n<errorCode> = 3 -> Assertion failed at assert(map[0] == 0)\n
+// Info 1180: Reentrancy property(ies) for :C:\n!(<errorCode> = 1)\n((!((map[1] + ((- 1) * map[0])) >= 0) || ((map'[0] + ((- 1) * map'[1])) <= 0)) && (((map'[1] + ((- 1) * map'[0])) <= 0) || !((map[1] + ((- 1) * map[0])) <= 0)) && !(<errorCode> = 2))\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(map[0] == map[1])\n<errorCode> = 2 -> Assertion failed at assert(map[0] == map[1])\n<errorCode> = 3 -> Assertion failed at assert(map[0] == 0)\n

test/libsolidity/smtCheckerTests/operators/conditional_assignment_6.sol

@@ -25,4 +25,4 @@ contract C {
 // SMTIgnoreOS: macos
 // ----
 // Warning 2072: (255-261): Unused local variable.
-// Info 1180: Reentrancy property(ies) for :C:\n((!(x' >= 3) || (a' = a)) && (!(x' <= 0) || !(x >= 2)) && (<errorCode> <= 0) && (!(x <= 2) || !(x' >= 3)))\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(x == 2 || x == 1)\n
+// Info 1180: Reentrancy property(ies) for :C:\n((!(x <= 2) || !(x' >= 3)) && (<errorCode> <= 0) && (!(x' <= 0) || !(x >= 2)))\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(x == 2 || x == 1)\n

test/libsolidity/smtCheckerTests/special/tx_vars_reentrancy_1.sol

@@ -13,4 +13,4 @@ contract C {
 // SMTEngine: all
 // SMTIgnoreOS: macos
 // ----
-// Warning 6328: (135-169): CHC: Assertion violation happens here.\nCounterexample:\n\n_i = 0\nx = 1236\n\nTransaction trace:\nC.constructor()\nC.g(0){ msg.value: 38 }\n    _i.f() -- untrusted external call, synthesized as:\n        C.g(0){ msg.value: 1 } -- reentrant call\n            _i.f() -- untrusted external call
+// Warning 6328: (135-169): CHC: Assertion violation happens here.\nCounterexample:\n\n_i = 0\nx = 2997\n\nTransaction trace:\nC.constructor()\nC.g(0){ msg.value: 2803 }\n    _i.f() -- untrusted external call, synthesized as:\n        C.g(0){ msg.value: 32278 } -- reentrant call\n            _i.f() -- untrusted external call

test/libsolidity/smtCheckerTests/special/tx_vars_reentrancy_2.sol

@@ -13,4 +13,4 @@ contract C {
 // SMTEngine: all
 // SMTIgnoreOS: macos
 // ----
-// Warning 6328: (157-191): CHC: Assertion violation happens here.\nCounterexample:\n\n_i = 0\nx = 101\n\nTransaction trace:\nC.constructor()\nC.g(0){ msg.value: 69 }\n    _i.f{ value: 100 }() -- untrusted external call
+// Warning 6328: (157-191): CHC: Assertion violation happens here.\nCounterexample:\n\n_i = 0\nx = 101\n\nTransaction trace:\nC.constructor()\nC.g(0){ msg.value: 83 }\n    _i.f{ value: 100 }() -- untrusted external call