Add errorCode list to invariants report

Author: Leo Alt

libsolidity/formal/CHC.cpp

@@ -1746,6 +1746,16 @@ void CHC::checkVerificationTargets()
 			for (auto const& inv: m_invariants.at(pred))
 				msg += inv + "\n";
 		}
+		if (msg.find("<errorCode>") != string::npos)
+		{
+			set<unsigned> seenErrors;
+			for (auto const& target: verificationTargets)
+				if (!seenErrors.count(target.errorId))
+				{
+					seenErrors.insert(target.errorId);
+					msg += "<errorCode> = " + to_string(target.errorId) + " -> " + ModelCheckerTargets::targetTypeToString.at(target.type) + "\n";
+				}
+		}
 		if (!msg.empty())
 			m_errorReporter.info(1180_error, msg);
 	}

libsolidity/formal/ModelCheckerSettings.cpp

@@ -71,6 +71,17 @@ map<string, TargetType> const ModelCheckerTargets::targetStrings{
 	{"outOfBounds", TargetType::OutOfBounds}
 };
 
+map<TargetType, string> const ModelCheckerTargets::targetTypeToString{
+	{TargetType::ConstantCondition, "Constant condition"},
+	{TargetType::Underflow, "Underflow"},
+	{TargetType::Overflow, "Overflow"},
+	{TargetType::DivByZero, "Division by zero"},
+	{TargetType::Balance, "Insufficient balance"},
+	{TargetType::Assert, "Assertion failed"},
+	{TargetType::PopEmptyArray, "Empty array pop"},
+	{TargetType::OutOfBounds, "Out of bounds access"}
+};
+
 std::optional<ModelCheckerTargets> ModelCheckerTargets::fromString(string const& _targets)
 {
 	set<TargetType> chosenTargets;

libsolidity/formal/ModelCheckerSettings.h

@@ -132,6 +132,8 @@ struct ModelCheckerTargets
 
 	static std::map<std::string, VerificationTargetType> const targetStrings;
 
+	static std::map<VerificationTargetType, std::string> const targetTypeToString;
+
 	bool operator!=(ModelCheckerTargets const& _other) const noexcept { return !(*this == _other); }
 	bool operator==(ModelCheckerTargets const& _other) const noexcept { return targets == _other.targets; }