Compiling assert(expr) yields redundant if

[tautschnig]

I haven't yet done any bisect, but just noticed that assert(expr) now yields both an assert instruction as well as an if:

$ cat as.c
#include <assert.h>

int main(int argc, char* argv[])
{
  assert(0);
  return 0;
}
$ cbmc/cbmc --show-goto-functions as.c
[...]
main /* main */
        // 0 file as.c line 5 function main
        ASSERT !((signed long int)!(0 != 0) != 0l) // assertion 0
        // 1 file as.c line 5 function main
        IF (signed long int)!(0 != 0) != 0l THEN GOTO 1
        // 2 file as.c line 6 function main
     1: main#return_value = 0;
        // 3 file as.c line 7 function main
        END_FUNCTION

This is on OS X, but the original observation was triggered on Linux.

[tautschnig]

It might actually not be a change in our code base. Doing gcc -E as.c:
Some rather ancient C library:

((0) ? (void) (0) : __assert_fail ("0", "as.c", 5, __PRETTY_FUNCTION__));

whereas recent ones have:

(__builtin_expect(!(0), 0) ? __assert_rtn(__func__, "as.c", 5, "0") : (void)0);

[tautschnig]

For the record: this is due to 6129d36. I'm working on a workaround.