Thanks Japheth. I confirmed that I can generate Isabelle files from camkes by modifying the camkes setting. I haven't tried with generated proof for glue code. Will let you know if I have more question. Thanks On Wed, Aug 21, 2019, 12:24 AM Lim, Japheth (Data61, Kensington NSW) < Japheth.Lim@data61.csiro.au> wrote:
Hi Norrathep,
Norrathep Rattanavipanon wrote:
I have been trying to generate Isabelle file from CapDL specification. But I run into an error when I'm running the command:
./parse-capDL --isabelle=out.thy --object-sizes=object_sizes.yaml example-arm.cdl
We recently put in a major change to the Isabelle translator. The input capDL file is now required to be pre-allocated, i.e. every object must be placed in an untyped with a known physical address.
The existing example files date from before this change, and so they don't meet the requirements to be translated into Isabelle. Sorry that you got confusing error messages as a result. We plan to make this more consistent in the near future.
Is there any step I'm missing? Or does the tool not support the conversion to Isabelle?
The standard way is to build a CAmkES application with the option `CAmkESCapDLStaticAlloc` enabled. This will generate a suitable capDL file for proofs.
Based on your other question thread, you may be interested in our README for CAmkES proofs:
https://github.com/seL4/camkes-tool/tree/master/cdl-refine-tests
This generates proofs between the CAmkES high-level model and the capDL system representation. However, we are not working on C glue code proofs at the moment.
This is all work in progress, and quite rough around the edges. Nevertheless, we're happy to try to answer any questions you might have. It would help if we knew more about your work, so that we can give more specific replies.
Cheers, Japheth Lim Proof Engineer, Trustworthy Systems