Issue when parsing versus printing and parsing

Steps to reproduce the issue

Running frama-c -meta example.c -then -wp first,
then frama-c -meta example.c -then-last -print -ocode meta_example.c
and frama-c -wp meta_example.c with the code below or the attached file:

/*example.c*/
#include <string.h>

typedef struct sub_type {
    int tag;
} sub_type;

typedef struct {
    int *ptr;
    int foo[sizeof(sub_type)];
} TEST_TYPE;

int main(){
    TEST_TYPE *ctx;
    memcpy(ctx->foo, ctx->ptr, sizeof(ctx->foo));
    return 0;
}

/*@  
    meta \prop, 
    \name(test_property), \targets(\ALL),
    \context(\writing), \valid( \written);
*/

Expected behaviour

Running the last two commands should result in Wp trying to prove any found properties.

Actual behaviour

Frama-C fails to parse the code output by frama-c -meta example.c -then-last -print -ocode meta_example.c, despite it being the same as the one observed in the GUI with frama-c-gui -meta example.c -then -wp

Contextual information

• Frama-C installation mode: Opam
• Frama-C version: 28.1 (Nickel) (as reported by frama-c -version)
• Plug-in used: Wp and MetAcsl, although the issue seems more related to how Frama-C parses the function contract for memcpy
• OS name: Ubuntu
• OS version: 20.04.6 LTS

FYI @nkosmatov

Additional information (optional)