尝试使用归纳谓词时的语法错误

Syntax error when trying to use inductive predicate

来源: link 标签:frama-c 更新时间:

  问题

我正在尝试使用来自网页 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}: 
         orall list* root; reachable(root,root); 
       case next_reachable{L}: 
         orall list* root, *node; 
         alid(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}: orall struct List* l; reachable(l, l);
      case non_empty{L}: orall list *l1,*l2;
        alid(l1) && reachable(l1->next, l2) ==> reachable(l1, l2);
    }
*/

也许我做错了什么?虽然我试图做的只是复制和粘贴教程代码.任何帮助赞赏.

  最佳答案

它确实很难找到,但在归罪>之前的−不是标准的ASCII dash -,而是其无数的unicode变体之一.这就是Frama-C感到困惑.当然,这在手写代码中不会发生,您有正常的-.

  相同标签的其他问题

frama-c
上一个问题:
下一个问题: