History log of /seL4-l4v-10.1.1/HOL4/examples/machine-code/graph/graph_specsLib.sml
Revision Date Author Comments
# b28664c3 13-Jun-2018 Anthony Fox <anthony.fox@cl.cam.ac.uk>

Add a selftest for the graph decompiler.


# 6bf2bfd1 08-Aug-2016 Magnus Myreen <magnus.myreen@cl.cam.ac.uk>

Make minor tweaks to graph decompiler's output

Following a request from Tom Sewell


# de536727 24-Mar-2016 Magnus Myreen <magnus.myreen@cl.cam.ac.uk>

Fix a few bugs in graph decompiler


# e050a833 04-Feb-2016 Magnus Myreen <magnus.myreen@cl.cam.ac.uk>

replace SKIP_TAGs with jumps to empty functions

This is in response to a feature request from Thomas Sewell.


# 49afc885 17-Dec-2015 Magnus Myreen <magnus.myreen@cl.cam.ac.uk>

clean up and minor updates


# 472f1780 21-Aug-2015 Magnus Myreen <magnus.myreen@cl.cam.ac.uk>

public release of decompiler tool developed at NICTA

An earlier version of this tool was described in the following paper:

Thomas Sewell, Magnus O. Myreen and Gerwin Klein.
Translation validation for a verified OS kernel.
In Programming Language Design and Implementation (PLDI), 2013.