sel4 verification
Closed this issue · 3 comments
After I've built the sel4 validation environment and run run_tests, I want to use c-parser, but I don't know how to build the environment and run it, I can't find the specific reference documentation, can you tell me where it is? Thank you very much for your answers.
When you say you want to use the C parser, what do you mean by that?
If you want to use it on seL4, and have already done the run_test command and the session CRefine has passed, then that means the C parser has read the seL4 code and the refinement proof between that C code and the abstract specification has passed.
If you want to run the C parser on other programs, then I'm sorry to say that there is no reference documentation for it. There is the AutoCorres tool built on top of the C parser which does come with some documentation in its release package.
Thank you very much for your answer, which is very helpful to me.
Glad to help.