问题标签 [acsl]

我想有一种方法来描述包含抽象列表的逻辑/规范级别结构。ACSL 参考手册第 27 页上的示例 2.2.7表明有一种方法可以做到这一点，如下所示：

如果我将此确切代码复制/粘贴到文本编辑器中并尝试使用 wp 插件运行此代码：

frama-c -wp -wp-rte -wp-prover alt-ergo shapes.c

我收到一个错误：

[kernel:annot-error] shapes.c:1: Warning: unexpected token '{'

如果我放弃尝试编写结构类型的逻辑/规范级别声明，但仍想编写实例化 C 中定义的结构的逻辑/规范级别表达式，如下所示：

我仍然收到一个错误：

并且没有办法将结构的特定值编写为规范中的表达式会导致一些相当丑陋的规范，所以我希望我做错了什么。

如果我深入研究 frama-C 20.0 的源代码以尝试找到用于/*@ type声明的解析器生成器代码部分，看起来 Ex 2.2.7 中的语法并没有真正实现。看起来类型级别声明的语法是 frama-c-20.0-Calcium/src/kernel_internals/parsing/logic_parser.mly 的第 799 行（称为 type_spec）并且结构的类型级别声明的解析规则是：

看起来它会支持

//@ type foo = struct c_struct;

但不像 Ex 2.2.7 那样：

//@ type point = struct { real x; real y; };

为了更好地支持 ACSL/Frama-C 中的结构，我还应该做些什么吗？谢谢！

我经常在其他正式规范中使用集合的基数，我想知道是否可以在带有 WP frama-c 插件的 ACSL 中使用它。

例如，我觉得写 assumes card({*a, *b, *c}) == 3 比 写更清楚assumes *a != *b && *a != *c && *b != *c

问题描述

我正在开发一个 frama-c 插件，它使用切片插件作为库来删除自动生成的代码中未使用的位。不幸的是，切片插件丢弃了一堆实际使用的堆栈值。只要它们的地址包含在传递给抽象外部功能的结构中，就可以使用它们。

简单的例子

这是一个更简单的示例，它模拟了我拥有的相同的一般结构。

frama-c-gui -slice-calls some_function experiment_slicing.c当使用（我还没有弄清楚在没有 gui 的情况下调用命令行时如何查看切片输出）对这个示例进行切片时，它会删除除声明int *a[];和对some_function.

尝试修复

我尝试通过添加 ACSL 注释来修复它。但是，我认为合理的规范（见下文）不起作用

然后我尝试了一个具有所需行为的分配（见下文）。然而，这不是一个正确的规范，因为该函数实际上从未写入指针，而是需要读取它以获得正确的功能。我担心如果我继续使用这种不正确的规范，它会导致奇怪的问题。

我尝试了ACSL 手册中的列表示例（第 37 页上的示例 2.23，在“功能合同”部分），但我隐藏了实现incr_list并更改了返回类型。完整来源如下。

我正在用切片机运行它frama-c test-1.c -slice-calls incr_list -then-last -print。输出看起来不错，但我担心运行此命令时生成的警告：

特别是第一个和第三个。好像有什么意想不到的事情发生了？我不太明白该工具在这里遇到的确切问题。

以下面的 C 代码示例为例。

在我们的例子中，my_entry_point将从程序集中调用，并且*foo这里必须假定它始终是正确的。

使用命令行运行...

... 结果是 ...

当然，我们总是可以添加一个NULL满足检查器的基本情况检查（这可能是我们现在解决这个问题的方法，无论如何）。

但我更好奇（出于学习目的）如何通过例如 ACSL 注释告诉检查器“嘿，我们知道这是指针在理论上可能是无效的 - 但是，请假设，因为它是条目点，它确实有效”。

这是 ACSL 支持的东西，还是可以通过命令行参数更改行为frama-c？我可以理解为什么标准委员会可能会犹豫是否要向 ACSL 添加这样的机制，因为它可能会被滥用，但是看到我刚刚学习 ACSL 的方式，我很想知道这里的常用方法是什么。

我尝试编写 ACSL 谓词以查看整数是否为 2 的幂，如下所示：

但是，当我将一些断言行添加到随机函数中时，会出现一些超时（即失败）。我不明白为什么？

在上一个问题中，我寻求帮助编写 apredicate以查找数字是否为 2 的幂。这是尝试证明以下 C 函数的前奏：

（这个“技巧”来自这里）。使用我尝试过的前一个谓词：

但我使用的各种 SMT 求解器（alt-ergo、z3、gappa、cvc4）似乎都无法证明这一点。

我正在尝试创建一个循环不变量来检查具有偶数索引的数组的所有元素是否都有数字 2（查找素数的程序，在此步骤中它正在生成 SPF）。

但是，当我尝试这个时：

我收到以下错误：

我真的不明白这里发生了什么，但非常感谢任何帮助

我目前正在尝试使用 Frama-C评估一个测试套件，它是插件Eva。为此，我使用以下标志运行 Frama-C：

Frama-C (24.0) 是通过 Opam 安装的。运行 eva 时，一个输出是：

和

正如您在此处看到的：Eva states unsupported ACSL construction。

在查看 string.h ( ~/.opam/default/share/frama-c/libc) 文件时，我能够找到 strcpy 函数：

和 strcmp 函数：

据我了解，Eva 将此文件与 ACSL 合同一起使用，以了解确切需要检查的内容，并为strcmp.

有人知道为什么会出现此错误消息以及如何解决此问题吗？
非常感谢提前！！！