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

Merge pull request #13952 from ethereum/fix-abstract-nondet

Browse Source 
fix abstract nondet exception
This commit is contained in:
Daniel 2023-02-08 19:39:19 +01:00 committed by GitHub
commit d33f2734b6
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
4 changed files with 21 additions and 12 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
Changelog.md
View File

@ -8,6 +8,7 @@ Compiler Features:
Bugfixes:
* SMTChecker: Fix internal error when using the custom NatSpec annotation to abstract free functions.
* TypeChecker: Also allow external library functions in ``using for``.

12
libsolidity/formal/SMTEncoder.cpp
View File

@ -2897,7 +2897,9 @@ vector<VariableDeclaration const*> SMTEncoder::stateVariablesIncludingInheritedA
vector<VariableDeclaration const*> SMTEncoder::stateVariablesIncludingInheritedAndPrivate(FunctionDefinition const& _function)
{
return stateVariablesIncludingInheritedAndPrivate(dynamic_cast<ContractDefinition const&>(*_function.scope()));
if (auto contract = dynamic_cast<ContractDefinition const*>(_function.scope()))
return stateVariablesIncludingInheritedAndPrivate(*contract);
return {};
}
vector<VariableDeclaration const*> SMTEncoder::localVariablesIncludingModifiers(FunctionDefinition const& _function, ContractDefinition const* _contract)
@ -3020,14 +3022,6 @@ set<FunctionDefinition const*, ASTNode::CompareByID> const& SMTEncoder::contract
return m_contractFunctionsWithoutVirtual.at(&_contract);
}
SourceUnit const* SMTEncoder::sourceUnitContaining(Scopable const& _scopable)
{
for (auto const* s = &_scopable; s; s = dynamic_cast<Scopable const*>(s->scope()))
if (auto const* source = dynamic_cast<SourceUnit const*>(s->scope()))
return source;
solAssert(false, "");
}
map<ContractDefinition const*, vector<ASTPointer<frontend::Expression>>> SMTEncoder::baseArguments(ContractDefinition const& _contract)
{
map<ContractDefinition const*, vector<ASTPointer<Expression>>> baseArgs;

3
libsolidity/formal/SMTEncoder.h
View File

@ -113,9 +113,6 @@ public:
/// @returns the ModifierDefinition of a ModifierInvocation if possible, or nullptr.
static ModifierDefinition const* resolveModifierInvocation(ModifierInvocation const& _invocation, ContractDefinition const* _contract);
/// @returns the SourceUnit that contains _scopable.
static SourceUnit const* sourceUnitContaining(Scopable const& _scopable);
/// @returns the arguments for each base constructor call in the hierarchy of @a _contract.
std::map<ContractDefinition const*, std::vector<ASTPointer<frontend::Expression>>> baseArguments(ContractDefinition const& _contract);

17
test/libsolidity/smtCheckerTests/natspec/abstract_free_function_1.sol Normal file
View File

@ -0,0 +1,17 @@
// SPDX-License-Identifier: MIT
pragma solidity >=0.8.13;
contract C {
function f(uint x) external pure {
uint t = msb(x);
assert(t == 0); // should fail
}
}
/// @custom:smtchecker abstract-function-nondet
function msb(uint256 x) pure returns (uint256 result) {}
// ====
// SMTEngine: chc
// ----
// Warning 6328: (144-158): CHC: Assertion violation happens here.