Search code examples
cframa-cacsl

How to include header files with E-ACSL wrapper script?

I am new to Frama-C and wanted to ask how I could add header files when using the E-ACSL wrapper script. Normally, I've been adding header files the following way with WP and RTE:

frama-c -rte main.c -cpp-extra-args="-I src/include -I ..."

However, I am unsure of how I can include these files when using the wrapper script.

e-acsl-gcc.sh --rte=all -c main.c

Without the header files I run into the following error:

[kernel] Parsing main.c (with preprocessing)/main.c:10:10: fatal error: header.h: No such file or directory #include "header.h"

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

Solution

  • If you run e-acsl-gcc.sh -h, you'll get a help message with the script's options:

    Options:
  -h         show this help page
  -c         compile instrumented code
  (...)
  -E         pass additional arguments to the Frama-C preprocessor
  -F         pass additional options to the Frama-C command line
  (...)

    The two above are relevant for you: -E adds arguments to an implicit -cpp-extra-args used by the script, while -F allows you to add the option itself.

    So, you can either run:

    e-acsl-gcc.sh -E "-Isrc/include -I..." <other options and source files>

    Or:

    e-acsl-gcc.sh -F -cpp-extra-args="-Isrc/include,-I..." <other options and source files>

    Note that with -F, due to quoting issues (between e-acsl-gcc.sh, Frama-C's command-line, C preprocessor, etc), you may need to replace spaces with commas, as in "-Isrc/include,-I...".

    Important: do not add spaces between -I and the directory name. Due to parsing issues, e-acsl-gcc.sh will not parse it correctly if you do. GCC accepts both syntaxes anyway, so I'd recommend getting used to not adding spaces after -I (and -D as well) in general.

    Overall, using -E is better here, but -F can be used to pass other options besides -cpp-extra-args.