cerc-io/solidity
10
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Add CLI and JSON option to show unproved targets

Browse Source
This commit is contained in:
Leo Alt 2021-07-02 14:43:20 +02:00
parent 685d7a8c99
commit 41087f3195
2 changed files with 22 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
libsolidity/interface/StandardCompiler.cpp
View File

@ -442,7 +442,7 @@ std::optional<Json::Value> checkSettingsKeys(Json::Value const& _input)
std::optional<Json::Value> checkModelCheckerSettingsKeys(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"); return checkKeys(_input, keys, "modelChecker");
} }
@ -951,6 +951,14 @@ std::variant<StandardCompiler::InputsAndSettings, Json::Value> StandardCompiler:
ret.modelCheckerSettings.engine = *engine; 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")) if (modelCheckerSettings.isMember("solvers"))
{ {
auto const& solversArray = modelCheckerSettings["solvers"]; auto const& solversArray = modelCheckerSettings["solvers"];

13
solc/CommandLineParser.cpp
View File

@ -87,6 +87,7 @@ static string const g_strMetadataHash = "metadata-hash";
static string const g_strMetadataLiteral = "metadata-literal"; static string const g_strMetadataLiteral = "metadata-literal";
static string const g_strModelCheckerContracts = "model-checker-contracts"; static string const g_strModelCheckerContracts = "model-checker-contracts";
static string const g_strModelCheckerEngine = "model-checker-engine"; 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_strModelCheckerSolvers = "model-checker-solvers";
static string const g_strModelCheckerTargets = "model-checker-targets"; static string const g_strModelCheckerTargets = "model-checker-targets";
static string const g_strModelCheckerTimeout = "model-checker-timeout"; 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"), po::value<string>()->value_name("all,bmc,chc,none")->default_value("none"),
"Select model checker engine." "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(), g_strModelCheckerSolvers.c_str(),
po::value<string>()->value_name("all,cvc4,z3,smtlib2")->default_value("all"), 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; 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)) if (m_args.count(g_strModelCheckerSolvers))
{ {
string solversStr = m_args[g_strModelCheckerSolvers].as<string>(); string solversStr = m_args[g_strModelCheckerSolvers].as<string>();
@ -1129,6 +1141,7 @@ General Information)").c_str(),
m_options.modelChecker.initialize = m_options.modelChecker.initialize =
m_args.count(g_strModelCheckerContracts) || m_args.count(g_strModelCheckerContracts) ||
m_args.count(g_strModelCheckerEngine) || m_args.count(g_strModelCheckerEngine) ||
m_args.count(g_strModelCheckerShowUnproved) ||
m_args.count(g_strModelCheckerSolvers) || m_args.count(g_strModelCheckerSolvers) ||
m_args.count(g_strModelCheckerTargets) || m_args.count(g_strModelCheckerTargets) ||
m_args.count(g_strModelCheckerTimeout); m_args.count(g_strModelCheckerTimeout);