1

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)

私はすでにそれを試しましたが、成功しませんでした。私は何か間違ったことをしていますか、それとも単に不可能ですか?

4

1 に答える 1

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;
}
于 2013-04-18T14:00:54.490 に答える