Issue when parsing versus printing and parsing
<!-- Thank you for submitting an issue to the Frama-C team. We propose the following template to ease the process. Please directly edit it inline to provide the required information. Before submitting the issue, please verify: - the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues); - you installed Frama-C as prescribed in the [instructions](INSTALL.md). If the issue applies to a specific Frama-C plug-in, please prefix the title by the plug-in name: [Eva], [WP], [E-ACSL]… --> ### Steps to reproduce the issue <!-- Please indicate here steps to follow to get a [minimal, complete, and verifiable example](https://stackoverflow.com/help/mcve) which reproduces 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: ```C /*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) <!-- You may add here any information deemed relevant with regard to this issue, and tell us if you already tried some workarounds or have some ideas to solve this issue. -->
issue