From 287ea63cde980e3b520857eee7729508644f6b3f Mon Sep 17 00:00:00 2001
From: Leo Alt <leo@ethereum.org>
Date: Tue, 12 Oct 2021 11:17:52 +0200
Subject: [PATCH] Create setting for trusted/untrusted external calls

---
 libsolidity/formal/ModelCheckerSettings.cpp |  9 +++++++++
 libsolidity/formal/ModelCheckerSettings.h   | 17 +++++++++++++++++
 2 files changed, 26 insertions(+)

diff --git a/libsolidity/formal/ModelCheckerSettings.cpp b/libsolidity/formal/ModelCheckerSettings.cpp
index 274571a15..d1e383d63 100644
--- a/libsolidity/formal/ModelCheckerSettings.cpp
+++ b/libsolidity/formal/ModelCheckerSettings.cpp
@@ -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 {};
+}
diff --git a/libsolidity/formal/ModelCheckerSettings.h b/libsolidity/formal/ModelCheckerSettings.h
index e3e93fcf4..2b17fa3b7 100644
--- a/libsolidity/formal/ModelCheckerSettings.h
+++ b/libsolidity/formal/ModelCheckerSettings.h
@@ -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 &&