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 -V, --rt-verbose
30 Output extra messages when executing generated code
31
32 -X, --instrumented-only
33 Do not compile original code. Has effect only in the presence of
34 the -c flag.
35
36 -C, --compile-only
37 compile the input files as if they were generated by E-ACSL.
38
39 -d, --debug=<N>
40 pass a value to the Frama-C -debug option. By default the
41 -debug flag is unused.
42
43 -v, --verbose=<N>
44 pass a value to the Frama-C -verbose option. By default the
45 -verbose flag is unused.
46
47 -V, --check
48 check integrity of the generated AST (mostly useful for develop‐
49 ers).
50
51 -o, --ocode=<FILE>
52 output the E-ACSL instrumented code to <FILE>. Defaults to
53 a.out.frama.c.
54
55 -O, --oexec=<FILE>
56 output the code compiled from the uninstrumented sources to
57 <FILE>. The executable compiled from the files generated by E-
58 ACSL is appended the .e.acsl suffix. Unless specified, the
59 names of the executables generated from the original and the
60 modified programs are a.out and a.out.e-acsl respectively.
61
62 --oexec-e-acsl=<FILE>
63 name of the executable file generated from the E-ACSL-instru‐
64 mented file. Unless specified, the executable is named as ini‐
65 dicated by the --oexec option.
66
67 -f, --frama-c-only
68 run input source files through Frama-C without E-ACSL instrumen‐
69 tations.
70
71 -E, --extra-cpp-args=<FLAGS>
72 pass additional arguments to the Frama-C pre-processor.
73
74 -L, --frama-c-stdlib
75 use the Frama-C standard library instead of a system-wide one.
76
77 -M, --full-mmodel
78 maximize memory-related instrumentation.
79
80 --temporal
81 enable checking for temporal memory errors in \valid and
82 \valid_read predicates.
83
84 --weak-validity
85 enable notion of weak validity. By default expression (p+i),
86 where p is a pointer and i is an integer offset is deemed valid
87 if both addresses p and (p+i) belong to the same allocated
88 block. With weak validity (p+i) is valid if the memory location
89 which address is given by expression (p+i) is allocated.
90
91 -g, --gmp
92 always use GMP integers instead of C integral types. By default
93 the GMP integers are used on as-needed basis.
94
95 -l, --ld-flags=<FLAGS>
96 pass the specified flags to the linker.
97
98 -e, --cpp-flags=<FLAGS>
99 pass the specified flags to the pre-processor at compile-time.
100 For instrumentation-time pre-processor flags see --extra-cpp-
101 args option.
102
103 -q, --quiet
104 suppress any output except for errors and warnings.
105
106 -s, --logfile=<FILE>
107 redirect all output to a given file.
108
109 -F, --frama-c-extra=<FLAGS>
110 pass an extra option to a Frama-C invocation.
111
112 -a, --rte=<OPTSTRING>
113 annotate a source program with assertions using a run of an RTE
114 plugin prior to E-ACSL. OPTSTRING is a comma-separated string
115 that specifies the types of generated assertions. Valid argu‐
116 ments are:
117
118 signed-overflow - signed integer overflows.
119 unsigned-overflow - unsigned integer overflows.
120 signed-downcast - signed downcast exceeding destination
121 range.
122 unsigned-downcast - unsigned downcast exceeding destination
123 range.
124 mem - pointer or array accesses.
125 float-to-int - casts from floating-point to integer.
126 div - division by zero.
127 shift - left and right shifts by a value out of
128 bounds.
129 ointer-call - annotate functions calls through pointers.
130 all - all of the above.
131
132 -A, --rte-select=<OPTSTRING>
133 Restrict annotations to a given list of functions. OPTSTRING is
134 a comma-separated string comprising function names.
135
136 --stack-size=<NUMBER>
137 Set the size (in MB) of the stack shadow space
138
139 --heap-size=<NUMBER>
140 Set the size (in MB) of the heap shadow space
141
142 -k, --keep-going
143 Continue execution after an assertion failure
144
145 --free-valid-address
146 Trigger failure if a NULL-pointer is used as an input to free
147 function
148
149 --fail-with-code=<NUMBER>
150 On assertion failure exit with the given integer code intead of
151 raising an abort signal
152
153 -m, --memory-model=<model>
154 memory model (i.e., a runtime library for checking memory
155 related annotations) to be linked against the instrumented file.
156
157 Valid arguments are:
158 bittree - memory modelling using a Patricia trie.
159 segment - shadow based segment model.
160
161 By default the Patricia trie memory model is used.
162
163 --print-models
164 Print the names of the supported memory models
165
166 -I, --frama-c=<FILE>
167 the name of the Frama-C executable. By default the first frama-c
168 executable found in the system path is used.
169
170 -G, --gcc=<FILE>
171 the name of the GCC executable. By default the first gcc exe‐
172 cutable found in the system path is used.
173
174 --then Separate with a -then the first Frama-C options from the actual
175 launch of the E-ACSL plugin. Prepends -e-acsl-prepare to the
176 list of options passed to Frama-C.
177
178 --e-acsl-extra=<OPTS>
179 Adds <OPTS> to the list of options that will be given to the E-
180 ACSL analysis. Only useful when --then is in use, in which case
181 <OPTS> will be placed after the -then on Frama-C's command-line.
182 Otherwise, equivalent to --frama-c-extra
183
185 0 Successful execution
186
187 1 Invalid user input
188
189 Frama-C or GCC error code
190 Instrumentation- or compile-time error
191
192
194 e-acsl-gcc.sh foo.c
195
196 Instrument foo.c and output the instrumented code to a.out.frama.c.
197
198 e-acsl-gcc.sh -P -c -ogen_foo.c -Ofoo foo.c
199
200 Instrument foo.c, output the instrumented code to gen_foo.c and compile
201 foo.c into foo and gen_foo.c into foo.e-acsl. The -P option specifies
202 that the instrumentation should omit debug functionality.
203
204 e-acsl-gcc.sh --memory-model=bittree -C gen_foo.c
205
206 Assume gen_foo.c has been instrumented by E-ACSL and compile it into
207 a.out.e-acsl using bittree memory model.
208
209
211 gcc(1), cpp(1), ld(1), frama-c(1)
212
213
214
215 2016-02-02 E-ACSL-GCC.SH(1)