--- name: "e-acsl-gcc.sh" section: "1" platform: "linux" package: "frama-c-base" version: "20220511-manganese-3+b4" release: "Debian 12 (Bookworm)" platforms: ["linux"] url: "https://new.carta.tech/e-acsl-gcc.sh" --- # e-acsl-gcc.sh(1) instrument and compile C files with E-ACSL ## 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=*\*** pass a value to the **Frama-C** -*debug* option. By default the -*debug* flag is unused. - **-v, --verbose=*\*** 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=*\*** output the **E-ACSL** instrumented code to *\*. Defaults to *a.out.frama.c*. - **-O, --oexec=*\*** output the code compiled from the uninstrumented sources to *\*. 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=*\*** 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=*\*** 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=*\*** 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=*\*** pass the specified flags to the linker. - **-e, --cpp-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=*\*** redirect all output to a given file. - **-F, --frama-c-extra=*\*** pass an extra option to a **Frama-C** invocation. - **-a, --rte=*\*** 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=*\*** restrict annotations to a given list of functions. *OPTSTRING* is a comma-separated string comprising function names. - **--zone-sizes=*\*** 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=*\*** 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=*\*** the filename that contains your own implementation of \_\_e\_acsl\_assert - **--external-print-value=*\*** the filename that contains your own implementation of \_\_e\_acsl\_print\_value - **-m, --memory-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=*\*** the name of the **Frama-C** executable. By default the first *frama-c* executable found in the system path is used. - **--e-acsl-share=*\*** the name of the **E-ACSL** share directory. If not provided, it is computed from your setting. - **-G, --gcc=*\*** 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=*\*** add *\* to the list of options that will be given to the **E-ACSL** analysis. Only useful when **--then** is in use, in which case *\* will be placed after the **-then** on **Frama-C**'s command-line. Otherwise, equivalent to **--frama-c-extra**. - **--ar=*\*** 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=*\*** 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=*\*** use *\* 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=*\*** compile dlmalloc library with *\* compile flags. Default to *-O2 -g3*. Unused if **--dlmalloc-from-sources** or **--dlmalloc-compile-only** isn't used. - **--odlmalloc=*\*** output compiled dlmalloc library to *\*. 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)](/gcc/1.md), [**cpp**(1)](/cpp/1.md), [**ld**(1)](/ld/1.md), [**frama-c**(1)](/frama-c/1.md)