mirror of
https://github.com/ethereum/solidity
synced 2023-10-03 13:03:40 +00:00
b0419da654
Previously, we did not remember trusted external calls for later phase when we compute possible verification targets for each function. This led to false negative in cases where verification target can be violated, but not by calling a public function directly, but only when it is called as an external function from other function. The added test cases witnesses this behaviour. The underflow in `dec` cannot happen in any other way except what the `dec` is called from `f`. The same problem did not occur when the functions are called internally, because for such cases, we have already been remembering these calls in the callgraph in the CHC engine. |
||
|---|---|---|
| .. | ||
| deploy_bmc_trusted.sol | ||
| deploy_bmc_untrusted.sol | ||
| deploy_trusted_addresses.sol | ||
| deploy_trusted_flow.sol | ||
| deploy_trusted_keep_storage_constraints.sol | ||
| deploy_trusted_state_flow_2.sol | ||
| deploy_trusted_state_flow_3.sol | ||
| deploy_trusted_state_flow_4.sol | ||
| deploy_trusted_state_flow.sol | ||
| deploy_trusted.sol | ||
| deploy_untrusted_addresses.sol | ||
| deploy_untrusted_erase_storage_constraints.sol | ||
| deploy_untrusted.sol | ||
| deployment_trusted_with_value_1.sol | ||