Hello, may I ask a few quick questions about the usage of Oyente?
Does Oyente provide edge coverage? If not by default, is there any way we can get the edge coverage by adding a few lines of statements into Oyente to get it?
Does the original version Docker image of Oyente presented in the paper provide any type of code or branch coverage?
Is the code coverage computed by dividing the number of covered opcodes by the total number of opcodes for a contract?
Does Oyente support solidity contracts with compiler versions equal to and above 0.5.0?
Are the states used to execute a function transaction produced by executing other real transactions, or synthetically produced? Synthetically meaning that they might not be states that can be actually produced in real-world scenarios.
I have answered you privately previously. Supporting it won't be difficult and such PR would be welcome!
As I didn't construct the paper version image, you might have to run it yourself and see the output. In any case, I would suggest you to use the latest version which has been improved a lot unless you are a very specific reason.
yes
I'm unsure about this. While I would like to confirm this also, I don't have a setup to allow me to do so at the moment. If you have encountered any problem on running contracts with Solidity 0.5+, you are welcome to file an issue for further discussion!
To the best of my knowledge (because I didn't touch the whole codebase), the base state is fully symbolic.
Hello, may I ask a few quick questions about the usage of Oyente?
Thank you so much for your time and help!