0

我正在尝试使用来自 FRAMA-C 的 E-ACSL 插件在 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

这使我认为注释中不允许函数调用或具有其他语法规范。有没有办法使用程序定义的函数来形成谓词？仍然适合我的另一种可能性是在其他地方获取函数调用的结果并在注释中使用它。

谢谢！

4

1 回答 1

1

首先，如果您提供您尝试启动 e-acsl 的确切代码，包括其注释，我们会更容易回答。将它们分开，没有在评论中正确地包含它们仅意味着重现问题更加复杂，并且我们无法确定我们正在重现您的设置。

也就是说，这是我通过查看上面的注释发现的问题（由于前面所述的原因，没有在其上启动 frama-c）。

  1. 实际上，您不能将C函数调用到ACSL注释中。但是，可以在 ACSL 中定义逻辑函数和谓词，然后您可以在注释中使用它们（当然在定义它们之后）。这在ACSL 手册第 2.6 节中有描述，ACSL by Example包含许多示例。

  2. 在 ACSL 中，与在 C 中一样，相等性由 表示==，而不是=。

  3. ensures将您的子句拆分为多个子句而不是一个作为连词的子句可能是一个好主意：这样可以更容易地找到未验证后置条件的哪一部分。

  4. 同样，除非您想完成合同，否则合同behavior A:没有任何实际用途。

  5. 在风格方面，@仅强制引入注释（带有/*@ ... */）。您不需要在每一行放置一个。

于 2018-05-01T15:54:27.433 回答