Синтаксическая ошибка при попытке использовать индуктивный предикат - PullRequest
Новая
       42

Синтаксическая ошибка при попытке использовать индуктивный предикат

1 голос
/ 27 сентября 2019

Я пытаюсь использовать пример индуктивного предиката, взятого с веб-страницы https://frama -c.com / acsl_tutorial_index.html : 

#include <stddef.h>
#include <stdlib.h>

typedef struct _list { int element; struct _list* next; } list; 

/*@ inductive reachable{L} (list* root, list* node) { 
       case root_reachable{L}: 
         \forall list* root; reachable(root,root); 
       case next_reachable{L}: 
         \forall list* root, *node; 
         \valid(root) ==>
            reachable(root−>next, node) ==> 
              reachable(root,node); 
     } 
*/

Однако я получаюошибка компиляции: 

$ frama-c -wp -wp-rte -wp-split list.c
[kernel] Parsing list.c (with preprocessing)
[kernel:annot-error] list.c:12: Warning: unexpected token '>'
[kernel] User Error: warning annot-error treated as fatal error.
[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.

Кажется, я получаю ошибку для root->next.

Если я попробую следующее, это сработает: 

/*@ inductive reachable{L} (list* root, list* node) {
      case empty{L}: \forall struct List* l; reachable(l, l);
      case non_empty{L}: \forall list *l1,*l2;
        \valid(l1) && reachable(l1->next, l2) ==> reachable(l1, l2);
    }
*/

Возможно, я 'что-то не так сделал?Хотя все, что я пытался сделать, это скопировать и вставить учебный код.Любая помощь приветствуется.

1 Ответ

1 голос
/ 27 сентября 2019

Это действительно трудно заметить, но − непосредственно перед инкриминированным > - это не стандартная ASCII-черта -, а один из бесчисленных вариантов Unicode.Это то, что запутывает Frama-C.Конечно, это не происходит в рукописном коде, где у вас есть нормальный -.

...