E-ACSL逻辑函数调用错误：未绑定函数及insert.c的ACSL契约定义需求

首先，你遇到的「Unbound function」错误，本质是E-ACSL无法识别你定义的逻辑函数与C语言观测函数之间的关联——ACSL的逻辑域和C的程序域是分离的，不能直接在逻辑注解里调用C函数，必须通过公理绑定或者直接用逻辑表达式定义语义来解决。

下面我给你两种可行的解决方案，同时基于你提到的观测函数完成insert的完整契约：

方案一：用公理块绑定逻辑函数与C观测函数 #

如果你的观测函数已经有成熟的C实现，我们可以通过ACSL的axiomatic块将逻辑函数和C函数的语义绑定，让E-ACSL能正确识别逻辑函数：

#include <stdbool.h>

struct stack {
    int data[100];
    int top;
};

// 定义栈相关的逻辑函数，并通过公理绑定到C观测函数
/*@ axiomatic StackLogic {
    // 声明逻辑函数
    logic boolean IsEmpty(struct stack *s);
    logic boolean IsFull(struct stack *s);

    // 公理：将逻辑函数IsEmpty与C函数isempty的语义关联
    axiom IsEmpty_Contract: \forall struct stack *s; 
        IsEmpty(s) <==> \bool(isempty(s));
    
    // 公理：将逻辑函数IsFull与C函数isfull的语义关联
    axiom IsFull_Contract: \forall struct stack *s; 
        IsFull(s) <==> \bool(isfull(s));
} @*/

// insert函数的完整ACSL契约（符合2.3.2节要求）
/*@ 
    // 前置条件：栈指针非空，且栈未满
    requires s != \null;
    requires !IsFull(s);

    // 后置条件：
    ensures !IsEmpty(s); // 插入后栈一定不为空（对应你提到的观测逻辑）
    ensures s->top == \old(s->top) + 1; // 栈顶指针比插入前加1
    ensures s->data[s->top] == val; // 新元素被正确放在栈顶
    ensures \forall integer i; 0 <= i <= \old(s->top) ==> 
        s->data[i] == \old(s->data[i]); // 原有元素未被修改
@*/
void insert(struct stack *s, int val) {
    s->data[++s->top] = val;
}

// 你原本的观测函数（C实现）
bool isempty(struct stack *s) {
    return s->top == -1;
}

bool isfull(struct stack *s) {
    return s->top == 99;
}

关键说明： #

• \bool()用于将C的bool类型转换为ACSL逻辑域的boolean类型，避免类型不匹配
• axiomatic块是ACSL中连接逻辑域和程序域的核心方式，通过公理明确逻辑函数和C函数的等价关系
• 契约中的\old()用于引用函数调用前的变量值，是ACSL中描述前后状态变化的标准用法

方案二：直接用逻辑表达式定义逻辑函数 #

如果你的观测函数逻辑比较简单（比如只是判断栈顶指针的值），可以直接在逻辑函数中定义语义，完全不需要依赖C观测函数，这样更简洁且不会出现绑定问题：

#include <stdbool.h>

struct stack {
    int data[100];
    int top;
};

// 直接用逻辑表达式定义逻辑函数的语义
/*@ logic boolean IsEmpty(struct stack *s) = s != \null && s->top == -1; @*/
/*@ logic boolean IsFull(struct stack *s) = s != \null && s->top == 99; @*/

/*@ 
    requires s != \null;
    requires !IsFull(s);
    ensures !IsEmpty(s);
    ensures s->top == \old(s->top) + 1;
    ensures s->data[s->top] == val;
    ensures \forall integer i; 0 <= i <= \old(s->top) ==> 
        s->data[i] == \old(s->data[i]);
@*/
void insert(struct stack *s, int val) {
    s->data[++s->top] = val;
}

// 观测函数可以直接复用逻辑函数的语义，保持一致性
bool isempty(struct stack *s) {
    return IsEmpty(s);
}

bool isfull(struct stack *s) {
    return IsFull(s);
}

为什么这个方案能避免错误？ #

因为逻辑函数的语义直接用ACSL逻辑表达式定义，E-ACSL可以直接解析，不需要额外绑定C函数，从根源上避免了「Unbound function」问题。

常见错误原因总结 #

你之前遇到的错误通常是以下情况之一：

1. 仅声明了逻辑函数，但没有通过公理或逻辑表达式定义其语义
2. 没有将C的bool类型转换为ACSL的boolean类型，导致类型不匹配
3. 逻辑函数的定义位置在注解之后，E-ACSL解析注解时还没识别到函数定义

内容的提问来源于stack exchange，提问作者Raul Coroban