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

Fix error in SMTChecker: Use rich indentifier instead of external identifier to ecnode member access to functions

Browse Source
This commit is contained in:
Pawel Gebal 2023-06-20 19:38:30 +02:00
parent b26090c288
commit 826fd90dcf
3 changed files with 20 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
Changelog.md
View File

@ -20,6 +20,7 @@ Bugfixes:
* Commandline Interface: It is no longer possible to specify both ``--optimize-yul`` and ``--no-optimize-yul`` at the same time. * Commandline Interface: It is no longer possible to specify both ``--optimize-yul`` and ``--no-optimize-yul`` at the same time.
* SMTChecker: Fix encoding of side-effects inside ``if`` and ``ternary conditional``statements in the BMC engine. * SMTChecker: Fix encoding of side-effects inside ``if`` and ``ternary conditional``statements in the BMC engine.
* SMTChecker: Fix false negative when a verification target can be violated only by trusted external call from another public function. * SMTChecker: Fix false negative when a verification target can be violated only by trusted external call from another public function.
* SMTChecker: Fix internal error caused by using external identifier to encode member access to functions that take an internal function as a parameter.
* Standard JSON Interface: Fix an incomplete AST being returned when analysis is interrupted by certain kinds of fatal errors. * Standard JSON Interface: Fix an incomplete AST being returned when analysis is interrupted by certain kinds of fatal errors.
* Yul Optimizer: Ensure that the assignment of memory slots for variables moved to memory does not depend on AST IDs that may depend on whether additional files are included during compilation. * Yul Optimizer: Ensure that the assignment of memory slots for variables moved to memory does not depend on AST IDs that may depend on whether additional files are included during compilation.
* Yul Optimizer: Fix optimized IR being unnecessarily passed through the Yul optimizer again before bytecode generation. * Yul Optimizer: Fix optimized IR being unnecessarily passed through the Yul optimizer again before bytecode generation.

6
libsolidity/formal/SMTEncoder.cpp
View File

@ -33,6 +33,7 @@
#include <liblangutil/CharStreamProvider.h> #include <liblangutil/CharStreamProvider.h>
#include <libsolutil/Algorithms.h> #include <libsolutil/Algorithms.h>
#include <libsolutil/FunctionSelector.h>
#include <range/v3/view.hpp> #include <range/v3/view.hpp>
@ -1358,7 +1359,10 @@ bool SMTEncoder::visit(MemberAccess const& _memberAccess)
{ {
auto const* functionType = dynamic_cast<FunctionType const*>(_memberAccess.annotation().type); auto const* functionType = dynamic_cast<FunctionType const*>(_memberAccess.annotation().type);
if (functionType && functionType->hasDeclaration()) if (functionType && functionType->hasDeclaration())
defineExpr(_memberAccess, functionType->externalIdentifier()); defineExpr(
_memberAccess,
util::selectorFromSignatureU32(functionType->richIdentifier())
);
return true; return true;
} }

14
test/libsolidity/smtCheckerTests/functions/functions_library_internal.sol Normal file
View File

@ -0,0 +1,14 @@
library L {
function value(function()internal a, uint256 b) internal {}
}
contract C {
using L for function()internal;
function f() public {
function()internal x;
x.value(42);
}
}
// ====
// SMTEngine: all
// ----