frama-c - ACSL 逻辑结构声明不像引用手册中那样工作

Question

我想要一种方法来描述包含抽象列表的逻辑/规范级结构。 ACSL Reference Manual 的第 27 页上的示例 2.2.7表明有一个 方法如下:

//@ type point = struct { real x; real y; };
//@ type triangle = point[3];
//@ logic point origin = { .x = 0.0 , .y = 0.0 };
/*@ logic triangle t_iso = { [0] = origin,
@ [1] = { .y = 2.0 , .x = 0.0 }
@ [2] = { .x = 2.0 , .y = 0.0 }};
@*/
/*@ logic point centroid(triangle t) = {
@ .x = mean3(t[0].x,t[1].x,t[2].x);
@ .y = mean3(t[0].y,t[1].y,t[2].y);
@ };
@*/
//@ type polygon = point[];
/*@ logic perimeter(polygon p) =
@ \sum(0,\length(p)-1,\lambda integer i;d(p[i],p[(i+1) % \length(p)])) ;
@*/

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

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

我得到一个错误:

[kernel:annot-error] shapes.c:1: 警告:意外的标记 '{'

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

struct somestruct {
     int x;
     int y;
 };

/*@
     logic struct somestruct foo = { .x = 3, .y = 4 };
*/

我仍然遇到错误:

[kernel:annot-error] aggregate_err.c:7: Warning:
  unsupported aggregated field construct. Ignoring global annotation

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

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

| STRUCT exit_rt_type identifier_or_typename { LTstruct $3 }

看起来会支持

//@type foo = struct c_struct;

但不像 Ex 2.2.7 中的那样:

//@type point = struct { real x;真实的你； };

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

Answer 1

当前的 Frama-C 实现不支持所有 ACSL 结构。每个 Frama-C 版本都附带一个 ACSL 实现手册，其中描述了尚未实现的结构。对于 Frama-C 20.0 钙，可以找到 here .在本文档中，相关 BNF 规则中未支持的结构显示为红色。但是请注意，手册的其他部分保持不变。值得注意的是，实现手册中包含示例的事实并不意味着它有望被当前的 Frama-C 版本成功解析。在您的情况下，这些是第 57 页上图 2.17 的规则，这表明确实没有实现记录。

正如您自己已经发现的那样，确实可以定义一个 C struct(可能是 ghost)和一个 ACSL 类型。当然，由于 struct 存在于 C 世界中，它的字段必须具有 C 类型(也不支持 ghost 声明中的 ACSL 类型)。

类似地，您可以通过对任意记录的所有字段进行更新(\with 构造)来模拟不存在直接记录定义，如下例所示:

//@ ghost struct c_s { float x; float y; };

//@ type point = struct c_s;

//@ axiomatic Arbitrary_point { logic point empty; }

//@ logic point my_point = {{ empty \with .x = (float)1. } \with .y = (float)2.};