在以下函数定义(list.c)中:
//@ type list<A> = Nil | Cons(A,list<A>);
/*@ logic integer list_length<A>(list<A> l) =
@ \match l {
@ case Nil : 0
@ case Cons(h,t) : 1 + list_length(tail)
@ };
*/
frama-c 失败并显示以下消息:
$ frama-c -wp -wp-rte list.c
[jessie3] Loading Why3 configuration...
[jessie3] Why3 environment loaded.
[jessie3] Loading Why3 theories...
[jessie3] Loading Why3 modules...
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing list.c (with preprocessing)
list.c:4:[kernel] user error: unexpected token 'l'
[kernel] user error: stopping on file "list.c" that has errors. Add '-kernel-msg-key pp'
for preprocessing command.
[kernel] Frama-C aborted: invalid user input.
该示例直接取自ACSL 手册。为什么它l
与函数的唯一参数相关联时遇到麻烦?
PS我使用frama-c版本:Sodium-20150201