c - 为什么 Frama-C v20.0 Calcium 不支持在非全局范围内重新定义 typedef

Question

我正在尝试分析以下 C 程序:

#include <stdio.h>

typedef struct a {
    int x;
    char y;
} alias;

int main()
{
    typedef struct b {
         int x;
         int y;
    } alias;

    alias *var = (unsigned long*) 0x12345678;
    var->y = 0x00;

    return 0;
}

由于在函数“main”中重新定义了 typedef，我遵循了 Frama-C 的用户手册并使用了选项 -c11。

-c11 allows the use of some C11 constructs. Currently supported are typedefs redefinition

但是，我收到以下错误:

redefinition of a typedef in a non-global scope is currently unsupported

你能帮我解释一下这个案例吗？
请注意，如果我使用 v12.x - Magnesium，则没有这个问题。

Answer 1

似乎 frama-c 不支持在本地范围内重新定义 typedef 符号。

C 标准允许这样做，并且支持自动生成的代码可能很有用，但故意这样做似乎是给代码的读者和维护者制造困惑的好方法。