Hi Ru,

the file l4v/tools/c-parser/testfiles/parse_include.thy has an example of how to do this. The Isabelle commands in the theory file there are:

external_file "includes/test_include2.h" external_file "parse_include.c"

new_C_include_dir "includes"

install_C_file "parse_include.c"

In the seL4 verification, there is a bit more to the invocation of the preprocessor, so we do this separately via the command line (in the build system) and concatenate the output of the preprocessor for all C files to make extra sure the theorem prover is seeing the same input as the compiler. These are just regular gcc or clang command line invocations, nothing specific to do with Isabelle.

Cheers, Gerwin

On 15 Oct 2023, at 13:55, r2ji@uwaterloo.ca wrote:

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 _______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems