Frama-c 未能证明关于指针比较的事实

Question

考虑以下 C 代码：

#include <assert.h>

//@ requires p < q;
void f(char *p, char *q)
{
    assert(p <= q-1);
}

//@ requires a < b;
void g(int a, int b)
{
    assert(a <= b-1);
}

使用 alt-ergo，frama-c 成功地证明了 g() 中的断言成立，但未能证明与 f() 相同。为什么？

Answer 1

形式上，指针和整数是两个非常不同的东西。特别是，C 语义指出，指针比较仅针对指向同一分配块（或所述分配块末尾的一个偏移量）中的指针明确定义。这反映在 Frama-C 的 WP 插件在 addr_le 和朋友的定义中使用的模型中（参见 $(frama-c -print-share-path)/wp/why3/Memory.why），其中在比较指针的偏移量之前检查指针是否具有相同的地址。