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

0
votes

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?

1
frama-cacsl
Did you try e-acsl-gcc.sh -c Insert.c AxiomTest.c -O my_executable? Normally the script should accept many source files as argument (hence <files> and not <file> in the manual). - Virgile
Doing e-acsl-gcc.sh -c Insert.c AxiomTest.c -O my_executable links both files, but I still get an error that says: unbound function foo. This function foo is defined in the Intert.c file, and it is called in AxiomTest.c inside a @ requires clause from the EACSL annotations. Could be that EACSL does not accept a function in the annotation and generates an error? - Raul Coroban
you can't call C functions (although you can refer to them as function pointer, e.g. my_fct_ptr == f1 || my_fct_ptr == f2) inside an ACSL annotationsindeed: only logic functions and predicates are allowed there. And of course, if errors happen before the link stage, no executable will be produced. If you have specific issues with the errors reported by Frama-C/E-ACSL, please create a new question, and be sure to include a MCVE showing us the exact problem you're facing. - Virgile

1 Answers

0
votes

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