Certifying C program correctness with respect to the CH2O formalization of the C standard with VeriFast: source code

Brief summary: We adapted the approach from our earlier 2021 report ("Certifying C program correctness with respect to CompCert with VeriFast", see: arXiv:2110.11034), so that now we verify against CH2O instead of against CompCert. The uploaded code contains a slightly modified version of CH2O and a fork of VeriFast. Building instructions can be found in README.md (and in the regular documentation for VeriFast). Notable features include: a big step semantics for a subset of CH2O, using coinduction to support diverging programs; a soundness proof of this big step semantics with respect to CH2O axiomatic semantics; a similar big step semantics for a subset of our own VeriFast C, together with a soundness proof with respect to CH2O big step semantics; a formalisation of VeriFast's symbolic execution for the relevant subset of C, together with a soundness proof with respect to VeriFast big step semantics. As in the 2021 report, we extend the VeriFast command line tool to export a Coq script whenever a program has been verified successfully. This generated Coq script proves correctness of the verified program in the CH2O formal semantics. It does so by generating a verification condition (VC) reflecting VeriFast's symbolic execution and a proof for this VC. It then applies to this result the "chain" of soundness proofs mentioned earlier, to arrive at a conclusion of correctness with respect to CH2O. References: The C standard formalized in Coq (Robbert Krebbers, PhD thesis, 2015) The original source code for CH2O on Githu