Provided by: frama-c-base_20220511-manganese-1.3_amd64 
NAME
e-acsl-gcc.sh - instrument and compile C files with E-ACSL
SYNOPSIS
e-acsl-gcc.sh [ options ] files
DESCRIPTION
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).
OPTIONS
-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.
--no-trace
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
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.
--oexec-e-acsl=<FILE>
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.
--concurrency
enable concurrency support.
--temporal
enable checking for temporal memory errors in \valid and \valid_read predicates.
--weak-validity
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.
--validate-format-strings
enable built-in detection of format-string vulnerabilities.
--libc-replacements
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.
--mbits=<BITS>
architecture to compile to. Valid arguments are 16, 32 or 64. Default to the
architecture of the current environment. This option is used to select the machdep
when calling Frama-C, and to pass the corresponding -m16, -m32 or -m64 flag to the
compiler.
-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.
pointer-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.
--zone-sizes=<NAME1:SIZE1,...,NAMEN:SIZEN>
set the size (in MB) of the given zones.
Valid zone names are:
stack - stack shadow space
heap - heap shadow space
tls - TLS shadow space
thread-stack - thread stack shadow space
-k, --keep-going
continue execution after an assertion failure
--free-valid-address
trigger failure if a NULL-pointer is used as an input to free function
--fail-with-code=<NUMBER>
on assertion failure exit with the given integer code intead of raising an abort
signal
--assert-print-data
print data contributing to the failed assertion along with the runtime error
message
--no-assert-print-data
do notprint data contributing to the failed assertion along with the runtime error
message
--external-assert=<FILE>
the filename that contains your own implementation of __e_acsl_assert
--external-print-value=<FILE>
the filename that contains your own implementation of __e_acsl_print_value
-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-mmodels
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.
--e-acsl-share=<DIR>
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.
--then separate with a -then the first Frama-C options from the actual launch of the E-
ACSL plugin.
--e-acsl-extra=<OPTS>
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.
--ar=<FILE>
the name of the AR executable. Only relevant with --dlmalloc-from-sources. By
default the first ar executable found in the system path is used.
--ranlib=<FILE>
the name of the RANLIB executable. Only relevant with --dlmalloc-from-sources. By
default the first ranlib executable found in the system path is used.
--with-dlmalloc=<FILE>
use <FILE> instead of distributed dlmalloc library.
--dlmalloc-from-sources
compile and use dlmalloc library from sources instead of using the distributed
library. Incompatible with --with-dlmalloc.
--dlmalloc-compile-only
do not instrument or compile code, only compile dlmalloc library from sources.
Implies --dlmalloc-from-sources and incompatible with --with-dlmalloc.
--dlmalloc-compile-flags=<FLAGS>
compile dlmalloc library with <FLAGS> compile flags. Default to -O2 -g3. Unused if
--dlmalloc-from-sources or --dlmalloc-compile-only isn't used.
--odlmalloc=<FILE>
output compiled dlmalloc library to <FILE>. Unused if --dlmalloc-from-sources or
--dlmalloc-compile-only isn't used.
EXIT STATUS
0 successful execution
1 invalid user input
Frama-C or GCC error code
instrumentation- or compile-time error
EXAMPLES
e-acsl-gcc.sh foo.c
instrument foo.c and output the instrumented code to a.out.frama.c.
e-acsl-gcc.sh -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.
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)
2016-02-02 E-ACSL-GCC.SH(1)