我在指定对内部状态变量的访问时遇到问题,即那些仅由 getter 和 setter 访问的模块的本地变量。我曾尝试在setter函数的函数契约规范中使用getter函数,但是frama-c返回错误:
> frama-c -wp -wp-rte -verbose 0 intstate.c intstate.h
...
intstate.h:4:[kernel] user error: unexpected token ')'
[kernel] user error: skipping file "intstate.c" that has errors.
[kernel] Frama-C aborted: invalid user input.
这是标题:
int get_state(void);
/*@
@ ensures val == get_state();
@*/
void set_state(int val);
这里是来源:
#include "intstate.h"
static int the_state = 0;
int get_state(void) {
return the_state;
}
void set_state(int val) {
the_state = val;
}
我认为这是一个普遍的问题。在 ACSL 中是如何完成的?有没有人有类似问题的例子?
我使用 Frama-C Fluorine-20130601。
提前致谢
坦率
编辑: 重新阅读 ACSL 规范更仔细地向我揭示了 C 函数在规范中是不可能的,只有逻辑函数。我试图将 C 函数包装在一个逻辑函数中,但这也没有被接受,同样的错误消息。我最终通过一个幽灵变量对内部状态变量进行了建模,但我不确定这是否是体面的方法。