Неограниченная функция в плагине EACSL Frama-C

Question

Я пытаюсь сгенерировать контракты в C с помощью плагина E-ACSL из FRAMA-C для следующей программы:

struct lnode {
    int value;
    struct lnode *next;
};

struct set {
    int capacity;
    int size;
    struct lnode *elems;
};

struct set* new(int capacity) {
    struct set *new_set;

    new_set = (struct set*) malloc(sizeof(struct set));
    if(new_set == NULL)
        return NULL; /* no memory left */

    new_set->capacity = capacity;
    new_set->size = 0;
    new_set->elems = NULL;
    return new_set;
}

int insert(struct set *s, int x) {
    struct lnode *new_node;
    struct lnode *end_node;
    struct lnode *n;

    if(s==NULL)
        return 0; /* NULL set */

    if(s->size >= s->capacity)
        return 0; /* no space left */

    end_node = s->elems;    
    n = end_node;
    while(n != NULL) {
        if(n->value == x)
            return 0; /* element already in the set */
        end_node = n;
        n = n->next;
    }

    /* Creation of new node */
    new_node = (struct lnode*) malloc(sizeof(struct lnode));
    if(new_node == NULL)
        return 0; /* no memory left */
    new_node->value = x;
    new_node->next = s->elems;

    s->elems = new_node;
    s->size += 1;

    return 1; /* element added */
}

int isnull(struct set *s) {
    if(s==NULL)
        return 1;
    return 0;
}

int isempty(struct set *s) {
    if(s==NULL)
        return 0; 
    if(s->elems==NULL)
        return 1; /* s is empty */
    return 0; 
}

int isfull(struct set *s) {
    if(s==NULL)
        return 0; 
    if(s->size >= s->capacity)
        return 1; /* s is full */
    return 0; 
}

int contains(struct set *s, int x) {
    struct lnode *n;

    if(s==NULL)
        return 0; /* s is NULL */

    n = s->elems;
    while(n != NULL){
        if(n->value == x)
            return 1; /* element found */
        n = n->next;
    }

    return 0; /* element NOT found */
}

int length(struct set *s) {
    struct lnode *n;
    int count;

    if(s==NULL)
        return 0; /* s is NULL */

    count = 0;
    n = s->elems;
    while(n != NULL){
        count = count + 1;
        n = n->next;
    }

    return count;   
}

В руководстве ACSL (раздел 2.3.2) сказано, что правильный способ сделать это - добавить аннотацию перед функцией. Однако в мою спецификацию я намереваюсь включить предикаты, которые используют функции программы для определения окончательной аксиомы для функции вставки. Например:

@ requires \valid(s);
@ behavior A:
    @ ensures (isfull(s)=0 && length(s)=0 && contains(s,x)=0 && isnull(s)=0 && isempty(s)=1) ==>
(length(s)=1 && contains(s,x)=1 && isnull(s)=0 && isempty(s)=0 && \result==1);

Когда я пытаюсь скомпилировать с помощью e-acsl-gcc.sh Я получаю эту ошибку:

user@ubuntu-tmpl:~/Documents/Code$ e-acsl-gcc.sh -c insert.c -O exec
++ frama-c -variadic-no-translation -machdep gcc_x86_64 '-cpp-extra-args= -std=c99 -D_DEFAULT_SOURCE -D__NO_CTYPE -D__FC_MACHDEP_X86_64 ' -no-frama-c-stdlib insert.c axiomTes.c -e-acsl -e-acsl-share=/home/user/.opam/system/bin/../share/frama-c/e-acsl/ -then-last -print -ocode a.out.frama.c
[kernel] Parsing FRAMAC_SHARE/e-acsl//e_acsl_gmp_api.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl//e_acsl.h (with preprocessing)
[kernel] Parsing insert.c (with preprocessing)
insert.c:31:[kernel] user error: unbound function isempty
[kernel] user error: stopping on file "insert.c" that has errors. Add '-kernel-msg-key pp'
    for preprocessing command.
[kernel] Frama-C aborted: invalid user input.
e-acsl-gcc: fatal error: aborted by Frama-C

Это заставляет меня думать, что вызов функции либо не разрешен внутри аннотации, либо имеет другую синтаксическую спецификацию. Есть ли способ использовать определенные функции программы для формирования предикатов? Другая возможность, которая все еще подходит для меня, - это получить результат вызова функции где-то еще и использовать его внутри аннотации.

Спасибо!

Answer 1

Прежде всего, нам будет гораздо проще ответить, если вы дадите точный код, по которому вы пытались запустить e-acsl, включая его аннотации. Разобрав их, не заключая их в комментарии должным образом, означает, что воспроизвести проблему сложнее, и мы не можем быть уверены, что воспроизводим именно ваши настройки.

Тем не менее, вот проблемы, которые я обнаружил, посмотрев на аннотацию выше (без запуска frama-c на нем по причинам, указанным ранее).

1. Действительно, вы не можете вызывать функцию C в аннотации ACSL. Тем не менее, в ACSL можно определить логические функции и предикаты, которые затем можно использовать в аннотациях (определив их, разумеется). Это описано в руководстве по ACSL, раздел 2.6, и ACSL by Example содержит много их примеров.

2. В ACSL, как и в C, равенство обозначается ==не =,

3. Это может быть хорошей идеей, чтобы разделить ваш ensures во многих предложениях вместо того, чтобы иметь одно предложение, которое является соединением: было бы легче найти, какая часть постусловия не проверена.

4. Точно так же, если вы не хотите завершить контракт, behavior A: не служит никакой реальной цели.

5. С стилистической стороны, @ обязательно вводить аннотацию (с /*@ ... */). Вам не нужно ставить один на каждой строке.