solidity
solidity copied to clipboard
SRI-CSL
This is solc-verify, a modular verifier for Solidity.
```solidity pragma solidity >=0.5.0; contract DanglingStorage { int[][] baz; function() external payable { baz.length = 10; baz[0].length = 10; int x = baz[0][0]; int[] storage bar = baz[0]; baz.length =...
Currently, the `if` part of a `modifies` spec is directly translated into a postcondition, meaning that it will refer to the new values (unless manually adding `old(...)`). As discussed in...
While we can add specs to libraries with local storage pointers, modifies specs are not yet working for them, because they are bound to state variables. Seems to be extendable...
Currently we have two old(...) expressions, taking/returning int256 and int256 respectively, casting smaller integers to bigger ones. This might cause problems as demonstrated by the example: ```solidity pragma solidity>=0.5.0; contract...
Depending on the target of verification, the postcondition of `setB0` might or might not hold. ```solidity pragma solidity >=0.5.0; contract A { struct S { int x; } function setA0(S...
For example libsolidity/syntaxTests/parsing/scientific_notation.sol ?? [0.076 s]
In `test/libsolidity/syntaxTests/specialFunctions/abidecode/abi_decode_memory_v2.sol` ```solidity pragma experimental "ABIEncoderV2"; contract C { struct S { uint x; uint[] b; } function f() public pure returns (S memory, bytes memory, uint[][2] memory) { return...
Using functions as getters is quite common and it would be good to support them in specs, such as `modifies` or `require`. The following currently fails for two reasons: 1....
In many syntax examples there are recursive struct definitions where we currently fail with a segmentation fault. - `test/libsolidity/syntaxTests/parsing/mapping_in_struct.sol`: mapping value type is the structure containing the mapping ```solidity contract...
This issues tracks all yet unsupported features, with notes. Fixes or discussion for individual issues in separate issues. ### Solidity Features #### Function types Error: `Boogie error: Unsupported type: 'function'`...