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) < [email protected]> 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 >
_______________________________________________ Devel mailing list [email protected] https://sel4.systems/lists/listinfo/devel
