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
