问题标签 [frama-c]

我将 frama-c 视为在 OCaml 中处理 C 头文件的一种方式（例如，用于生成语言绑定）。它很有吸引力，因为它看起来是一个文档齐全且维护良好的项目。但是，经过大量谷歌搜索和文档搜索后，我找不到任何适合该目的的内容。我只是错过了执行此操作的正确方法，还是超出了 frama-c 的范围？与其他一些插件相比，这似乎是一件相当微不足道的事情。

我正在尝试使用 Frama-C 值分析来研究生成的大型 C 代码，其中边界检查是使用按位与 (&) 而不是逻辑与 (&&) 完成的。例如：

Frama-C 值分析抱怨数组访问：

通过在测试之前添加断言，我设法使它对小例子感到满意：

并增加slevel但我不能在实际代码中做到这一点（太大！）。

有人知道我可以做些什么来消除这个警报吗？

（顺便说一句，有什么理由这样写测试吗？）

我试图指定外部函数的行为，更准确地说，它们的终止。ACSL 文档说该\terminates p;属性指定如果谓词p成立，则保证函数终止，但在p不成立时不指定任何内容。它还解释了一个永远不会返回的函数可以通过以下方式指定：

此外，ACSL 提供了一个属性\exits p;来指定在突然终止的情况下的后置条件。所以我想知道是否：

会指定函数总是永远循环吗？

此外，规范是什么：

意味着关于可能的无限循环？

在为字符串长度定义公理时，我需要使用 reads 子句。

但是，任意区域的 reads 子句在 WP 中还没有实现，还有哪些替代方案呢？

我需要这个公理来证明 string.h 中的一些函数（例如：strcmp）

我刚开始开发一个进行某种别名分析的 frama-c 插件。我正在使用 Dataflow.Backwards 分析，现在我必须通过不同的赋值语句并收集一些关于左值的东西。

frama-c 是否为我提供 3 地址代码？我对左值的形状（或任何内存访问）有一些保证吗？我的意思是，就像在 soot 或 wala 中一样，对于 a->b->c，最多有一个字段访问，st，会有一个临时变量，比如 tmp=a->b; tmp->c;? 我查看了手册，但找不到与此相关的任何内容。

我无法证明 2 个循环不变量：

我猜 \at 不像我预期的那样适用于数组。

ACSL by Example中有一个类似的函数（第 68 页，swap_ranges），它使用了这个，但是，如前所述，他们无法用 WP 插件证明这个特定的函数。我在我的机器上尝试过，确实无法证明相同的不变量。

完整代码

编辑

我使用 Frama-C Oxygen 版本并尝试使用 alt-ergo(0.94) 和 cvc3(2.4.1) 进行自动证明

frama-c 的输出：

cvc3:

交替：

是否可以使用 ACSL 注释 C 宏？

例如：

甚至函数调用，例如

我已经尝试过了，但没有成功。我做错了什么还是根本不可能？

我对如何在结构上正确使用 \valid 注释有一些疑问。

验证结构的内存安全性的正确谓词是：

或者

第一个示例假设\valid(p)（p指向结构的指针在哪里）确保它指向的结构的内存安全，而第二个示例我必须手动指定范围（考虑到内存字段的大小）

通过示例查看 ACSL中的堆栈示例（第 125 页）。他们采用第一个例子。然而，在许多地方\valid(some_string+(0..strlen(some_string)))用于确保那些特定内存位置的内存安全。

编辑：

回应给出的答案。一个正确的内存安全谓词（取自 stdio.h）

例如：

我是 Frama-C 的新手，我想正确学习 ACSL 语法。我有这个虚拟示例，Jessie 插件无法验证第 9 行和第 12 行。我错过了什么吗？要验证的函数（相等）将检查两个数组（a 和 b）在每个索引处是否具有相同的值：

我正在尝试验证 FFS 的软件实现。FFS 的作用是返回一个数字中最低位的索引位置（从 1 开始）。我尝试了许多不同的方式，包括使用幽灵变量。Jessie 无法验证，我不知道为什么？一些指示会非常有帮助。这是代码示例，我假设是 8 位数字：