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
44 -debug 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-mmodel
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 -l, --ld-flags=<FLAGS>
107 pass the specified flags to the linker.
108 -e, --cpp-flags=<FLAGS>
110 pass the specified flags to the pre-processor at compile-time.
111 For instrumentation-time pre-processor flags see --extra-cpp-
112 args option.
113 -q, --quiet
115 suppress any output except for errors and warnings.
116 -s, --logfile=<FILE>
118 redirect all output to a given file.
119 -F, --frama-c-extra=<FLAGS>
121 pass an extra option to a Frama-C invocation.
122 -a, --rte=<OPTSTRING>
124 annotate a source program with assertions using a run of an RTE
125 plugin prior to E-ACSL. OPTSTRING is a comma-separated string
126 that specifies the types of generated assertions. Valid argu‐
127 ments are:
128 signed-overflow - signed integer overflows.
130 unsigned-overflow - unsigned integer overflows.
131 signed-downcast - signed downcast exceeding destination
132 range.
133 unsigned-downcast - unsigned downcast exceeding destination
134 range.
135 mem - pointer or array accesses.
136 float-to-int - casts from floating-point to integer.
137 div - division by zero.
138 shift - left and right shifts by a value out of
139 bounds.
140 ointer-call - annotate functions calls through pointers.
141 all - all of the above.
142 -A, --rte-select=<OPTSTRING>
144 restrict annotations to a given list of functions. OPTSTRING is
145 a comma-separated string comprising function names.
146 --stack-size=<NUMBER>
148 set the size (in MB) of the stack shadow space
149 --heap-size=<NUMBER>
151 set the size (in MB) of the heap shadow space
152 -k, --keep-going
154 continue execution after an assertion failure
155 --free-valid-address
157 trigger failure if a NULL-pointer is used as an input to free
158 function
159 --fail-with-code=<NUMBER>
161 on assertion failure exit with the given integer code intead of
162 raising an abort signal
163 --external-assert=<FILE>
165 the filename that contains your own implementation of
166 __e_acsl_assert
167 -m, --memory-model=<model>
169 memory model (i.e., a runtime library for checking memory
170 related annotations) to be linked against the instrumented file.
171 Valid arguments are:
173 bittree - memory modelling using a Patricia trie.
174 segment - shadow based segment model.
175 By default the Patricia trie memory model is used.
177 --print-mmodels
179 print the names of the supported memory models
180 -I, --frama-c=<FILE>
182 the name of the Frama-C executable. By default the first frama-c
183 executable found in the system path is used.
184 --e-acsl-share=<DIR>
186 the name of the E-ACSL share directory. If not provided, it is
187 computed from your setting.
188 -G, --gcc=<FILE>
190 the name of the GCC executable. By default the first gcc exe‐
191 cutable found in the system path is used.
192 --then separate with a -then the first Frama-C options from the actual
194 launch of the E-ACSL plugin. Prepends -e-acsl-prepare to the
195 list of options passed to Frama-C.
196 --e-acsl-extra=<OPTS>
198 add <OPTS> to the list of options that will be given to the E-
199 ACSL analysis. Only useful when --then is in use, in which case
200 <OPTS> will be placed after the -then on Frama-C's command-line.
201 Otherwise, equivalent to --frama-c-extra
202
204 0 successful execution
205 1 invalid user input
207 Frama-C or GCC error code
209 instrumentation- or compile-time error
210
213 e-acsl-gcc.sh foo.c
214 instrument foo.c and output the instrumented code to a.out.frama.c.
216 e-acsl-gcc.sh -P -c -ogen_foo.c -Ofoo foo.c
218 instrument foo.c, output the instrumented code to gen_foo.c and compile
220 foo.c into foo and gen_foo.c into foo.e-acsl. The -P option specifies
221 that the instrumentation should omit debug functionality.
222 e-acsl-gcc.sh --memory-model=bittree -C gen_foo.c
224 assume gen_foo.c has been instrumented by E-ACSL and compile it into
226 a.out.e-acsl using bittree memory model.
227
230 gcc(1), cpp(1), ld(1), frama-c(1)
231 2016-02-02 E-ACSL-GCC.SH(1)