SMACK assertion failure trace help message

[MontyCarter]

Overview

Implement a C source level assert() function with a signature similar to void assert(expr test, string msg). When such an assertion fails, msg gets printed out after (ASSERTION FAILS) in the SMACK error trace.

Background/Rationale

I'm working on modeling pthreads, which is being implemented as a C level library provided with SMACK. This means any assertions in the pthread library model are not written by the tool users. If such any such assertions fail, users must dig through the library source to see what the problem was.

Implementing an assert() function with a signature similar to void assert(expr test, string msg) would allow deep or complicated assertion failures to provide a helpful message about the nature of the assertion violation.

Caveats

I realize that strings in C are seen as char* arrays in SMACK, but we must be doing something similar for __SMACK_code(), so we should be able to get around this.

Also, if my proposed signature causes overloading problems with the existing assert(), then an alternate such as assert_msg() would work just fine for my purposes.

[michael-emmi]

Very good idea Monty. Just two comments

1. Strings in C are indeed char * types; string is a distinct type available in C++. So the signature should be void ___(int,char*).
2. The function void assert(int) is in the standard <assert.h> library, so we will need a different name. Your suggestion assert_msg seems reasonable.

[shaobo-he]

I would like to revive this issue and propose something different than Monty's. I propose that we reuse the __assert_fail function to which libc expands the assert macro. We could write a pass that converts each call site of this function into either a call to a Boogie function or a series of Boogie commands that consist of assumes and assert false;.