solidity
solidity copied to clipboard
SRI-CSL
This is solc-verify, a modular verifier for Solidity.
``` pragma solidity ^0.5.0; contract test { function g() public returns (uint) { return block.timestamp; } } ----------------- test::[implicit_constructor]: OK test::g: SKIPPED Use --show-warnings to see 2 warnings. Some functions...
Currently the helper function for default values returns simply an expression. However, in many cases default values have side effects: e.g., allocation, element/member initialization, which is currently done "manually" all...
```solidity pragma solidity ^0.5.0; contract Test { function test(uint n) public pure { require(n > 0); int[] memory a = new int[](1); delete a; assert(a.length == 0); } } ```...
```solidity contract Test { struct S { int x; } function test() { S[2][3] memory a; assert(a.length == 3); assert(a[0].length == 2); assert(a[1].length == 2); assert(a[0][0].x == 0); assert(a[1][0].x ==...
How can I write solc-verify annotations for the following function to specify that the function reverts when `a>=10`? ``` contract test { function add(uint256 a) public pure returns (uint256) {...
Can solc-verify handle the [ecrecover](https://solidity.readthedocs.io/en/latest/units-and-global-variables.html#mathematical-and-cryptographic-functions) function? For example, how I can write annotations that specify that this function returns the recovered address if the signature components are valid and otherwise...
``` $ cat a.sol && solc-verify.py a.sol pragma solidity ^0.5.0; contract A { /// @notice postcondition address(this).balance >= __verifier_old_uint(address(this).balance) function f1() public payable { } } A::f1: ERROR - a.sol:6:5:...
While #57 was fixed by havocing the variables, the developer can still introduce inconsistencies (e.g. by mistake) with the postconditions of unimplemented/skipped functions: ```solidity contract C { int x; function...
```solidity pragma solidity >=0.5.0; contract Test { struct S { int x; } S[] m_a; function test() external view { S[] memory a; a = m_a; } } ``` Gives...
When we resize an array by assigning to length, the new elements are not set to their default value (except in the constructor). We should give at least give a...