Add CLI and JSON option to show unproved targets

Author: Leo Alt

libsolidity/interface/StandardCompiler.cpp

@@ -442,7 +442,7 @@ std::optional<Json::Value> checkSettingsKeys(Json::Value const& _input)
 
 std::optional<Json::Value> checkModelCheckerSettingsKeys(Json::Value const& _input)
 {
-	static set<string> keys{"contracts", "engine", "solvers", "targets", "timeout"};
+	static set<string> keys{"contracts", "engine", "showUnproved", "solvers", "targets", "timeout"};
 	return checkKeys(_input, keys, "modelChecker");
 }
 
@@ -951,6 +951,14 @@ std::variant<StandardCompiler::InputsAndSettings, Json::Value> StandardCompiler:
 		ret.modelCheckerSettings.engine = *engine;
 	}
 
+	if (modelCheckerSettings.isMember("showUnproved"))
+	{
+		auto const& showUnproved = modelCheckerSettings["showUnproved"];
+		if (!showUnproved.isBool())
+			return formatFatalError("JSONError", "settings.modelChecker.showUnproved must be a Boolean value.");
+		ret.modelCheckerSettings.showUnproved = showUnproved.asBool();
+	}
+	
 	if (modelCheckerSettings.isMember("solvers"))
 	{
 		auto const& solversArray = modelCheckerSettings["solvers"];

solc/CommandLineParser.cpp

@@ -87,6 +87,7 @@ static string const g_strMetadataHash = "metadata-hash";
 static string const g_strMetadataLiteral = "metadata-literal";
 static string const g_strModelCheckerContracts = "model-checker-contracts";
 static string const g_strModelCheckerEngine = "model-checker-engine";
+static string const g_strModelCheckerShowUnproved = "model-checker-show-unproved";
 static string const g_strModelCheckerSolvers = "model-checker-solvers";
 static string const g_strModelCheckerTargets = "model-checker-targets";
 static string const g_strModelCheckerTimeout = "model-checker-timeout";
@@ -724,6 +725,11 @@ General Information)").c_str(),
 			po::value<string>()->value_name("all,bmc,chc,none")->default_value("none"),
 			"Select model checker engine."
 		)
+		(
+			g_strModelCheckerShowUnproved.c_str(),
+			po::value<bool>()->value_name("false,true")->default_value(false),
+			"Select whether to show all unproved targets."
+		)
 		(
 			g_strModelCheckerSolvers.c_str(),
 			po::value<string>()->value_name("all,cvc4,z3,smtlib2")->default_value("all"),
@@ -1098,6 +1104,12 @@ General Information)").c_str(),
 		m_options.modelChecker.settings.engine = *engine;
 	}
 
+	if (m_args.count(g_strModelCheckerShowUnproved))
+	{
+		bool showUnproved = m_args[g_strModelCheckerShowUnproved].as<bool>();
+		m_options.modelChecker.settings.showUnproved = showUnproved;
+	}
+
 	if (m_args.count(g_strModelCheckerSolvers))
 	{
 		string solversStr = m_args[g_strModelCheckerSolvers].as<string>();
@@ -1129,6 +1141,7 @@ General Information)").c_str(),
 	m_options.modelChecker.initialize =
 		m_args.count(g_strModelCheckerContracts) ||
 		m_args.count(g_strModelCheckerEngine) ||
+		m_args.count(g_strModelCheckerShowUnproved) ||
 		m_args.count(g_strModelCheckerSolvers) ||
 		m_args.count(g_strModelCheckerTargets) ||
 		m_args.count(g_strModelCheckerTimeout);