我想有一种方法来描述包含抽象列表的逻辑/规范级别结构。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 中的结构,我还应该做些什么吗?谢谢!