Support for `sizeof T[n]` in the Frama-C framework

I am wondering how difficult it would be to add rudimentary support for something like sizeof T[n] (which to my knowledge is an explicit C construct for a variable length array), to be used in a dynamic allocation context such as malloc.

My experiments so far have shown that it is not supported (well?) in Frama-C. So my questions are: What would be required to implement it, in any capacity? What about kernel support? What about the development of an analysis domain for Eva, that can make use of such a feature in relations over allocated memory?

Here is an example that uses sizeof(T[n]) (supposing that malloc always succeeds):

#include <stdlib.h>

int *foo(int n, int x)
{
    int *a = malloc(sizeof(int[n]));
    a[n - 1] = x;
    return a;
}

This is clearly not accepted by the Frama-C (version 29.0 [Copper]) kernel. It prints this message:

[kernel] mem.c:5: User Error: 
  Array length n is not a compile-time constant,
  and currently VLAs may only have their first dimension as variable.

Question: What could make this work? I do not expect it to be easy to add complete support.

Here is yet another example which makes use of a (pointer to a) variable length array. This compiles fine with gcc (GCC) 14.2.1 (w/ flag -c):

#include <assert.h>
#include <stdlib.h>

int *foo(int n, int x)
{
    int (*a)[n] = malloc(sizeof(int[n])); // shamelessly crude cast
    assert(sizeof(*a) == sizeof(int[n])); // this holds (at runtime)
    (*a)[n - 1] = x;
    return (*a);
}

AFAIK, this is the most that the C language can "accommodate" the direct semantics I am hinting at, yet this vital information about *a is still lost upon the conclusion of foo(). Due to similar issues with the previous, this example is also not accepted by Frama-C.

Basically, this requires to completely rearchitecture the way VLA are handled in Frama-C: currently, as a heritage of the original CIL library, they are treated as pointers allocated with a built-in alloca function (and freed at the end of the enclosing block). There are many other reasons to change that and make VLA first-class citizens in the Frama-C AST, but this is clearly not a completely trivial change.