cerc-io/solidity
11
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

Create setting for trusted/untrusted external calls

Browse Source
This commit is contained in:
Leo Alt 2021-10-12 11:17:52 +02:00
parent 37f6dc1f88
commit 287ea63cde
2 changed files with 26 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
libsolidity/formal/ModelCheckerSettings.cpp
View File

@ -130,3 +130,12 @@ std::optional<ModelCheckerContracts> ModelCheckerContracts::fromString(string co
return ModelCheckerContracts{chosen};
}
std::optional<ModelCheckerExtCalls> ModelCheckerExtCalls::fromString(string const& _mode)
{
if (_mode == "untrusted")
return ModelCheckerExtCalls{Mode::UNTRUSTED};
if (_mode == "trusted")
return ModelCheckerExtCalls{Mode::TRUSTED};
return {};
}

17
libsolidity/formal/ModelCheckerSettings.h
View File

@ -140,6 +140,21 @@ struct ModelCheckerTargets
std::set<VerificationTargetType> targets;
};
struct ModelCheckerExtCalls
{
enum class Mode
{
UNTRUSTED,
TRUSTED
};
Mode mode = Mode::UNTRUSTED;
static std::optional<ModelCheckerExtCalls> fromString(std::string const& _mode);
bool isTrusted() const { return mode == Mode::TRUSTED; }
};
struct ModelCheckerSettings
{
ModelCheckerContracts contracts = ModelCheckerContracts::Default();
@ -151,6 +166,7 @@ struct ModelCheckerSettings
/// might prefer the precise encoding.
bool divModNoSlacks = false;
ModelCheckerEngine engine = ModelCheckerEngine::None();
ModelCheckerExtCalls externalCalls = {};
ModelCheckerInvariants invariants = ModelCheckerInvariants::Default();
bool showUnproved = false;
smtutil::SMTSolverChoice solvers = smtutil::SMTSolverChoice::All();
@ -164,6 +180,7 @@ struct ModelCheckerSettings
contracts == _other.contracts &&
divModNoSlacks == _other.divModNoSlacks &&
engine == _other.engine &&
externalCalls.mode == _other.externalCalls.mode &&
invariants == _other.invariants &&
showUnproved == _other.showUnproved &&
solvers == _other.solvers &&