How can be C files linked when using E-ACSL plugin?

Question

I am trying to generate an annotated file with Frama-C E-ACSL plugin. I created the following files:

• Insert.c: contains all the structures to create a linked list.
• AxiomTest.c: includes the main function where the asserts it must fulfil are indicated. All functions and structures are determined in terms of Insert.c file

When compiling/instrumenting a program the manual specifies the following terminal command:

$ e-acsl-gcc.sh -c <files> -O <output>

For a successful compilation Insert.c and AxiomTest.c must be linked but I cannot find any flag for that.

Any help? Or is there any other way to do it right?

Answer 1

e-acsl-gcc.sh does compile and link files with option -c, despite looking like it only compiles (the -c here is unrelated to GCC's -c option, which does only compilation, without linking).

If you want to give extra flags to the linker, man e-acsl-gcc.sh (or e-acsl-gcc.sh -h) will indicate option -l:

-l         pass additional options to the linker