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

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

0 голосов
/ 30 апреля 2018

Я пытаюсь сгенерировать контракты в 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) говорится, что правильный способ сделать это - добавить аннотацию перед функцией. Однако в мою спецификацию я намереваюсь включить предикаты, которые используют функции программы для определения окончательной аксиомы для функции insert . Например: 

@ 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

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

Спасибо!

1 Ответ

0 голосов
/ 01 мая 2018

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

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

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

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

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

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

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

...