frama-c - E-ACSL 逻辑函数调用错误 - 未绑定函数

Question

我想从下面说明的程序insert.c中定义简单的函数契约（在ACSL 手册，第 2.3.2 节中定义） 。这些合约将根据观察者函数定义（例如： If ，在 inserton 之后）。我们可以在程序结束时找到它们。isempty(s)==trueisempty(s)==false

为此，由于注释中不能使用已经定义的观察者函数，我定义了放在insert()函数之前的逻辑函数：

/* Procedure insert: adds a new element in a set of integers represented by a linked list */

#include <stdlib.h>


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


/* @ logic integer isnullE(struct set *s) =
    s == \null ? 0:1;
*/

/* @ logic integer isemptyE(struct set *s) =
    s == \null ? 0:
    s.elms == \null ? 1:0;
*/

/* @ logic integer isfullE(struct set *s) =
    s == \null ? 0:
    s.size >= s.capacity ? 1:0;
*/

/* @ logic integer containsE(struct set *s, integer x) =
    \let n = s.elems;
    if (s == \null) { return 0; }
    while (n=! \null) {
        if (n.value == x) {
            return 0;
        };
        n = n.next;
    }
    return 0;
*/

/* @ logic integer lengthE(struct set *s) =
    \let n = s.elems;
    \let count = 0;
    if (s == \null) { return 0; }
    while (n=! \null){
        count = count + 1;
        n = n.next;
    }
    return count;
*/

/*
@ ensure isemptyE(s)==1 ==> isemptyE(s)==0;
*/
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;   
}

但是，逻辑函数（具有相同的名称+“E”，以区分）使用返回的错误与使用已定义的观察者函数完全相同：

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:66:[kernel] user error: unbound function isemptyE
[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

知道我的代码有什么问题吗？

标签： frama-cacsl