|E-ACSL-GCC.SH(1)||General Commands Manual||E-ACSL-GCC.SH(1)|
e-acsl-gcc.sh - instrument and compile C files with E-ACSL
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.
- 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 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.
- 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.
- 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.
- -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.
- set the size (in MB) of the stack shadow space
- set the size (in MB) of the heap shadow space
- -k, --keep-going
- 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
- -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 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.
- 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.
- 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
- Frama-C or GCC error code
- instrumentation- or compile-time error
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.