I am new to Frama-C and wanted to ask what could be causing this issue:

When I run the E-ACSL wrapper script on annotated code with no header files, the a.out.e-acsl file is properly created.

However, when I try to include header files using -E and -I, the wrapper script fails to print anything and does not generate any files.

e-acsl-gcc.sh -E "-I src/include -I ..." main.c

I noticed that this issue happens specifically when the -I option is added.

I am using Frama-C 24.0 (Chromium). Any help would be appreciated. Thanks.

CodePudding user response：

I just added a detail to this answer which should help here: the issue is that e-acsl-gcc.sh cannot handle spaces between -I/-D and its arguments.

GCC accepts both -I dir and -Idir, but for e-acsl-gcc.sh, only -Idir should be used.

So, the following should hopefully work:

e-acsl-gcc.sh -E "-Isrc/include -I..." main.c