Аннотации ACSL к макросам C

Можно ли аннотировать макросы C с помощью 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)

или даже вызовы функций, такие как

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

Я уже пробовал, но безуспешно. Я что-то не так делаю или это просто невозможно?


c static-analysis c-preprocessor frama-c design-by-contract
person Cristiano Sousa    schedule 28.03.2013    source источник
comment
Frama-C предварительно обрабатывает исходный код с помощью gcc -C -E -I.. После этой предварительной обработки контракт, который вы предлагаете в качестве первого примера, больше не имеет смысла (см. предварительно обработанный файл для себя, набрав gcc -C -E -I. самостоятельно). Что я делаю, так это преобразовываю такие макросы в функции с целью их аннотирования.   -  person Pascal Cuoq    schedule 29.03.2013

Ответы (1)


arrow_upward
1
arrow_downward

В 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;
}
person Cristiano Sousa    schedule 18.04.2013