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 #11333 from ethereum/smt_fix_free_functions

Browse Source 
[SMTChecker] Fix ICE in free functions
This commit is contained in:
Leonardo 2021-05-03 14:59:00 +02:00 committed by GitHub
commit fe4822a1d2
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
3 changed files with 51 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
libsolidity/formal/SMTEncoder.cpp
View File

@ -2960,9 +2960,6 @@ vector<smtutil::Expression> SMTEncoder::symbolicArguments(FunctionCall const& _f
void SMTEncoder::collectFreeFunctions(set<SourceUnit const*, ASTNode::CompareByID> const& _sources)
{
if (!m_freeFunctions.empty())
return;
for (auto source: _sources)
for (auto node: source->nodes())
if (auto function = dynamic_cast<FunctionDefinition const*>(node.get()))

23
test/libsolidity/smtCheckerTests/imports/import_free_functions.sol Normal file
View File

@ -0,0 +1,23 @@
==== Source: Address.sol ====
pragma solidity ^0.8.0;
function s() pure {}
==== Source: ERC20.sol ====
pragma solidity ^0.8.0;
import "./Address.sol";
function sub(uint256 a, uint256 b) pure returns (uint256) {
return a - b;
}
contract ERC20 {
mapping (address => uint256) private _balances;
function transferFrom(uint256 amount) public view {
sub(_balances[msg.sender], amount);
}
}
// ====
// SMTEngine: all
// ----
// Warning 3944: (ERC20.sol:121-126): CHC: Underflow (resulting value less than 0) happens here.\nCounterexample:\n\namount = 1\n\nTransaction trace:\nERC20.constructor()\nERC20.transferFrom(1)\n ERC20.sol:sub(0, 1) -- internal call

28
test/libsolidity/smtCheckerTests/imports/import_library_2.sol Normal file
View File

@ -0,0 +1,28 @@
==== Source: Address.sol ====
pragma solidity ^0.8.0;
library Address { function s() internal pure {} }
==== Source: ERC20.sol ====
pragma solidity ^0.8.0;
import "./Address.sol";
library SafeMath {
function sub(uint256 a, uint256 b) internal pure returns (uint256) {
return a - b;
}
}
contract ERC20 {
using SafeMath for uint256;
using Address for address;
mapping (address => uint256) private _balances;
function transferFrom(uint256 amount) public view {
_balances[msg.sender].sub(amount);
}
}
// ====
// SMTEngine: all
// ----
// Warning 3944: (ERC20.sol:157-162): CHC: Underflow (resulting value less than 0) happens here.\nCounterexample:\n\namount = 1\n\nTransaction trace:\nERC20.constructor()\nERC20.transferFrom(1)\n SafeMath.sub(0, 1) -- internal call