solidity
solidity copied to clipboard
SRI-CSL
This is solc-verify, a modular verifier for Solidity.
```solidity pragma solidity >=0.5.0; contract A { function f(uint x, uint y, uint m) public returns (uint r) { r = addmod(x, y, m); } } ``` Currently gives ```console...
```solidity pragma solidity >=0.5.0; contract A { constructor() public payable {} } contract B { A a; constructor() public payable { a = (new A).value(msg.value)(); } } ``` Gives ```console...
```solidity pragma solidity >=0.5.0; contract A { address public constant owner = address(0x0CD95a59fAd089c4EBCCEB54f335eC8f61Caa80e); } contract B { A a; function f() public view returns (address b) { b = a.owner();...
```solidity pragma solidity >=0.5.0; contract A { modifier m(string memory msg) { _; } function f() public m("heyheyhey") {} } ``` gives ```console $ solc-verify.py modifier_string.sol --output . Error while...
We now have a type error in boogie to fix: ``` ./solc-verify.py test/libsolidity/syntaxTests/types/rational_number_huge.sol --output . Error while running verifier, details: Parsing ./rational_number_huge.sol.bpl ./rational_number_huge.sol.bpl(16,5): Error: command assigns to an immutable variable:...
There is a Truffle test failing (`Payable.sol`). I isolated the issue, and seems like `address(this).balance` generates an invalid opcode. Even the following very simple example fails with Truffle: ```solidity pragma...
Return variables should be initialized to default value: ```solidity contract Ret { function f() public pure returns (int x) { // Returns 0 by default } function() external payable {...
``` pragma solidity ^0.5.0; contract test { function g(address payable a) public { selfdestruct(a); } } ----------------- Error while running verifier, details: [TRACE] Using prover: /usr/bin/z3 Parsing /tmp/tmp7s2u6u6t/test9.sol.bpl /tmp/tmp7s2u6u6t/test9.sol.bpl(18,1): Error:...
