2

我想有一种方法来描述包含抽象列表的逻辑/规范级别结构。ACSL 参考手册第 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: Warning: unexpected token '{'

如果我放弃尝试编写结构类型的逻辑/规范级别声明，但仍想编写实例化 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 中的语法并没有真正实现。看起来类型级别声明的语法是 frama-c-20.0-Calcium/src/kernel_internals/parsing/logic_parser.mly 的第 799 行（称为 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; real y; };

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

4

1 回答 1

2

当前的 Frama-C 实现并不支持所有的 ACSL 结构。每个 Frama-C 版本都附带一个 ACSL 实施手册，其中描述了尚未实施的结构。对于 Frama-C 20.0 钙，可在此处找到。在本文档中，不支持的结构在相关 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.};
于 2019-12-27T17:49:54.147 回答