NAME¶

SYNOPSIS¶

DESCRIPTION¶

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.

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

-V, --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-mmodel

maximize memory-related instrumentation.

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

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

--stack-size=<NUMBER>

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

--heap-size=<NUMBER>

Set the size (in MB) of the heap 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

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

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.

-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. Prepends -e-acsl-prepare to the list of options passed to Frama-C.

--e-acsl-extra=<OPTS>

Adds <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¶

0

Successful execution

1

Invalid user input

Frama-C or GCC error code

Instrumentation- or compile-time error

EXAMPLES¶

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¶