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: 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中的语法似乎并未真正实现。看起来类型级别声明的语法是第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; real y; };

我还应该做些其他事以更好地支持ACSL / Frama-C中的结构吗？谢谢！

Answer 1

当前的Frama-C实现并不支持所有的ACSL结构。每个Frama-C版本均随附ACSL实施手册，该手册描述了尚未实施的构造。对于Frama-C 20.0钙，可以找到here。在本文档中，不支持的结构在相关的BNF规则中以红色显示。但是请注意，示例保持不变。对于您而言，这些是第57页的图2.17的规则，这些规则表明确实未实现记录。

您已经发现，确实可以定义一个C struct（可能是ghost）和一个ACSL类型。当然，由于struct生活在C语言世界中，因此其字段必须具有C类型（也不支持在虚幻声明中使用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.};