Hi,
I have been trying to reuse the seL4 verification framework to verify a toy example I built on seL4, and I am currently stuck on the c-parser step. I am trying to use c-parser to parse the example I built, then conduct refinement verification. The toy example is a normal c project, which includes `sel4.h`.
From this thread: https://lists.sel4.systems/hyperkitty/list/devel@sel4.systems/thread/3QYNFY4... I learned that I am supposed to do
$ ./isabelle/bin/isabelle jedit -d . -l CParser toy.thy And the toy.thy file is supposed to begin with `install_C_file("toy.c")`.
However, since toy.c includes sel4.h, I am not sure how to preprocess it before I put it into toy.thy. I know the standalone c-parser can have a -I flag to include in all the dependency directories, but it cannot open an interactive window. (From my understanding, the standalone c-parser seems to be only a checking tool)
I also know that when sel4 is parsed into HOL, it is preprocessed into a single c file `kernel_all.c_pp`, which is later parsed. I am not sure if the preprocessor tool can be reused for other applications as well.
My question is summarized as: 1. Is there a way to add an include directory in interactive CParser? 2. If not, can I reuse the preprocessing approach for sel4 to preprocess my application to a singleton file that can be parsed by c-parser?
Any help will be appreciated!
Thanks, Ru