solidity
solidity copied to clipboard
SRI-CSL
This is solc-verify, a modular verifier for Solidity.
Hello, is there any possibility for solc-verify to detect vulnerabilites such as: - front running - denial of service - bad randomness - time manipulation If yes it would be...
Hello again, I'm trying to verify the following contract with solc-verify, but it is returning to me an error, that i guess is because this tool can't deal with tx.origin,...
- First, much thanks to your contribution. - But I find encode function is not supported. - My contract is `test/libsolidity/semanticTests/abiEncoderV1/abi_encode_call.sol` ``` contract C { bool x; function c(uint256 a,...
`basic/ExplicitScopings.sol` gives ``` ======= Converting to Boogie IVL ======= ======= test/solc-verify/basic/ExplicitScopings.sol ======= Annotation:1:10: solc-verify error: Undeclared identifier. x + 1 == y ^ ``` where `y` is the return value...
```solidity contract C { function f() external view {} function test(address a) external view returns (bool status) { // This used to incorrectly raise an error about violating the view...
```solidity pragma solidity >=0.5.0; contract EventTrackingStorageRef { mapping(address=>bool) data; /// @notice tracks-changes-in data event e(address a); /// @notice emits e function f(address a) public { mapping(address=>bool) storage ref = data;...
```solidity pragma solidity >=0.5.0; contract FunctionArgs { uint8 x; uint y; /// postcondition x == __verifier_old_uint(x) function noop() public view returns (bool ok) { assert(x == y); return true; }...
Proving the postcondition below seems to require expressing that `f1` and `f2` return true if and only if some element of `a1` and `a2` respectively are greater than zero. ```solidity...
``` pragma solidity ^0.5.0; contract test { string constant a = "solc-verify" ; function g() public { require(true, a); } } ----------------- Error while running verifier, details: [TRACE] Using prover:...
If there is an unsupported feature in a function, we give a quite user friendly message and skip that function. However, implicit constructors are generated separately and for them this...