@valorzard
regarding https://codeberg.org/ValorZard/ValorC
i think you should take a look at https://plv.mpi-sws.org/refinedc/. it's a BSD licensed tool to formally verify C code using refinement type annotations (c23 attribute syntax just like you want). the advantage is that Rocq program validity proofs are generated, so the trusted computing base is only the Rocq kernel (which has many eyes on it), and not the frontend for verification.
also regarding CompCert: UB is still a consideration in CompCert. see https://www.ralfj.de/blog/2021/11/24/ub-necessary.html for an example how programs with UB can be compiled into inconsistent code by CompCert. the idea of "the code won't have UB" is also misleading in itself (it would only be true if UB-ridden code was rejected at compile time), because even if a compiler doesn't perform any UB-based optimizations and compiles faulty code into something that matches the "intuition" of the C code, something that might be what the programmer expected, there's no actual definition for how it should behave, it is not specified, so bad surprises can per se always happen.
cc @navi
regarding https://codeberg.org/ValorZard/ValorC
i think you should take a look at https://plv.mpi-sws.org/refinedc/. it's a BSD licensed tool to formally verify C code using refinement type annotations (c23 attribute syntax just like you want). the advantage is that Rocq program validity proofs are generated, so the trusted computing base is only the Rocq kernel (which has many eyes on it), and not the frontend for verification.
also regarding CompCert: UB is still a consideration in CompCert. see https://www.ralfj.de/blog/2021/11/24/ub-necessary.html for an example how programs with UB can be compiled into inconsistent code by CompCert. the idea of "the code won't have UB" is also misleading in itself (it would only be true if UB-ridden code was rejected at compile time), because even if a compiler doesn't perform any UB-based optimizations and compiles faulty code into something that matches the "intuition" of the C code, something that might be what the programmer expected, there's no actual definition for how it should behave, it is not specified, so bad surprises can per se always happen.
cc @navi
