search

dapphub / klab

K framework proof explorer & smart contract specification format
GNU Affero General Public License v3.0
123 stars 36 forks source link

Fetch bytecode from the K configuration of spec, when possible. #276

Open MrChico opened 5 years ago

MrChico commented 5 years ago

Right now, one cannot open the evm (e) view, even though all of the information displayed there is available to the execution environment. Currently, the bytecode of contracts is fetched from the projects .sol.json. In many cases (but not all, for example in klab-run of GSTS), it can be fetched from the <accounts> cell.

mhhf commented 5 years ago

we omit the bytecode in klab-prove otherwise my harddrive would be #sad g

MrChico commented 5 years ago

Right, but it's available from the K spec from. Which we start

mhhf commented 5 years ago

go forward and write a parser then

livnev commented 5 years ago

@mhhf @MrChico is it possible to parse K syntax with regex?