| #
77d86cfc |
|
07-Dec-2016 |
Thomas Sewell <Thomas.Sewell@nicta.com.au> |
GraphRefine + CRefine: handle slightly more cases.
New testfile for graph-refine export with new handling code. Also
some slight tweaks to some CRefine proofs that will be needed to
remove DONT_TRANSLATE markers from certain key places in the seL4
code. These proofs are also compatible with previous seL4.
|