aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--Changelog.md1
-rw-r--r--libsolidity/formal/SMTChecker.cpp12
-rw-r--r--test/libsolidity/smtCheckerTests/functions/functions_bound_1.sol19
-rw-r--r--test/libsolidity/smtCheckerTests/functions/functions_bound_1_fail.sol21
-rw-r--r--test/libsolidity/smtCheckerTests/functions/functions_library_1.sol18
-rw-r--r--test/libsolidity/smtCheckerTests/functions/functions_library_1_fail.sol20
6 files changed, 91 insertions, 0 deletions
diff --git a/Changelog.md b/Changelog.md
index fae28bb7..197419fa 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -8,6 +8,7 @@ Compiler Features:
* Code generator: Do not perform redundant double cleanup on unsigned integers when loading from calldata.
* SMTChecker: Support ``msg``, ``tx`` and ``block`` member variables.
* SMTChecker: Support ``gasleft()`` and ``blockhash()`` functions.
+ * SMTChecker: Support internal bound function calls.
Bugfixes:
diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index 9a2b9bbf..bbc78c0c 100644
--- a/libsolidity/formal/SMTChecker.cpp
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -457,6 +457,14 @@ void SMTChecker::inlineFunctionCall(FunctionCall const& _funCall)
else if (_funDef && _funDef->isImplemented())
{
vector<smt::Expression> funArgs;
+ auto const& funType = dynamic_cast<FunctionType const*>(_calledExpr->annotation().type.get());
+ solAssert(funType, "");
+ if (funType->bound())
+ {
+ auto const& boundFunction = dynamic_cast<MemberAccess const*>(_calledExpr);
+ solAssert(boundFunction, "");
+ funArgs.push_back(expr(boundFunction->expression()));
+ }
for (auto arg: _funCall.arguments())
funArgs.push_back(expr(*arg));
initializeFunctionCallParameters(*_funDef, funArgs);
@@ -548,6 +556,10 @@ void SMTChecker::endVisit(Return const& _return)
bool SMTChecker::visit(MemberAccess const& _memberAccess)
{
+ auto const& accessType = _memberAccess.annotation().type;
+ if (accessType->category() == Type::Category::Function)
+ return true;
+
auto const& exprType = _memberAccess.expression().annotation().type;
solAssert(exprType, "");
if (exprType->category() == Type::Category::Magic)
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_bound_1.sol b/test/libsolidity/smtCheckerTests/functions/functions_bound_1.sol
new file mode 100644
index 00000000..5e9722de
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/functions_bound_1.sol
@@ -0,0 +1,19 @@
+pragma experimental SMTChecker;
+
+library L
+{
+ function add(uint x, uint y) internal pure returns (uint) {
+ require(x < 1000);
+ require(y < 1000);
+ return x + y;
+ }
+}
+
+contract C
+{
+ using L for uint;
+ function f(uint x) public pure {
+ uint y = x.add(999);
+ assert(y < 10000);
+ }
+}
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_bound_1_fail.sol b/test/libsolidity/smtCheckerTests/functions/functions_bound_1_fail.sol
new file mode 100644
index 00000000..99c785d0
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/functions_bound_1_fail.sol
@@ -0,0 +1,21 @@
+pragma experimental SMTChecker;
+
+library L
+{
+ function add(uint x, uint y) internal pure returns (uint) {
+ require(x < 1000);
+ require(y < 1000);
+ return x + y;
+ }
+}
+
+contract C
+{
+ using L for uint;
+ function f(uint x) public pure {
+ uint y = x.add(999);
+ assert(y < 1000);
+ }
+}
+// ----
+// Warning: (261-277): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_library_1.sol b/test/libsolidity/smtCheckerTests/functions/functions_library_1.sol
new file mode 100644
index 00000000..2ceb9e60
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/functions_library_1.sol
@@ -0,0 +1,18 @@
+pragma experimental SMTChecker;
+
+library L
+{
+ function add(uint x, uint y) internal pure returns (uint) {
+ require(x < 1000);
+ require(y < 1000);
+ return x + y;
+ }
+}
+
+contract C
+{
+ function f(uint x) public pure {
+ uint y = L.add(x, 999);
+ assert(y < 10000);
+ }
+}
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_library_1_fail.sol b/test/libsolidity/smtCheckerTests/functions/functions_library_1_fail.sol
new file mode 100644
index 00000000..32419700
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/functions_library_1_fail.sol
@@ -0,0 +1,20 @@
+pragma experimental SMTChecker;
+
+library L
+{
+ function add(uint x, uint y) internal pure returns (uint) {
+ require(x < 1000);
+ require(y < 1000);
+ return x + y;
+ }
+}
+
+contract C
+{
+ function f(uint x) public pure {
+ uint y = L.add(x, 999);
+ assert(y < 1000);
+ }
+}
+// ----
+// Warning: (245-261): Assertion violation happens here