Scroll to navigation

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

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

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 concurrency support.
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.
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.
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.
pointer-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 given zones.

Valid zone names are:
stack - stack shadow space
heap - heap shadow space
tls - TLS shadow space
thread-stack - thread stack 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
print data contributing to the failed assertion along with the runtime error message
do notprint data contributing to the failed assertion along with the runtime error message
the filename that contains your own implementation of __e_acsl_assert
the filename that contains your own implementation of __e_acsl_print_value
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.
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.
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.
use <FILE> instead of distributed dlmalloc library.
compile and use dlmalloc library from sources instead of using the distributed library. Incompatible with --with-dlmalloc.
do not instrument or compile code, only compile dlmalloc library from sources. Implies --dlmalloc-from-sources and incompatible with --with-dlmalloc.
compile dlmalloc library with <FLAGS> compile flags. Default to -O2 -g3. Unused if --dlmalloc-from-sources or --dlmalloc-compile-only isn't used.
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
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