Moved assert macro into its assert header

[zvonimir]

This is a more meaningful and consistent location
for it.

[shaobo-he]

LGTM.

[shaobo-he]

I have a minor concern: it appears assert.h is coupled with smack.h. This could be a problem when our custom front-ends defined in frontend.py are not used. For example, when a program with assertions is compiled using a makefile and its bc file is intended to be obtained using wllvm. Compilation ignores SMACK's assert.h unless we modify its CFLAGS to include SMACK's header path. But when do it, linking fails because __VERIFIER_assert is not defined.

[zvonimir]

Good point. But how do we deal with this problem when it comes to all other headers we have - like stdlib, stdio, etc.?

[shaobo-he]

Good point. But how do we deal with this problem when it comes to all other headers we have - like stdlib, stdio, etc.?

I think assert.h is unique because assert is a macro while other libraries provide functions. So normally linkers will easily find them.

[shaobo-he]

Another issue with the current implementation manifests in a not-so-realistic case where the users can opt-out assertions in certain files by enabling NDEBUG. SMACK will still check these assertions.

[zvonimir]

We can easily add NDEBUG into assert.h, that is not a problem.
Related to your earlier comment, if a user does not point to SMACK's assert.h, then the bc file we end up containing (most likely) calls to __assert_fail, which we are planning on implementing too.

Btw, I am not set on this solution, and I am open to other proposals. This solution made sense to me since it is consistent with how we deal with other standard C headers.