为什么Frama-C v20.0钙不支持在非全局范围内重新定义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允许使用某些C11构造。当前支持typedef重新定义

但是，出现以下错误：

当前在非全局范围内重新定义typedef不支持

您能帮我解释一下这个情况吗？请注意，如果我使用v12.x-镁，则不会出现此问题。

Answer 1

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

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