2 ms·

I’m not sure what C code bases you’ve worked with but refactoring in a large C code base is almost never local. Especially if it’s a code base that made extensi

I’m not sure what C code bases you’ve worked with but refactoring in a large C code base is almost never local. Especially if it’s a code base that made extensive use of the gcc flags that disable making sure code does not alias.

pron 6y ago
Providing enough information for the prover does not require a big refactoring, and is significantly cheaper and less risky than a rewrite for an established codebase.