问题标签 [alt-ergo]

以下 SMT-LIB 代码在 Z3、MathSat 和 CVC4 中运行没有问题，但在 Alt-Ergo 中没有运行，请告诉我发生了什么，非常感谢：

在下文中，当相关的 C 代码被注释掉时，行为 neg_limit 的后置条件如何被证明为真？

正如预期的那样，Safety->check 算术溢出之一是不可证明的，但似乎 neg_limit 也应该是不可证明的。

背景：我正在使用 Frama-C-Boron、Jessie 以及通过 gWhy、Alt-Ergo 来学习如何编写规范并证明函数符合它们。任何关于规范策略、工具等的线索测试、RTFMing 等也值得赞赏。到目前为止，我正在阅读 ACSL 1.7 实施手册（比 -Boron 的更新）和 Jessie 教程和参考。手动的。

谢谢！

这是第一个后置条件的 gWhy 目标：

第二个：

我应该如何证明如下代码的正确性，为了避免效率低下，它依赖于模运算？

我已经尝试过 WP 的“int”模型，但是，如果我理解正确，该模型配置了 PO 中逻辑整数的语义，而不是 C 代码的正式模型。例如，当使用“int”模型时，WP 和 RTE 插件仍然需要并为上面的无符号加法注入溢出断言 PO。

在这种情况下，我是否可以为语句或基本块添加规定逻辑模型的注释，以便我可以告诉 Frama-C 特定编译器如何实际解释语句？如果是这样，我可以使用其他验证技术来处理已定义但经常导致缺陷的行为，如无符号环绕、编译器定义的行为、非标准行为（内联组件？）等，然后证明周围的代码。我正在描绘类似于（但比）更强大的“断言修复”，用于通知某些静态分析器某些属性在它们无法为自己派生属​​性时保持不变。

我正在使用 Frama-C Fluorine-20130601，作为参考，使用 alt-ergo 95.1。

以下 SMT-LIB 代码在 Z3、MathSat 和 CVC4 中运行没有问题，但在 Alt-Ergo 中没有运行，请告诉我发生了什么，非常感谢：

在此处在线运行此示例

1. 在 Z3 中，unsupported ; :incremental生成了消息，但这不会改变计算并获得正确的答案。

2. 在 mathsat 中，unsupported会生成一些消息，但会显示正确答案。

3. 在 Cvc4 中，代码执行没有问题并获得正确答案。

4. 在 Alt-Ergo 中，代码在没有消息的情况下执行，但unsat会生成错误答案（正确答案是：）unsat, sat。

我正在尝试使用 alt-ergo 证明器在 frama-c 上运行测试文件。但是，我在使用 alt-ergo 时遇到了以下错误。所有其他的 frama-c 检查都很好。我知道问题不在于测试文件。

我在windows机器上并通过cygwin以管理员模式执行所有安装我得到了frama-C Neon并安装了它./configure & make & make-install，安装成功（所有frama-c检查都通过了我的测试文件）

我从http://alt-ergo.ocamlpro.com/download.php获得了以下版本的 alt-ergo Linux x86_64 二进制文件：alt-ergo-0.95.2-x86_64 。我选择了这个版本，因为 frama-c 文档要求版本 0.95。

我使用以下说明安装 alt-ergo ( https://www.lri.fr/~marche/MPRI-2-36-1/install.html )

安装 Alt-ergo

最简单的方法是获取alt-ergo的二进制文件。下载名为“Linux x86_64 binary”的文件然后：

打电话时，which但 frama-c 和 alt-ergo 有正确的路径

我也安装了Why3，它检测到了ergo prover

编辑

我使用在线示例创建了以下 test.mlw

运行 alt-ergo 会导致：

有任何想法吗？

假设我们有以下带注释的 C 代码：

Z3 和 Alt-ergo 都无法证明 assert final_a 和后置条件；Z3 也不能证明循环不变；

Alt-Ergo 的输出：

Z3 的输出：

什么不见​​了？

假设我们有以下 C 注释代码：

尽管 final_progress 语句已被证明，为什么 Alt-Ergo/Z3 会为 final_c 断言产生“未知”或超时？对于这种明显（从用户的角度）无效的陈述，我肯定希望看到“无效”。

如何frama-c -wp验证wp 手册中的示例- 一个简单的swap函数 (swap.c)：

调用

$ frama-c -wp -wp-rte swap.c

给出：

我想知道为什么

1. 我的尝试与手册中的目标数量不同（4 对 9）？
2. Alt-Ergo（事实上，没有一个cvc3, gappa, simplify, verit, yices, z3）不能放弃这 4 个证明义务中的任何一个？

我使用最新的 OPAM 安装：

• frama-c: 钠-20150201
• alt-ergo：0.95.2（来自 ubuntu 14.04 主存储库包alt-ergo）
• why3: 0.86.1

一个证明义务的例子，传递alt-ergo给wp：

我正在尝试使用 Frama-C 的 WP 插件来证明一些 C 代码，但下面的示例有问题：

命令：

我的 frama-c 有版本：Sodium-20150201，alt-ergo 是 0.95.2

结果是

我注意到我什么时候会改变

至

和

结果是

但我不想依赖'需要 STRING_LEN == 5;' 并用'const'证明第一个例子。如何做到这一点？

假设我们有以下 C 代码：

我想在初始化时使用静态分析计算变量 x 的边界，从而得到满足的谓词。在这个例子中，main 开头的 x 的间隔应该是 [8, 12]。

TL;DR：给定代码中某处的断言，计算这些范围的最佳方法是什么？

到目前为止我尝试了什么：

我认为解决这个问题的最佳方法是使用最弱的前提条件计算器。我尝试过使用 frama-c 的 wp 插件，但由于它是为验证目的而构建的，我不确定它在这个用例中有多有用。在以下代码上应用插件时：

我收到以下谓词发送到 alt-ergo 求解器：

如果您仔细观察，可以通过遵循变量 i 上不会导致 (i_1 = 0) 的边界来识别输入所需的间隔。我已经标记了这些界限。这不是很健壮，例如，如果断言更改为&& n <= 13，则隐含谓词的“左侧”保持不变，因为没有任何条件改变。另外我不确定这在其他情况下有多大用处，例如在调用函数时将我的断言更改为 requires 语句，我无法理解生成的谓词：

并向函数添加 requires 语句：

我得到：