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