March 29, 2021 1:51 PM, "Ben Fiedler" <sel4(a)bfiedler.ch> wrote:
I'm having troubles generating the CAmkES glue
component specification and proofs from our source.
I can and have successfully generated the ADL/CDL spec and implementations using the
Grepping around the docs I've found references to a 'camkes.sh' script,
but neither the project
tree nor the files generated during build contain it.
Digging around reveals commit 21becfa909595f0ba204b7fafef9e3629e8627c7  in camkes-tool
to be a
potential culprit. Even though the camkes.sh script was removed long before, it seems that
removed support for the --platform argument and shifted to a more CMake-focused build (and
documentation was not updated - it still mentions the --platform argument).
In the course of this, the cimp-base.thy template was orphaned and is not referenced
least according to grep). I think I can hack some CAmkESGen expression together that
cimp-base.thy template, but I'm still not entirely clear where/how the user-provided
theory comes into play, or what to specify in it. Any help is still greatly appreciated!