C宏上的ACSL批注

Question

可以用ACSL注释C宏吗？

例如：

/*@
    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)

或者甚至函数调用，比如

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

我已经试过了，但没有成功。是我做错了什么，还是根本不可能？

Answer 1

在frama-c中有一个标志，它允许对宏进行预处理：-pp-annot。自动展开所有宏调用，因此您不需要注释宏，这是在使用这些宏的函数中需要的地方完成的。

简单的例子：

#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;
}