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 --external-assert=<FILE>
172 the filename that contains your own implementation of
173 __e_acsl_assert
174 -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 Valid arguments are:
180 bittree - memory modelling using a Patricia trie.
181 segment - shadow based segment model.
182 By default the Patricia trie memory model is used.
184 --print-mmodels
186 print the names of the supported memory models
187 -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 --e-acsl-share=<DIR>
193 the name of the E-ACSL share directory. If not provided, it is
194 computed from your setting.
195 -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 --then separate with a -then the first Frama-C options from the actual
201 launch of the E-ACSL plugin.
202 --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 --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 --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 --with-dlmalloc=<FILE>
220 use <FILE> instead of distributed dlmalloc library.
221 --dlmalloc-from-sources
223 compile and use dlmalloc library from sources instead of using
224 the distributed library. Incompatible with --with-dlmalloc.
225 --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 --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 --odlmalloc=<FILE>
237 output compiled dlmalloc library to <FILE>. Unused if --dlmal‐
238 loc-from-sources or --dlmalloc-compile-only isn't used.
239
242 0 successful execution
243 1 invalid user input
245 Frama-C or GCC error code
247 instrumentation- or compile-time error
248
251 e-acsl-gcc.sh foo.c
252 instrument foo.c and output the instrumented code to a.out.frama.c.
254 e-acsl-gcc.sh -c -ogen_foo.c -Ofoo foo.c
256 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 e-acsl-gcc.sh --memory-model=bittree -C gen_foo.c
261 assume gen_foo.c has been instrumented by E-ACSL and compile it into
263 a.out.e-acsl using bittree memory model.
264
267 gcc(1), cpp(1), ld(1), frama-c(1)
268 2016-02-02 E-ACSL-GCC.SH(1)