为什么 frama-c 会产生语法错误？答案

【问题标题】：Why does frama-c yield a syntax error on this?为什么 frama-c 会产生语法错误？
【发布时间】：2014-04-30 20:29:30
【问题描述】：

这是一个从一个更大的程序中缩减的快速测试用例，该程序使用 frama-c NEON 产生了语法错误：

cat <<"EOF" > min.i
struct list;
typedef struct list list_t;
void list_merge(list_t *, list_t *, int (const void *, const void *));
EOF
frama-c -val min.i

frama-c 是否仅限于我在这里违反的 c99 的某个子集？

【问题讨论】：

您几乎已经收到了bts.frama-c.com/my_view_page.php 的错误报告。您只需要包含观察到的行为（“min.i:3:[kernel] user error: syntax error”）和期望的行为（程序接受，因为“gcc -c -Wall -std=c99 -pedantic min.i”接受它）。
输入程序可以进一步简化为void list_merge(int(int));。这个简化的程序可以重写为void list_merge(int (*)(int));（我认为它是等效的），以便被 Frama-C 接受，以防万一。我什至不知道第一种形式是否可以接受，所以我不会在这里责怪 Frama-C。

标签： c frama-c

【解决方案1】：

void list_merge(int(int)); 被 Clang 和 GCC 接受，但被http://cdecl.org/拒绝

这似乎是有效的语法（相关的是抽象声明器在 C11 中的 6.7.7:1 的定义）：

抽象声明器：指针指针_opt 直接抽象声明符直接抽象声明符：（抽象声明者） direct-abstract-declarator_opt [ type-qualifier-listopt assignment-expressionopt ] 直接抽象声明符_opt [静态类型限定符列表_opt 赋值表达式] 直接抽象声明符_opt [类型限定符列表静态赋值表达式] 直接抽象声明符_opt [ * ] 直接抽象声明符_opt ( 参数类型列表_opt )

换句话说，是的，似乎 Frama-C 仅限于函数参数的非奇怪抽象声明符的子集。这可能是一个简单的遗漏，如果您报告它可能会得到修复。

【讨论】：