e-acsl-gcc.sh - Man Page

instrument and compile C files with E-ACSL


e-acsl-gcc.sh [ options ] files


e-acsl-gcc.sh is a convenience wrapper for instrumentation of C programs using the E-ACSL Frama-C plugin and their subsequent compilation using the GNU compiler collection (GCC).


-h,  --help

show a help page.

-c,  --compile

compile the generated and the original (supplied) sources. By default no compilation is performed.

-D,  --rt-debug

enable runtime debug features, i.e., compile unoptimized executable with assertions and extra checks.


disable stack trace reporting in debug mode

-V,  --rt-verbose

output extra messages when executing generated code

-X,  --instrumented-only

do not compile original code. Has effect only in the presence of the -c flag.

-C,  --compile-only

compile the input files as if they were generated by E-ACSL.

-d,  --debug=<N>

pass a value to the Frama-C -debug option. By default the -debug flag is unused.

-v,  --verbose=<N>

pass a value to the Frama-C -verbose option. By default the -verbose flag is unused.


check integrity of the generated AST (mostly useful for developers).

-o,  --ocode=<FILE>

output the E-ACSL instrumented code to <FILE>. Defaults to a.out.frama.c.

-O,  --oexec=<FILE>

output the code compiled from the uninstrumented sources to <FILE>. The executable compiled from the files generated by E-ACSL is appended the .e.acsl suffix. Unless specified, the names of the executables generated from the original and the modified programs are a.out and a.out.e-acsl respectively.


name of the executable file generated from the E-ACSL-instrumented file. Unless specified, the executable is named as inidicated by the --oexec option.

-f,  --frama-c-only

run input source files through Frama-C without E-ACSL instrumentations.

-E,  --extra-cpp-args=<FLAGS>

pass additional arguments to the Frama-C pre-processor.

-L,  --frama-c-stdlib

use the Frama-C standard library instead of a system-wide one.

-M,  --full-mtracking

maximize memory-related instrumentation.


enable checking for temporal memory errors in \valid and \valid_read predicates.


enable notion of weak validity. By default expression (p+i), where p is a pointer and i is an integer offset is deemed valid if both addresses p and (p+i) belong to the same allocated block. With weak validity (p+i) is valid if the memory location which address is given by expression (p+i) is allocated.


enable built-in detection of format-string vulnerabilities.


replace some of the unsafe LIBC functions (e.g., strcpy, memcpy) with RTL alternatives that include internal runtime error checking.

-g,  --gmp

always use GMP integers instead of C integral types. By default the GMP integers are used on as-needed basis.

-l,  --ld-flags=<FLAGS>

pass the specified flags to the linker.

-e,  --cpp-flags=<FLAGS>

pass the specified flags to the pre-processor at compile-time. For instrumentation-time pre-processor flags see --extra-cpp-args option.

-q,  --quiet

suppress any output except for errors and warnings.

-s,  --logfile=<FILE>

redirect all output to a given file.

-F,  --frama-c-extra=<FLAGS>

pass an extra option to a Frama-C invocation.

-a,  --rte=<OPTSTRING>

annotate a source program with assertions using a run of an RTE plugin prior to E-ACSL. OPTSTRING is a comma-separated string that specifies the types of generated assertions. Valid arguments are:

 signed-overflow   - signed integer overflows.
 unsigned-overflow - unsigned integer overflows.
 signed-downcast   - signed downcast exceeding destination range.
 unsigned-downcast - unsigned downcast exceeding destination range.
 mem               - pointer or array accesses.
 float-to-int      - casts from floating-point to integer.
 div               - division by zero.
 shift             - left and right shifts by a value out of bounds.
 ointer-call       - annotate functions calls through pointers.
 all               - all of the above.

-A,  --rte-select=<OPTSTRING>

restrict annotations to a given list of functions. OPTSTRING is a comma-separated string comprising function names.


set the size (in MB) of the stack shadow space


set the size (in MB) of the heap shadow space

-k,  --keep-going

continue execution after an assertion failure


trigger failure if a NULL-pointer is used as an input to free function


on assertion failure exit with the given integer code intead of raising an abort signal


the filename that contains your own implementation of __e_acsl_assert

-m,  --memory-model=<model>

memory model (i.e., a runtime library for checking memory related annotations) to be linked against the instrumented file.

Valid arguments are:
 bittree     - memory modelling using a Patricia trie.
 segment     - shadow based segment model.

By default the Patricia trie  memory model is used.


print the names of the supported memory models

-I,  --frama-c=<FILE>

the name of the Frama-C executable. By default the first frama-c executable found in the system path is used.


the name of the E-ACSL share directory. If not provided, it is computed from your setting.

-G,  --gcc=<FILE>

the name of the GCC executable. By default the first gcc executable found in the system path is used.


separate with a -then the first Frama-C options from the actual launch of the E-ACSL plugin.


add <OPTS> to the list of options that will be given to the E-ACSL analysis. Only useful when --then is in use, in which case <OPTS> will be placed after the -then on Frama-C's command-line. Otherwise, equivalent to --frama-c-extra

Exit Status


successful execution


invalid user input

Frama-C or GCC error code

instrumentation- or compile-time error


e-acsl-gcc.sh foo.c

instrument foo.c and output the instrumented code to a.out.frama.c.

e-acsl-gcc.sh -P -c -ogen_foo.c -Ofoo foo.c

instrument foo.c, output the instrumented code to gen_foo.c and compile foo.c into foo and gen_foo.c into foo.e-acsl. The -P option specifies that the instrumentation should omit debug functionality.

e-acsl-gcc.sh --memory-model=bittree -C gen_foo.c

assume gen_foo.c has been instrumented by E-ACSL and compile it into a.out.e-acsl using bittree memory model.

See Also

gcc(1), cpp(1), ld(1), frama-c(1)