Add a flag to the frontend that checks that all functions have been verified
From #37:
Perhaps I'm simply not well-versed in the verification methodology but as a bit of an "outsider" seeing the conclusion stating File [src/test.c] successfully checked.
when no proofs have been written is really bothersome to me.
To me, this indicates that unless I am a researcher of some sort, I will have to make sure everything is properly specified or else I will receive no errors even though I might have buggy code. This is only worsened by the fact that contributors to the project will have to also be the same, which is something I cannot (and want not) enforce before accepting contributions.
Generally speaking, I would rather be 100% confident that getting a status 0 indicates the highest degree of certainty that the tool has checked my code and has found no issues. In that sense, having no proofs for the program to run (in the case that the file has function definitions) should be a very loud error message indicating "hey, you've not actually tried to verify this code - this is a problem".
More specifically, it would be great to get a huge, fatal error if a function is skipped when generating specs. This should never be the case in our sort of project and I would imagine many others might want the same safety net.
Realizing this is not the preferred mode of operation for many, putting this sort of behavior behind a strict flag of some sort would be just fine, but giving the idea of "success, you're safe!" when in reality something has been missed entirely seems counterproductive to the goal of actually verifying a codebase.