SRI-CSL / solidity

This is solc-verify, a modular verifier for Solidity.
https://github.com/SRI-CSL/solidity/blob/boogie/SOLC-VERIFY-README.md
GNU General Public License v3.0
50 stars 14 forks source link

Implicit constructor for libraries #142

Closed hajduakos closed 4 years ago

hajduakos commented 4 years ago

We seem to generate an implicit constructor for every contract node, even if its kind is a library. I think we can remove it from libraries as they do not have any state. It does not harm, but introduces a confusing line on the output:

library MathLib {
    function add(uint256 a, uint256 b) internal pure returns (uint256) { return a + b; }
}

contract Library {
    using MathLib for uint256;
    // ...
}
$ solc-verify.py basic/Library.sol
MathLib::[implicit_constructor]: OK  <--- What???
Library::[fallback]: OK
Library::[implicit_constructor]: OK
No errors found.
hajduakos commented 4 years ago

It is actually possible to call a library's constructor (for deployment, see #15). I think we can just inline them, in this case they will not appear in the output.

dddejan commented 4 years ago

It is actually possible to call a library's constructor (for deployment, see #15). I think we can just inline them, in this case they will not appear in the output.

Seems simplest. There is no actual constructor for libraries, so you could just skip it. The new statement will deploy the code and return the address, but that's it.

hajduakos commented 4 years ago

Done in 2be98d6f3474217aa9605fc1ec2932f1563fffe0. Currently, I still generate and call the (empty method), but I inline it so it does not appear as a "proved" function in the output. This makes the transformation more uniform and easier. But later we might just completely remove it.