e-acsl-gcc.sh - Man Page

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.

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

-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 preprocessor at compile-time. For instrumentation-time preprocessor 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.

--then-last

separate with a -then-last 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.

0

successful execution

1

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

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