C宏上的ACSL註釋

是否可以使用ACSL註釋C宏？C宏上的ACSL註釋

如：

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

我已經嘗試過，但沒有成功。我做錯了什麼或者是不可能的？

來源

2013-03-28 Cristiano Sousa

郵資-C前處理源與代碼'的GCC -C -E -I.'。在這個預處理之後，作爲第一個例子提供的合同再也沒有意義了（通過自己輸入'gcc -C -E -I.'來查看預處理文件）。我所做的是將這些宏轉換爲用於註釋它們的函數。 –

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

來源

2013-04-18 14:00:54

C宏上的ACSL註釋

回答

相關問題