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