.\"------------------------------------------------------------------------ .\" .\" This file is part of the Frama-C's E-ACSL plug-in. .\" .\" Copyright (C) 2012-2020 .\" CEA (Commissariat à l'énergie atomique et aux énergies .\" alternatives) .\" .\" you can redistribute it and/or modify it under the terms of the GNU .\" Lesser General Public License as published by the Free Software .\" Foundation, version 2.1. .\" .\" It is distributed in the hope that it will be useful, .\" but WITHOUT ANY WARRANTY; without even the implied warranty of .\" MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the .\" GNU Lesser General Public License for more details. .\" .\" See the GNU Lesser General Public License version 2.1 .\" for more details (enclosed in the file licenses/LGPLv2.1). .\" .\"------------------------------------------------------------------------ .TH E-ACSL-GCC.SH 1 2016-02-02 .SH NAME .B e-acsl-gcc.sh \- instrument and compile C files with E-ACSL .SH SYNOPSIS .B e-acsl-gcc.sh [ .I options ] .I files .SH DESCRIPTION .B e-acsl-gcc.sh is a convenience wrapper for instrumentation of C programs using the \fBE-ACSL\fP \fBFrama-C\fP plugin and their subsequent compilation using the GNU compiler collection (\fBGCC\fP). .SH OPTIONS .TP .B -h, --help show a help page. .TP .B -c, --compile compile the generated and the original (supplied) sources. By default no compilation is performed. .TP .B -D, --rt-debug enable runtime debug features, i.e., compile unoptimized executable with assertions and extra checks. .TP .B --no-trace disable stack trace reporting in debug mode .TP .B -V, --rt-verbose output extra messages when executing generated code .TP .B -X, --instrumented-only do not compile original code. Has effect only in the presence of the \fI-c\fP flag. .TP .B -C, --compile-only compile the input files as if they were generated by \fBE-ACSL\fP. .TP .B -d, --debug=\fI pass a value to the \fBFrama-C\fP -\fIdebug\fP option. By default the -\fIdebug\fP flag is unused. .TP .B -v, --verbose=\fI pass a value to the \fBFrama-C\fP -\fIverbose\fP option. By default the -\fIverbose\fP flag is unused. .TP .B --check check integrity of the generated AST (mostly useful for developers). .TP .B -o, --ocode=\fI output the \fBE-ACSL\fP instrumented code to \fI\fP. Defaults to \fIa.out.frama.c\fP. .TP .B -O, --oexec=\fI output the code compiled from the uninstrumented sources to \fI\fP. The executable compiled from the files generated by \fBE-ACSL\fP is appended the \fI.e.acsl\fP suffix. Unless specified, the names of the executables generated from the original and the modified programs are \fIa.out\fP and \fIa.out.e-acsl\fP respectively. .TP .B --oexec-e-acsl=\fI name of the executable file generated from the \fBE-ACSL\fP-instrumented file. Unless specified, the executable is named as inidicated by the \fB--oexec\fP option. .TP .B -f, --frama-c-only run input source files through \fBFrama-C\fP without \fBE-ACSL\fP instrumentations. .TP .B -E, --extra-cpp-args=\fI pass additional arguments to the \fBFrama-C\fP pre-processor. .TP .B -L, --frama-c-stdlib use the \fBFrama-C\fP standard library instead of a system-wide one. .TP .B -M, --full-mtracking maximize memory-related instrumentation. .TP .B --temporal enable checking for temporal memory errors in \\\fBvalid\fP and \\\fBvalid_read\fP predicates. .TP .B --weak-validity enable notion of weak validity. By default expression \fB(p+i)\fP, where \fBp\fP is a pointer and \fBi\fP is an integer offset is deemed valid if both addresses \fBp\fP and \fB(p+i)\fP belong to the same allocated block. With weak validity \fB(p+i)\fP is valid if the memory location which address is given by expression \fB(p+i)\fP is allocated. .TP .B --validate-format-strings enable built-in detection of format-string vulnerabilities. .TP .B --libc-replacements replace some of the unsafe LIBC functions (e.g., strcpy, memcpy) with RTL alternatives that include internal runtime error checking. .TP .B -g, --gmp always use GMP integers instead of C integral types. By default the GMP integers are used on as-needed basis. .TP .B -l, --ld-flags=\fI pass the specified flags to the linker. .TP .B -e, --cpp-flags=\fI pass the specified flags to the pre-processor at compile-time. For instrumentation-time pre-processor flags see \fB--extra-cpp-args\fP option. .TP .B -q, --quiet suppress any output except for errors and warnings. .TP .B -s, --logfile=\fI redirect all output to a given file. .TP .B -F, --frama-c-extra=\fI pass an extra option to a \fBFrama-C\fP invocation. .TP .B -a, --rte=\fI annotate a source program with assertions using a run of an RTE plugin prior to E-ACSL. \fIOPTSTRING\fP is a comma-separated string that specifies the types of generated assertions. Valid arguments are: \fIsigned-overflow\fP \- signed integer overflows. \fIunsigned-overflow\fP \- unsigned integer overflows. \fIsigned-downcast\fP \- signed downcast exceeding destination range. \fIunsigned-downcast\fP \- unsigned downcast exceeding destination range. \fImem\fP \- pointer or array accesses. \fIfloat-to-int\fP \- casts from floating-point to integer. \fIdiv\fP \- division by zero. \fIshift\fP \- left and right shifts by a value out of bounds. \fpointer-call\fP \- annotate functions calls through pointers. \fIall\fP \- all of the above. .TP .B -A, --rte-select=\fI restrict annotations to a given list of functions. \fIOPTSTRING\fP is a comma-separated string comprising function names. .TP .B --stack-size=\fI set the size (in MB) of the stack shadow space .TP .B --heap-size=\fI set the size (in MB) of the heap shadow space .TP .B -k, --keep-going continue execution after an assertion failure .TP .B --free-valid-address trigger failure if a NULL-pointer is used as an input to free function .TP .B --fail-with-code=\fI on assertion failure exit with the given integer code intead of raising an abort signal .TP .B --external-assert=\fI the filename that contains your own implementation of __e_acsl_assert .TP .B -m, --memory-model=\fI memory model (i.e., a runtime library for checking memory related annotations) to be linked against the instrumented file. Valid arguments are: \fIbittree\fP \- memory modelling using a Patricia trie. \fIsegment\fP \- shadow based segment model. By default the Patricia trie memory model is used. .TP .B --print-mmodels print the names of the supported memory models .TP .B -I, --frama-c=\fI the name of the \fBFrama-C\fP executable. By default the first \fIframa-c\fP executable found in the system path is used. .TP .B --e-acsl-share=\fI the name of the \fBE-ACSL\fP share directory. If not provided, it is computed from your setting. .TP .B -G, --gcc=\fI the name of the \fBGCC\fP executable. By default the first \fIgcc\fP executable found in the system path is used. .TP .B --then separate with a \fB-then\fP the first \fBFrama-C\fP options from the actual launch of the \fBE-ACSL\fP plugin. .TP .B --e-acsl-extra=\fI add \fI\fP to the list of options that will be given to the \fBE-ACSL\fP analysis. Only useful when \fB--then\fP is in use, in which case \fI\fP will be placed after the \fB-then\fP on \fBFrama-C\fP's command-line. Otherwise, equivalent to \fB--frama-c-extra\fP .SH EXIT STATUS .TP .B 0 successful execution .TP .B 1 invalid user input .TP .B \fBFrama-C\fP or \fBGCC\fP error code instrumentation- or compile-time error .SH EXAMPLES .B e-acsl-gcc.sh foo.c instrument foo.c and output the instrumented code to \fIa.out.frama.c\fP. .B e-acsl-gcc.sh -P -c -ogen_foo.c -Ofoo foo.c instrument \fIfoo.c\fP, output the instrumented code to \fIgen_foo.c\fP and compile \fIfoo.c\fP into \fIfoo\fP and \fIgen_foo.c\fP into \fIfoo.e-acsl\fP. The \fB-P\fP option specifies that the instrumentation should omit debug functionality. .B e-acsl-gcc.sh --memory-model=bittree -C gen_foo.c assume \fIgen_foo.c\fP has been instrumented by \fBE-ACSL\fP and compile it into \fIa.out.e-acsl\fP using \fBbittree\fP memory model. .SH SEE ALSO \fBgcc\fP(1), \fBcpp\fP(1), \fBld\fP(1), \fBframa-c\fP(1)