Compiler Explorer

Source code

#include <stdlib.h>   // abort

__attribute__((noinline))
__attribute__((warning("condition is not guaranteed")))
static void never_reach(void) { abort(); }   // must define a side effect, to not be optimized away

// EXPECT() : will trigger a warning if the condition is not guaranteed
#define EXPECT(c)  (void)((c) ? (void)0 : never_reach())

// assume() : tell the compiler that `cond` is true
// note : only works for simple conditions, such as `i>=0`.
// Avoid complex conditions invoking functions.
#define assume(cond) do { if (!(cond)) __builtin_unreachable(); } while (0)

// *********************************************************
// Function declaration
// *********************************************************

int positive_plus1_body(int v); 
#define positive_plus1_preconditions(v)   ((v)>=0)     // Let's first define the preconditions. 
                                                       // Name is long, because conditions must be unique to the function

// The inlined function express the contract, with both pre and post conditions.
// `inline` is essential, so that actual input values get verified,
// and result gets enriched with `assume` conditions.
// Problem is, the error is now located INTO the inlined function, not at the place where it's called.
// This makes it very hard to identify where the problem happens.
static inline int positive_plus1(int v)                // Ideally, this function should also have additional attribute to not trigger warnings when it's not invoked
{
    int r;
    EXPECT(positive_plus1_preconditions(v));           // preconditions
    r = positive_plus1_body(v);
    assume(r > 0);                                     // postconditions
    return r;
}

// Note : one consequence of this construction is that 
//        there is no `positive_plus1()` function symbol in the library,
//        only positive_plus1_body(), which doesn't implement the contract.
//        Invoking positive_plus1() now requires the header file.

// *********************************************************
// Usages
// *********************************************************

int test11(void)  { return positive_plus1(3); }  // Fine : condition is respected
int test12(int i) { if (i<0) return 0; return positive_plus1(i); }  // after the `if`, i >= 0 necessarily, so `i` respects the condition => no warning
int test13(int i) { if (i<2) return 0; i-=2; return positive_plus1(i); }  // compiler can correctly track the range value of `i` after simple arithmetic

# if 0   // Replace by 1 to trigger warnings due to incorrect invocations

// The following usages will trigger warnings
// Problem is, the error will be located _inside_ the inlined function, at EXPECT()'s position
int test21(void)  { return positive_plus1(-1); }  // Condition not respected : triggers a warning 
int test22(int i) { return positive_plus1(i); }   // No idea about value of `i` : it may not respect condition => correctly triggers a warning

#endif

// *********************************************************
// Function definition
// *********************************************************

__attribute__((noinline))
int positive_plus1_body(int v) 
{ 
    assume(positive_plus1_preconditions(v));    // Re-use conditions defined in declaration, to keep synchronized
    return v+1;
}

int positive_plus2(int v)
{
    assume(v>=0);
    v = positive_plus1(v);   
    v = positive_plus1(v);   // Without post-conditions, this second invocation would fail.
                             // This can be tested by commenting out the postcondition line inside `positive_plus1()`.
    return v;
}