问题标签 [acsl]

我是 Frama-C 框架的新手，我正在尝试使用 C 程序进行一些合同测试。我打算为此使用 E-ACSL 插件，并尝试了一个测试程序来查看它是如何工作的，但是我得到了一些编译错误。这是我的代码：

然后，这里是 Frama-C 注释的代码：

最后，我尝试使用gcc和手册指示的标志（第 13 页）对其进行编译，但出现以下错误（和警告）：

我还删除了“-rtl-bittree”标签，因为它返回另一个错误。

Frama-C 版本是最新的：Sulfur-20171101 知道发生了什么吗？

谢谢！

我正在用 frama-c 测试这个小程序，但我一直收到同样的错误。我不确定这意味着什么。我对分配一切意味着什么感到特别困惑。

这是带有 ACSL 注释的代码：

这是我尝试测试代码时终端所说的内容：

我正在尝试使用 Frama-C E-ACSL 插件生成带注释的文件。我创建了以下文件：

• Insert.c：包含创建链表的所有结构。
• AxiomTest.c：包括主要功能，其中指示了它必须满足的断言。所有功能和结构都根据Insert.c文件

在编译/检测程序时，手册指定了以下终端命令：

为了成功编译Insert.c和AxiomTest.c必须链接，但我找不到任何标志。

有什么帮助吗？或者有没有其他方法可以做到这一点？

我正在尝试使用来自 FRAMA-C 的 E-ACSL 插件在 C 中为以下程序生成合同：

ACSL 手册（第2.3.2 节）说正确的方法是在函数之前添加注释。但是，在我的规范中，我打算包含使用程序函数为插入函数定义最终公理的谓词。例如：

当我尝试使用编译时e-acsl-gcc.sh出现此错误：

这使我认为注释中不允许函数调用或具有其他语法规范。有没有办法使用程序定义的函数来形成谓词？仍然适合我的另一种可能性是在其他地方获取函数调用的结果并在注释中使用它。

谢谢！

我想从下面说明的程序insert.c中定义简单的函数契约（在ACSL 手册，第 2.3.2 节中定义） 。这些合约将根据观察者函数定义（例如： If ，在 inserton 之后）。我们可以在程序结束时找到它们。isempty(s)==trueisempty(s)==false

为此，由于注释中不能使用已经定义的观察者函数，我定义了放在insert()函数之前的逻辑函数：

但是，逻辑函数（具有相同的名称+“E”，以区分）使用返回的错误与使用已定义的观察者函数完全相同：

知道我的代码有什么问题吗？

我目前正在发现 frama-c 的功能，尤其是 WP & Value 的分析工具。我的最终目标是能够在涉及多个层的较大代码上使用 frama-c：

• 很多函数调用
• 使用复杂的数据结构
• 静态和/或全局变量

到目前为止，我一直在尝试应用自下而上的方法，即开始指定不包含任何函数调用的函数，并通过使用 -lib-entry 和 -main 内核选项隔离它们来分析它们的行为。通过这样做，我确保如果假设前提条件为真，则验证整个函数合同。一旦我试图指定调用这些函数的上层，事情就变得复杂了。首先，我经常必须指定被调用函数的行为，这并不容易，因为这些函数可能会处理当前函数范围之外的变量/函数。

让我举一个简单的例子：

假设在file1.h中我们定义了一个数据结构“my_struct”，它包含一个字段编号和一个字段奇偶校验。

在file1.c我有两个功能：

• 第一个函数“check_parity”只测试静态变量_sVar 的奇偶校验字段是否正确。
• 第二个函数“correct_parity”调用第一个函数，并在字段不正确时更正奇偶校验。

在file2.c中，我有一个函数“outside_caller”，它只调用了正确的奇偶校验（）。我的目标是能够以与指定正确奇偶校验相同的方式指定 outside_caller。下面是对应的源码：

文件1.h

文件1.c

文件2.c

这里的主要问题是，为了指定 outside_caller()，我需要访问超出 file2.c 范围的 _sVar。这意味着要处理在 file1.h 中声明并在 correct_parity 函数中更新的幽灵变量 (g_sVar)。为了使调用者（correct_parity）能够使用被调用者的合约，必须在被调用者的合约中使用ghost变量g_sVar。

WP分析结果如下：

(1) check_parity()

frama-c -wp src/main.c src/test.c -cpp-command 'gcc -C -E -Isrc/' -main 'check_parity' -lib-entry -wp-timeout 1 -wp-fct check_parity -wp -rte -wp-fct check_parity -then -report
[rte] 注释函数 check_parity
[wp] 14 个预定目标
[wp] 已证明目标：14 / 14
Qed：9 (4ms)
Alt-Ergo：5 (8ms-12ms-20ms) (30)

(2)正确奇偶校验()

frama-c -wp src/main.c src/test.c -cpp-command 'gcc -C -E -Isrc/' -main 'correct_parity' -lib-entry -wp-timeout 1 -wp-fct correct_parity -wp -rte -wp-fct 正确奇偶校验 -then -report
[rte] 注释函数正确奇偶校验 [wp] 18 个预定目标
[wp] 已证明目标：18 / 18
Qed：12 (4ms)
Alt-Ergo：6 (4ms-37ms-120ms) (108)

(3) outside_caller()

frama-c -wp src/main.c src/test.c -cpp-command 'gcc -C -E -Isrc/' -main 'outside_caller' -lib-entry -wp-timeout 1 -wp-fct outside_caller -wp -rte -wp-fct outside_caller -then -report
[rte] 注释函数 outside_caller
[wp] 14 个预定目标
[wp] [Alt-Ergo] 目标 typed_outside_caller_assign_exit : 未知 (Qed:4ms) (515ms)
[wp] [Alt-Ergo ] Goal typed_outside_caller_call_correct_parity_pre_correct_req_is_par___ : Unknown (636ms)
[wp] [Alt-Ergo] Goal typed_outside_caller_assert : Timeout
[wp] [Alt-Ergo] Goal typed_outside_caller_assign_normal_part1 : Timeout
[wp] [Alt-Ergo] Goal typed_outside_caller_call_correct_parity_pre_correct_req_is_num___ : Unknown (205ms)
[wp]证明目标：9 / 14
Qed：9（4ms）
Alt-Ergo：0（中断：2）（未知：3）

==> WP：图形用户界面输出

在此配置中，调用者使用 g_sVar ghost 变量指定，除了 requires 和 assings 子句，原因有两个：

• 我需要使用 \valid & \valid_read 检查 _sVar R/W 访问，因为它是一个指针
• 当我尝试使用 g_sVar 指定被调用者的分配子句时，我无法验证相应的子句。

但是通过这样做，我以某种方式使调用者的规范无效，正如您在 WP 的输出中看到的那样。

为什么看起来我调用的函数越多，证明函数的行为就越复杂？是否有适当的方法来处理多个函数调用和静态变量？

非常感谢您！

PS：我在运行 Ubuntu 14.04、64 位机器的 VM 上使用 Magnesium-20151002 版本。我知道开始使用 WhyML 和 Why3 对我有很大帮助，但到目前为止，我无法按照本教程的每个步骤在 Windows 和 Ubuntu 上安装 Why3 ide。

I am running an old application called ACSLX. It is trying to call a DOS move command, but because sh.exe is in my path, I am getting an error. sh.exe is part of Git and also RTools, both of which I have installed. As you can see it is simply trying to move a file, but this is failing. How can I prevent this? This is the console output of ACSLX when I try to build the "Spring" example project.

我想找到一些可以应用于函数或函数指针的 ACSL 注释，以表明它具有引用透明的属性。以某种方式说“当给定相同的参数时，此函数将始终返回相同的值”。到目前为止，我还没有找到任何这样的方法。谁能给我指出一种表达方式？

也许某种方式来引用任意逻辑函数？如果我可以命名一个未知数logic boolean uknown_function(void* a, void* b) = /* this is unkown */;，那么我可以将一个函数记录为具有\result等于这个任意/未知逻辑函数的后置条件？

更大的上下文是尝试进行类型擦除比较。我想概括地表达“用户给了我void*s 和 abool (*)(void const*, void const*)来比较它们的概念，并且用户向我保证，所提供的函数确实是严格的偏序，无论这些指针指向什么。” 如果我有这个，那么我可以开始描述这些被排序的类型擦除对象的属性，例如。

此函数模拟一个函数，该函数返回一个持续上升的值，直到发生溢出。这就像millis()Arduino 中的函数。

为了证明实现，我需要增加（因此，分配）静态变量以保持调用之间的状态。但是，调用的函数mock_millis()应该仍然能够assign \nothing.

有没有办法让 WP 忽略 assigns 子句？

我尝试使用 ghost 变量执行此操作，并注意到分配 ghost 变量的函数不能是assigns \nothing. 我认为幽灵变量完全独立于程序实现。这有什么特殊原因吗？

我试图证明一个函数的正确性，该函数检查数组是否按递增/递减顺序排序或未排序。如果按降序排序，则返回-1，如果按升序排序，大小为 1，则返回 -1，或者包含相同的值，如果没有排序或为空，则返回 0。跑步：Frama-c-gui -wp -wp-rte filename.c

这是 logics.h：

问题来自 Frama-c 未能证明后置条件：

这是一个预期的问题，因为在包含相同值的数组的情况下谓词重叠，这意味着数组 [42,42,42] 可以使两个谓词都返回 true，这使 Frama-c 感到困惑。

我想修改谓词 is_sortedDec(t,size) 以表达以下想法：数组按递减排序，并确保该属性，至少有 2 个索引 x,y 例如 array[x] != array[y ]。

存在两个索引 x,y 使得 t[x] != [y] 并且数组按所有索引的降序排序。

我试过这样的事情：

但是 Frama-c 对语法不太满意。

关于如何解决这个问题的任何想法？也许可以改善整体证明？谢谢。