Scroll to navigation

E-ACSL-GCC.SH(1) General Commands Manual E-ACSL-GCC.SH(1)

NAME - instrument and compile C files with E-ACSL

SYNOPSIS [ options ] files

DESCRIPTION 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).


show a help page.
compile the generated and the original (supplied) sources. By default no compilation is performed.
enable runtime debug features, i.e., compile unoptimized executable with assertions and extra checks.
disable stack trace reporting in debug mode
output extra messages when executing generated code
do not compile original code. Has effect only in the presence of the -c flag.
compile the input files as if they were generated by E-ACSL.
pass a value to the Frama-C -debug option. By default the -debug flag is unused.
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).
output the E-ACSL instrumented code to <FILE>. Defaults to a.out.frama.c.
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.
run input source files through Frama-C without E-ACSL instrumentations.
pass additional arguments to the Frama-C pre-processor.
use the Frama-C standard library instead of a system-wide one.
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.
always use GMP integers instead of C integral types. By default the GMP integers are used on as-needed basis.
pass the specified flags to the linker.
pass the specified flags to the pre-processor at compile-time. For instrumentation-time pre-processor flags see --extra-cpp-args option.
suppress any output except for errors and warnings.
redirect all output to a given file.
pass an extra option to a Frama-C invocation.
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.

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
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
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
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.
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


successful execution
invalid user input
instrumentation- or compile-time error


instrument foo.c and output the instrumented code to a.out.frama.c. -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. --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.


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