关于Frama-C中`pointer_comparable`谓词的使用疑问

最近我在尝试用Frama-C验证一段涉及指针比较的C代码，但对\pointer_comparable这个ACSL谓词的用法一直摸不着头脑。

根据ACSL文档的说明：

\pointer_comparable接受两个指向对象或函数类型的指针作为参数。\pointer_comparable{L}(p1,p2)成立当且仅当p1和p2指向同一个函数，或者指向同一个数组对象的某个元素（或数组末尾的下一个位置）。

按照这个规则，我认为下面这段C代码里的两个断言都应该能被Frama-C验证通过：

int main(int argc, char** argv)
{
  unsigned char buffer[1024] = {0};

  unsigned char* a = &buffer[1];
  unsigned char* b = &buffer[8];

  //@ assert \pointer_comparable(a, b);
  //@ assert \pointer_comparable(a, a+7);
}

但当我用Frama-C分析这段代码时，却发现结果和预期不符，我实在搞不清楚问题出在哪里。

备注：内容来源于stack exchange，提问作者Random Citizen