luongnt95

`if(balances[_from] < _feeSmt + _value) revert();` is the same as `require(balances[_from] < _feeSmt + _value)` which Oyente consider as being a false positive. Do you have any idea to distinguish...

The second contract works now with this [commit](https://github.com/melonproject/oyente/commit/351a6e1d69732f460fca25852815bcf2a25cae03)

Thanks @vietlq I know the expoitation and the commit. - Yeah, `require` and `if revert()` is compiled to the same opcodes. - The #306 commit will help flag `require(a +...

No, there's not

https://github.com/ethereum/tests/tree/develop/VMTests

https://github.com/melonproject/oyente/blob/master/CONTRIBUTING.md is the opcode testing instruction. It would be great if we could also add integration testing with the inputs are smart contracts and the outputs are expected vulnerabilities. Plmk...

Hi @vietlq . Currently, Oyente only detects overflow caused by addition. Will consider adding support for other operations like: multiplication, ...

Thanks @MicahZoltu Will consider this

@beaugunderson it's not fully supported. Could you help me test this feature? Just report any problems you have with this feature. Thanks

@joeykrug Currently, Oyente only gets json input as the input. In order to run json input with Oyente, you also have to use --alow-paths parameter as in [solc](https://github.com/ethereum/solidity/issues/2266) `oyente/oyente.py --standard-json...