1
2E-ACSL-GCC.SH(1)            General Commands Manual           E-ACSL-GCC.SH(1)
3
4
5

NAME

7       e-acsl-gcc.sh - instrument and compile C files with E-ACSL
8

SYNOPSIS

10       e-acsl-gcc.sh [ options ] files
11

DESCRIPTION

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

OPTIONS

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
44              -debug 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       -V, --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-mmodel
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       -l, --ld-flags=<FLAGS>
107              pass the specified flags to the linker.
108
109       -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
114       -q, --quiet
115              suppress any output except for errors and warnings.
116
117       -s, --logfile=<FILE>
118              redirect all output to a given file.
119
120       -F, --frama-c-extra=<FLAGS>
121              pass an extra option to a Frama-C invocation.
122
123       -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
129                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
143       -A, --rte-select=<OPTSTRING>
144              Restrict annotations to a given list of functions.  OPTSTRING is
145              a comma-separated string comprising function names.
146
147       --stack-size=<NUMBER>
148              Set the size (in MB) of the stack shadow space
149
150       --heap-size=<NUMBER>
151              Set the size (in MB) of the heap shadow space
152
153       -k, --keep-going
154              Continue execution after an assertion failure
155
156       --free-valid-address
157              Trigger failure if a NULL-pointer is used as an  input  to  free
158              function
159
160       --fail-with-code=<NUMBER>
161              On  assertion failure exit with the given integer code intead of
162              raising an abort signal
163
164       -m, --memory-model=<model>
165              memory model  (i.e.,  a  runtime  library  for  checking  memory
166              related annotations) to be linked against the instrumented file.
167
168              Valid arguments are:
169                bittree     - memory modelling using a Patricia trie.
170                segment     - shadow based segment model.
171
172              By default the Patricia trie  memory model is used.
173
174       --print-models
175              Print the names of the supported memory models
176
177       -I, --frama-c=<FILE>
178              the name of the Frama-C executable. By default the first frama-c
179              executable found in the system path is used.
180
181       -G, --gcc=<FILE>
182              the name of the GCC executable. By default the  first  gcc  exe‐
183              cutable found in the system path is used.
184
185       --then Separate  with a -then the first Frama-C options from the actual
186              launch of the E-ACSL plugin.  Prepends  -e-acsl-prepare  to  the
187              list of options passed to Frama-C.
188
189       --e-acsl-extra=<OPTS>
190              Adds  <OPTS> to the list of options that will be given to the E-
191              ACSL analysis. Only useful when --then is in use, in which  case
192              <OPTS> will be placed after the -then on Frama-C's command-line.
193              Otherwise, equivalent to --frama-c-extra
194

EXIT STATUS

196       0      Successful execution
197
198       1      Invalid user input
199
200       Frama-C or GCC error code
201              Instrumentation- or compile-time error
202
203

EXAMPLES

205       e-acsl-gcc.sh foo.c
206
207       Instrument foo.c and output the instrumented code to a.out.frama.c.
208
209       e-acsl-gcc.sh -P -c -ogen_foo.c -Ofoo foo.c
210
211       Instrument foo.c, output the instrumented code to gen_foo.c and compile
212       foo.c  into foo and gen_foo.c into foo.e-acsl.  The -P option specifies
213       that the instrumentation should omit debug functionality.
214
215       e-acsl-gcc.sh --memory-model=bittree -C gen_foo.c
216
217       Assume gen_foo.c has been instrumented by E-ACSL and  compile  it  into
218       a.out.e-acsl using bittree memory model.
219
220

SEE ALSO

222       gcc(1), cpp(1), ld(1), frama-c(1)
223
224
225
226                                  2016-02-02                  E-ACSL-GCC.SH(1)
Impressum