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 --temporal
84 enable checking for temporal memory errors in \valid and
85 \valid_read predicates.
86 --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 --validate-format-strings
95 enable built-in detection of format-string vulnerabilities.
96 --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 -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 --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 -l, --ld-flags=<FLAGS>
114 pass the specified flags to the linker.
115 -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 -q, --quiet
122 suppress any output except for errors and warnings.
123 -s, --logfile=<FILE>
125 redirect all output to a given file.
126 -F, --frama-c-extra=<FLAGS>
128 pass an extra option to a Frama-C invocation.
129 -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 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 -A, --rte-select=<OPTSTRING>
151 restrict annotations to a given list of functions. OPTSTRING is
152 a comma-separated string comprising function names.
153 --stack-size=<NUMBER>
155 set the size (in MB) of the stack shadow space
156 --heap-size=<NUMBER>
158 set the size (in MB) of the heap shadow space
159 -k, --keep-going
161 continue execution after an assertion failure
162 --free-valid-address
164 trigger failure if a NULL-pointer is used as an input to free
165 function
166 --fail-with-code=<NUMBER>
168 on assertion failure exit with the given integer code intead of
169 raising an abort signal
170 --assert-print-data
172 print data contributing to the failed assertion along with the
173 runtime error message
174 --no-assert-print-data
176 do notprint data contributing to the failed assertion along with
177 the runtime error message
178 --external-assert=<FILE>
180 the filename that contains your own implementation of
181 __e_acsl_assert
182 --external-print-value=<FILE>
184 the filename that contains your own implementation of
185 __e_acsl_print_value
186 -m, --memory-model=<model>
188 memory model (i.e., a runtime library for checking memory re‐
189 lated annotations) to be linked against the instrumented file.
190 Valid arguments are:
192 bittree - memory modelling using a Patricia trie.
193 segment - shadow based segment model.
194 By default the Patricia trie memory model is used.
196 --print-mmodels
198 print the names of the supported memory models
199 -I, --frama-c=<FILE>
201 the name of the Frama-C executable. By default the first frama-c
202 executable found in the system path is used.
203 --e-acsl-share=<DIR>
205 the name of the E-ACSL share directory. If not provided, it is
206 computed from your setting.
207 -G, --gcc=<FILE>
209 the name of the GCC executable. By default the first gcc exe‐
210 cutable found in the system path is used.
211 --then separate with a -then the first Frama-C options from the actual
213 launch of the E-ACSL plugin.
214 --e-acsl-extra=<OPTS>
216 add <OPTS> to the list of options that will be given to the E-
217 ACSL analysis. Only useful when --then is in use, in which case
218 <OPTS> will be placed after the -then on Frama-C's command-line.
219 Otherwise, equivalent to --frama-c-extra.
220 --ar=<FILE>
222 the name of the AR executable. Only relevant with --dlmalloc-
223 from-sources. By default the first ar executable found in the
224 system path is used.
225 --ranlib=<FILE>
227 the name of the RANLIB executable. Only relevant with --dlmal‐
228 loc-from-sources. By default the first ranlib executable found
229 in the system path is used.
230 --with-dlmalloc=<FILE>
232 use <FILE> instead of distributed dlmalloc library.
233 --dlmalloc-from-sources
235 compile and use dlmalloc library from sources instead of using
236 the distributed library. Incompatible with --with-dlmalloc.
237 --dlmalloc-compile-only
239 do not instrument or compile code, only compile dlmalloc library
240 from sources. Implies --dlmalloc-from-sources and incompatible
241 with --with-dlmalloc.
242 --dlmalloc-compile-flags=<FLAGS>
244 compile dlmalloc library with <FLAGS> compile flags. Default to
245 -O2 -g3. Unused if --dlmalloc-from-sources or --dlmalloc-com‐
246 pile-only isn't used.
247 --odlmalloc=<FILE>
249 output compiled dlmalloc library to <FILE>. Unused if --dlmal‐
250 loc-from-sources or --dlmalloc-compile-only isn't used.
251
254 0 successful execution
255 1 invalid user input
257 Frama-C or GCC error code
259 instrumentation- or compile-time error
260
263 e-acsl-gcc.sh foo.c
264 instrument foo.c and output the instrumented code to a.out.frama.c.
266 e-acsl-gcc.sh -c -ogen_foo.c -Ofoo foo.c
268 instrument foo.c, output the instrumented code to gen_foo.c and compile
270 foo.c into foo and gen_foo.c into foo.e-acsl.
271 e-acsl-gcc.sh --memory-model=bittree -C gen_foo.c
273 assume gen_foo.c has been instrumented by E-ACSL and compile it into
275 a.out.e-acsl using bittree memory model.
276
279 gcc(1), cpp(1), ld(1), frama-c(1)
280 2016-02-02 E-ACSL-GCC.SH(1)