supposing a compiler, was written in c, would frama-c be able to get similar guarantees that coq allows for compcert?
also, what happens when the loop invariants can't be automatically proved? is there some way to manually prove invariants hold?
also, what happens when the loop invariants can't be automatically proved? is there some way to manually prove invariants hold?
Coq has been used to formally verify a large body of classical mathematics. Coq can 'understand' what a prime number is and can be used to prove that there are infinitely many primes, can prove that sqrt(2) is irrational, etc. Coq can prove a recursive solver for the Towers of Hanoi actually solves the problem, etc. And thus Coq can prove a C program to solve the Towers of Hanoi correctly solves the problem, because Coq can reason about C programs.
I've been slowly working through the Software Foundations series on using Coq/Gallina:
https://softwarefoundations.cis.upenn.edu/
Another poster mentioned CBMC which I just started playing with. It is much less powerful than Frama-C, there isn't the ACSL specification capability and theorem proving, but it is much more automatic and much faster to get started with. For many cases if I just want to verify that a certain C file frees all its mallocs, doesn't have out-of-bounds accesses, and that all obviously bounded loops terminate, CBMC is much easier. Also, like Frama-C, it converts C functions into "goto programs" (removes the syntactic sugar of 'for' and 'while' loops to obtain a more pure Control-Flow-Graph (CFG)) for certain forms of analysis, and when I first encountered this in Frama-C there was no explanation why, whereas the manual for CBMC actually has an excellent gentle introduction: