> They can be compile time if the compiler can verify them statically (where they become a noop)

This only happens during constant evaluation. For example, the following could be determined statically, but compiles w/o error on gcc

int add_nums(int x, int y)

    pre(x >= 0)

    pre(y >= 0)

    return x + y;

int result_rt = add_nums(-1,-1); // no compile error