ACSL annotations on C macros

Question

Is it possible to annotate C macros with ACSL?

eg:

/*@
    assigns \nothing;

    behavior xmin:
        assumes x < y;
        ensures \result == x;

    behavior ymin:
        assumes y <= x;
        ensures \result == y;

    disjoint behaviors;
    complete behaviors; 
@*/
#define min(x,y) (x < y ? x : y)

or even function calls such as

#define min(x,y) __min(x,y)

I already tried it, but with no success. Am I doing something wrong or is it simply not possible?

Answer 1

There exists a flag in frama-c that allows the pre-processing of macros: -pp-annot. Automatically unfolding all macro calls, so you don't need to annotate the macro, this is done where needed in the functions that uses those macros.

Simple example:

#define min(x,y) (x < y ? x : y)

/*@
    requires 0 <= x <= 100000 && 0 <= y <= 100000; // for overflow...
    assigns \nothing;

    behavior xmin:
        assumes x < y;
        ensures \result == 2*x;

    behavior ymin:
        assumes y <= x;
        ensures \result == 2*y;

    disjoint behaviors;
    complete behaviors; 
@*/
int double_of_min(int x, int y){
    int a = min(x,y);   
    return 2*a;
}