Search code examples
cframa-c

Why Frama-C v20.0 Calcium does not support redefinition of a typedef in a non-global scope

I am trying to analyze the following C program:

#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;
}

As typedef is redefined in function "main", I followed the user manual of Frama-C and used the option -c11.

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

However, I got the following error:

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

Could you please help me explain this case? Note that I don't have this problem if I use v12.x - Magnesium.

Solution

  • It seems frama-c does not support redefining a typedef symbol in a local scope.

    The C Standard allows this, and it might be useful to support automatically generated code, but doing this on purpose seems a good way to create confusion for readers and maintainers of the code.