Provided by: frama-c-base_20220511-manganese-5_amd64 bug

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

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

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), cpp(1), ld(1), frama-c(1)

                                            2016-02-02                           E-ACSL-GCC.SH(1)