Suhabe Bugrara

What happens when the EvmSSAEngine encounters bytecode that cannot be put into SSA form? Does it raise an error? Is there an example bytecode I can try that triggers this...

Annotation for specifying reverts

1

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) {...

Support for relevant aspects of ecrecover

1

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...

Hi, I wrote this spec using the solidity-semantics, but can't get it to compile: ``` requires "solidity.k" module T1-SPEC imports SOLIDITY rule #execute => . int sum ; sum =...