mirror of
https://github.com/ethereum/solidity
synced 2023-10-03 13:03:40 +00:00
fix abstract nondet exception
This commit is contained in:
parent
665bf29a84
commit
db9c11a2a5
@ -8,6 +8,7 @@ Compiler Features:
|
|||||||
|
|
||||||
|
|
||||||
Bugfixes:
|
Bugfixes:
|
||||||
|
* SMTChecker: Fix internal error when using the custom NatSpec annotation to abstract free functions.
|
||||||
* TypeChecker: Also allow external library functions in ``using for``.
|
* TypeChecker: Also allow external library functions in ``using for``.
|
||||||
|
|
||||||
|
|
||||||
|
@ -2897,7 +2897,9 @@ vector<VariableDeclaration const*> SMTEncoder::stateVariablesIncludingInheritedA
|
|||||||
|
|
||||||
vector<VariableDeclaration const*> SMTEncoder::stateVariablesIncludingInheritedAndPrivate(FunctionDefinition const& _function)
|
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)
|
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);
|
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<frontend::Expression>>> SMTEncoder::baseArguments(ContractDefinition const& _contract)
|
||||||
{
|
{
|
||||||
map<ContractDefinition const*, vector<ASTPointer<Expression>>> baseArgs;
|
map<ContractDefinition const*, vector<ASTPointer<Expression>>> baseArgs;
|
||||||
|
@ -113,9 +113,6 @@ public:
|
|||||||
/// @returns the ModifierDefinition of a ModifierInvocation if possible, or nullptr.
|
/// @returns the ModifierDefinition of a ModifierInvocation if possible, or nullptr.
|
||||||
static ModifierDefinition const* resolveModifierInvocation(ModifierInvocation const& _invocation, ContractDefinition const* _contract);
|
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.
|
/// @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);
|
std::map<ContractDefinition const*, std::vector<ASTPointer<frontend::Expression>>> baseArguments(ContractDefinition const& _contract);
|
||||||
|
|
||||||
|
@ -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.
|
Loading…
Reference in New Issue
Block a user