Non ghost lvalue when assigning array (frama-c 22)

The following code aborts when using the e-acsl plug-in of frama-c 22.0, while it passes when using frama-c 20.0. I paste the failing case output bellow. The warning mentions lines //@ ghost int acopy[len]; and //@ ghost acopy[i] = a[i];. I am wondering if this is actually not allowed or if it is just a bug?

Regards, Raúl Monti.

#include <stdio.h>

/*@ requires len >= 0;
  @ requires \valid(a+(0..len-1));
  @*/
void add1(int* a, int len) {
    //@ ghost int acopy[len];
    int i;
    for(i = 0; i < len; i++) {
        //@ ghost acopy[i] = a[i];
    }
    for(i = 0; i < len; i++) {
        a[i] = a[i] + 1;
    }
    //@ assert \forall integer i; 0 <= i < len ==> a[i] == acopy[i] + 1;
}

int main() {
    int a[3];
    a[0] = 0;
    a[1] = 1;
    a[2] = 2;
    add1(a, 3);
    return 0;
}

The output I get when running e-acsl-gcc.sh add.c -c -O add in frama-c-22:

e-acsl-gcc.sh add.c -c -O add
+ frama-c -remove-unused-specified-functions -machdep gcc_x86_64 -cpp-extra-args= -std=c99 -D_DEFAULT_SOURCE -D__NO_CTYPE -D__FC_MACHDEP_X86_64  -no-frama-c-stdlib add.c -e-acsl -e-acsl-share=.../.opam/default/bin/../share/frama-c/e-acsl/ -then-last -print -ocode a.out.frama.c
[kernel] Parsing add.c (with preprocessing)
[kernel:ghost:bad-use] add.c:7: Warning: 
  Call to non-ghost function from ghost code is not allowed
[kernel:ghost:bad-use] add.c:10: Warning: 
  '*(acopy + i)' is a non-ghost lvalue, it cannot be assigned in ghost code
[e-acsl] beginning translation.
[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing)
[e-acsl] translation done in project "e-acsl".
[kernel] Warning: warning ghost:bad-use treated as deferred error. See above messages for more information.
[kernel] Frama-C aborted: invalid user input.

added e-acsl label

assigned to @signoles

removed e-acsl label

added bug confirmed kernel labels

assigned to @blanchard and unassigned @signoles

There is indeed a bug with the way ghost VLAs are handled by the kernel. More precisely, VLAs are translated into pointers (+ allocation/deallocation using some Frama-C builtins), but the ghost status is lost during this translation.

More precisely, we should have builtins for allocating and freeing ghost VLA.

And we should fix ghost status of pointed memory.