// S : tags   pointers min sym  $TAGS
// S : expect --result error --location-comment ERROR
// S : cc     -o test.bc  $CC_OPT $file
// S : verify --lamp pointers --symbolic $V_OPT test.bc

#include <assert.h>
#include <stdlib.h>

extern "C" void * __lamp_lift_objid( void * p );

#define noinline __attribute__((__noinline__))

noinline void foo( void * a, void * b,  void * c )
{
    uintptr_t ai = (uintptr_t)a;
    uintptr_t bi = (uintptr_t)b;
    uintptr_t ci = (uintptr_t)c;

    if ( ci <= bi )
        // c <= b <= a
        assert( ci > ai ); /* ERROR */
}

int main()
{
    void * a = __lamp_lift_objid( malloc(1) );
    void * b = __lamp_lift_objid( malloc(1) );
    void * c = __lamp_lift_objid( malloc(1) );

    uintptr_t ai = (uintptr_t)a;
    uintptr_t bi = (uintptr_t)b;

    if ( bi <= ai )
        foo( a, b, c );

    free( a );
    free( b );
    free( c );
}