ACSL, formal verification with Frama-C

[Tjoppen]

Hi

This might be a big ask, but since there is some overlap between langsec and formal methods it would be cool if hammer provided ACSL contracts for its API. This way downstream projects can prove not only that their parsers terminate, but also that they are free of undefined behavior. This assumes hammer itself has been formally verified of course :)