1E-ACSL-GCC.SH(1) General Commands Manual E-ACSL-GCC.SH(1)
3
7 e-acsl-gcc.sh - instrument and compile C files with E-ACSL
8
10 e-acsl-gcc.sh [ options ] files
11
13 e-acsl-gcc.sh is a convenience wrapper for instrumentation of C pro‐
14 grams using the E-ACSL Frama-C plugin and their subsequent compilation
15 using the GNU compiler collection (GCC).
16
18 -h, --help
19 show a help page.
20 -c, --compile
22 compile the generated and the original (supplied) sources. By
23 default no compilation is performed.
24 -D, --rt-debug
26 enable runtime debug features, i.e., compile unoptimized exe‐
27 cutable with assertions and extra checks.
28 --no-trace
30 disable stack trace reporting in debug mode
31 -V, --rt-verbose
33 output extra messages when executing generated code
34 -X, --instrumented-only
36 do not compile original code. Has effect only in the presence of
37 the -c flag.
38 -C, --compile-only
40 compile the input files as if they were generated by E-ACSL.
41 -d, --debug=<N>
43 pass a value to the Frama-C -debug option. By default the -de‐
44 bug flag is unused.
45 -v, --verbose=<N>
47 pass a value to the Frama-C -verbose option. By default the
48 -verbose flag is unused.
49 --check
51 check integrity of the generated AST (mostly useful for develop‐
52 ers).
53 -o, --ocode=<FILE>
55 output the E-ACSL instrumented code to <FILE>. Defaults to
56 a.out.frama.c.
57 -O, --oexec=<FILE>
59 output the code compiled from the uninstrumented sources to
60 <FILE>. The executable compiled from the files generated by E-
61 ACSL is appended the .e.acsl suffix. Unless specified, the
62 names of the executables generated from the original and the
63 modified programs are a.out and a.out.e-acsl respectively.
64 --oexec-e-acsl=<FILE>
66 name of the executable file generated from the E-ACSL-instru‐
67 mented file. Unless specified, the executable is named as ini‐
68 dicated by the --oexec option.
69 -f, --frama-c-only
71 run input source files through Frama-C without E-ACSL instrumen‐
72 tations.
73 -E, --extra-cpp-args=<FLAGS>
75 pass additional arguments to the Frama-C pre-processor.
76 -L, --frama-c-stdlib
78 use the Frama-C standard library instead of a system-wide one.
79 -M, --full-mtracking
81 maximize memory-related instrumentation.
82 --concurrency
84 enable concurrency support.
85 --temporal
87 enable checking for temporal memory errors in \valid and
88 \valid_read predicates.
89 --weak-validity
91 enable notion of weak validity. By default expression (p+i),
92 where p is a pointer and i is an integer offset is deemed valid
93 if both addresses p and (p+i) belong to the same allocated
94 block. With weak validity (p+i) is valid if the memory location
95 which address is given by expression (p+i) is allocated.
96 --validate-format-strings
98 enable built-in detection of format-string vulnerabilities.
99 --libc-replacements
101 replace some of the unsafe LIBC functions (e.g., strcpy, memcpy)
102 with RTL alternatives that include internal runtime error check‐
103 ing.
104 -g, --gmp
106 always use GMP integers instead of C integral types. By default
107 the GMP integers are used on as-needed basis.
108 --mbits=<BITS>
110 architecture to compile to. Valid arguments are 16, 32 or 64.
111 Default to the architecture of the current environment. This
112 option is used to select the machdep when calling Frama-C, and
113 to pass the corresponding -m16, -m32 or -m64 flag to the com‐
114 piler.
115 -l, --ld-flags=<FLAGS>
117 pass the specified flags to the linker.
118 -e, --cpp-flags=<FLAGS>
120 pass the specified flags to the pre-processor at compile-time.
121 For instrumentation-time pre-processor flags see --extra-cpp-
122 args option.
123 -q, --quiet
125 suppress any output except for errors and warnings.
126 -s, --logfile=<FILE>
128 redirect all output to a given file.
129 -F, --frama-c-extra=<FLAGS>
131 pass an extra option to a Frama-C invocation.
132 -a, --rte=<OPTSTRING>
134 annotate a source program with assertions using a run of an RTE
135 plugin prior to E-ACSL. OPTSTRING is a comma-separated string
136 that specifies the types of generated assertions. Valid argu‐
137 ments are:
138 signed-overflow - signed integer overflows.
140 unsigned-overflow - unsigned integer overflows.
141 signed-downcast - signed downcast exceeding destination
142 range.
143 unsigned-downcast - unsigned downcast exceeding destination
144 range.
145 mem - pointer or array accesses.
146 float-to-int - casts from floating-point to integer.
147 div - division by zero.
148 shift - left and right shifts by a value out of
149 bounds.
150 pointer-call - annotate functions calls through pointers.
151 all - all of the above.
152 -A, --rte-select=<OPTSTRING>
154 restrict annotations to a given list of functions. OPTSTRING is
155 a comma-separated string comprising function names.
156 --zone-sizes=<NAME1:SIZE1,...,NAMEN:SIZEN>
158 set the size (in MB) of the given zones.
159 Valid zone names are:
161 stack - stack shadow space
162 heap - heap shadow space
163 tls - TLS shadow space
164 thread-stack - thread stack shadow space
165 -k, --keep-going
167 continue execution after an assertion failure
168 --free-valid-address
170 trigger failure if a NULL-pointer is used as an input to free
171 function
172 --fail-with-code=<NUMBER>
174 on assertion failure exit with the given integer code intead of
175 raising an abort signal
176 --assert-print-data
178 print data contributing to the failed assertion along with the
179 runtime error message
180 --no-assert-print-data
182 do notprint data contributing to the failed assertion along with
183 the runtime error message
184 --external-assert=<FILE>
186 the filename that contains your own implementation of
187 __e_acsl_assert
188 --external-print-value=<FILE>
190 the filename that contains your own implementation of
191 __e_acsl_print_value
192 -m, --memory-model=<model>
194 memory model (i.e., a runtime library for checking memory re‐
195 lated annotations) to be linked against the instrumented file.
196 Valid arguments are:
198 bittree - memory modelling using a Patricia trie.
199 segment - shadow based segment model.
200 By default the Patricia trie memory model is used.
202 --print-mmodels
204 print the names of the supported memory models
205 -I, --frama-c=<FILE>
207 the name of the Frama-C executable. By default the first frama-c
208 executable found in the system path is used.
209 --e-acsl-share=<DIR>
211 the name of the E-ACSL share directory. If not provided, it is
212 computed from your setting.
213 -G, --gcc=<FILE>
215 the name of the GCC executable. By default the first gcc exe‐
216 cutable found in the system path is used.
217 --then separate with a -then the first Frama-C options from the actual
219 launch of the E-ACSL plugin.
220 --then-last
222 separate with a -then-last the first Frama-C options from the
223 actual launch of the E-ACSL plugin.
224 --e-acsl-extra=<OPTS>
226 add <OPTS> to the list of options that will be given to the E-
227 ACSL analysis. Only useful when --then is in use, in which case
228 <OPTS> will be placed after the -then on Frama-C's command-line.
229 Otherwise, equivalent to --frama-c-extra.
230 --ar=<FILE>
232 the name of the AR executable. Only relevant with --dlmalloc-
233 from-sources. By default the first ar executable found in the
234 system path is used.
235 --ranlib=<FILE>
237 the name of the RANLIB executable. Only relevant with --dlmal‐
238 loc-from-sources. By default the first ranlib executable found
239 in the system path is used.
240 --with-dlmalloc=<FILE>
242 use <FILE> instead of distributed dlmalloc library.
243 --dlmalloc-from-sources
245 compile and use dlmalloc library from sources instead of using
246 the distributed library. Incompatible with --with-dlmalloc.
247 --dlmalloc-compile-only
249 do not instrument or compile code, only compile dlmalloc library
250 from sources. Implies --dlmalloc-from-sources and incompatible
251 with --with-dlmalloc.
252 --dlmalloc-compile-flags=<FLAGS>
254 compile dlmalloc library with <FLAGS> compile flags. Default to
255 -O2 -g3. Unused if --dlmalloc-from-sources or --dlmalloc-com‐
256 pile-only isn't used.
257 --odlmalloc=<FILE>
259 output compiled dlmalloc library to <FILE>. Unused if --dlmal‐
260 loc-from-sources or --dlmalloc-compile-only isn't used.
261
264 0 successful execution
265 1 invalid user input
267 Frama-C or GCC error code
269 instrumentation- or compile-time error
270
273 e-acsl-gcc.sh foo.c
274 instrument foo.c and output the instrumented code to a.out.frama.c.
276 e-acsl-gcc.sh -c -ogen_foo.c -Ofoo foo.c
278 instrument foo.c, output the instrumented code to gen_foo.c and compile
280 foo.c into foo and gen_foo.c into foo.e-acsl.
281 e-acsl-gcc.sh --memory-model=bittree -C gen_foo.c
283 assume gen_foo.c has been instrumented by E-ACSL and compile it into
285 a.out.e-acsl using bittree memory model.
286
289 gcc(1), cpp(1), ld(1), frama-c(1)
290 2016-02-02 E-ACSL-GCC.SH(1)