Frama-c не может проанализировать приведенный вручную пример ACSL list_length, включающий конструкцию сопоставления с образцом

В следующем определении функции (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 с единственным параметром функции?

P.S. Я использую версию frama-c: Sodium-20150201


formal-verification frama-c
person Necto    schedule 08.09.2015    source источник

Ответы (1)


arrow_upward
2
arrow_downward

Сопоставление с образцом не поддерживается в текущей реализации Frama-C. Чтобы проверить, поддерживается ли ядром конкретная функция ACSL (что не всегда означает, что ваш любимый подключаемый модуль справится с ней), обратитесь к руководство по реализации ACSL. Как упоминалось во вступлении к руководству, каждая запись, выделенная красным цветом, не поддерживается текущей версией Frama-C.

person Virgile    schedule 08.09.2015