An Annotated variant CompCert-Clightgen
Extending CompCert for annotated C programs
Oct. 2019 – Jan. 2020 Supervised by QinXiang Cao from SJTU.
In CompCert, the verified compiler, Clightgen can automatically generate the correctness proofs (written in Coq) that need to be done for C programs.
My work aimed to allow users to provide auxiliary proof information in the form of comments within the C program, thereby enabling VST to automatically complete the proofs. I extended the annotation syntax based on a basic version of VST-A, implemented the collection and parsing of out-of-function annotations on the Clight syntax tree, and ultimately generated the corresponding Coq commands automatically.
Based on this, we made a demo that enables interpretive verification of annotation C programs called VST-IDE.
