Changelog 261 KB
Newer Older
1
2
3
4
5
6
7
8
###############################################################################
# Preliminary notes:                                                          #
# ------------------                                                          #
# Mark "-": change with an impact for users (and possibly developers).        #
# Mark "o": change with an impact for developers only.                        #
# Mark "+": change for Frama-C-commits audience (not in html version).        #
# Mark "*": bug fixed.                                                        #
# Mark "!": change that can break compatibility with existing development.    #
9
# '##nnn'  : Public Gitlab (pub/frama-c) issue
10
11
# '#@nnn'  : Gitlab frama-c/frama-c issue                                     #
# For compatibility with old change log formats:                              #
12
13
# '#nnn'   : BTS entry #nnn (OBSOLETE)                                        #
# '#!nnn'  : BTS private entry #nnn  (OBSOLETE)                               #
14
15
16
# '#?nnn'  : OLD-BTS entry #nnn                                               #
###############################################################################

17
18
19
20
##################################
Open Source Release <next-release>
##################################

21
22
-   Kernel    [2022-10-05] Support for ghost VLA and calls to builtins with
              ghost arguments.
Allan Blanchard's avatar
Allan Blanchard committed
23
-   Eva       [2022-09-16] Numerors now needs MLMPFR 4.1.0+bugfix2
Andre Maroneze's avatar
Andre Maroneze committed
24
-   Kernel    [2022-09-07] Improve error message for invalid options -D/-I/-U.
Allan Blanchard's avatar
Allan Blanchard committed
25
26
o!  Configure [2022-07-28] Removed autoconf and configure
o!  Makefile  [2022-07-11] Removed Makefile, Frama-C is now built using Dune 3.x
Patrick Baudin's avatar
Patrick Baudin committed
27
o!  Pdg       [2022-07-01] Removed from Db. Use proper Pdg API instead.
28
29
-!  Kernel    [2022-06-06] Remove journalisation.

30
31
32
33
####################################
Open Source Release 25.0 (Manganese)
####################################

34
35
o   Kernel    [2022-05-03] Prototype of AST comparison between two versions
              of the same program, via the new option -ast-diff.
David Bühler's avatar
David Bühler committed
36
-   Eva       [2022-05-02] Fixes stack overflow errors on very large C functions.
37
38
39
40
41
-   Eva       [2022-04-25] Improve the multidim abstract domain: it is now
              more precise and more robust, it is able to infer simple array
              invariants on some loops without unrolling, and has a new option
              -eva-multidim-disjunctive-invariants to infer structures
              disjunctive invariants.
42
43
o   Kernel    [2022-03-07] Known compiler builtins are no longer hardcoded in
              OCaml, but defined via JSON files (in share/compliance).
Andre Maroneze's avatar
Andre Maroneze committed
44
45
46
o   Kernel    [2022-02-23] New visitor functions visitFramacFileFunctions
              and visitCilFileFunctions to visit only function definitions,
              for better performance.
47
o!  Kernel    [2022-02-23] Remove State_selection.Static (deprecated since
48
              10 years, use directly State_selection instead)
Andre Maroneze's avatar
Andre Maroneze committed
49
50
-*  Kernel    [2022-02-22] Fix list of potential types for decimal
              integer literal constants
51
52
*   Kernel    [2022-02-17] Reject programs using unsupported
              vector_size attribute (fixes ##2573)
53
54
55
56
o   Eva       [2022-02-15] New API to run the analysis and access its results,
              intended to replace the old API in Db.Value. It is more precise
              as it uses all available domains to evaluate values and locations.
              See file Eva.mli for more details.
57
58
*   Kernel    [2022-02-08] Reject array whose size is too big with a proper
              error message instead of a crash (fixes ##2590)
59
60
61
o!  Kernel    [2022-02-19] Removed obsolete AST nodes IndexPI and Info
*   Kernel    [2022-02-08] Reject array whose size is too big with a proper
              error message instead of a crash (fixes ##2590)
62
63
64
o!  Kernel    [2021-12-03] Remove unused AST node Dcustom_annot and field
              fpadding_in_bits. Do not cache size of types in the AST but in
              a dedicated table.
Allan Blanchard's avatar
Allan Blanchard committed
65
-*  Logic     [2021-11-30] Fix type of expressions whose value are functions
66
o!  Kernel    [2021-11-29] Integer.pretty does not have the optional argument
67
68
69
              hexa anymore. Use Integer.pretty_hex or Integer.pp_hex if you
              want to print integers in hexadecimal format.

70
71
72
73
###################################
Open Source Release 24.0 (Chromium)
###################################

Andre Maroneze's avatar
Andre Maroneze committed
74
75
76
77
-*  Eva       [2022-01-19] Always emits alarms about initialization, escaping
              pointers and special floating-point values for the arguments of
              calls to functions without body (or whose body is not analyzed),
              even when -eva-warn-copy-indeterminate is unset.
Virgile Prevosto's avatar
Virgile Prevosto committed
78
79
80
81
82
83
84
-   ACSL      [2021-10-28] better type checks for volatile clauses
-   Variadic  [2021-10-26] translates printf/scanf calls even if formatting
              string is not constant, warning that it will assume arguments
              match the format.
-   Kernel    [2021-10-26] Support for C11's  _Static_assert
-   Libc      [2021-10-26] Frama-C's libc #define _STDC_NO_COMPLEX as mandated by
              ISO C11 for libraries without support for complex numbers
David Bühler's avatar
David Bühler committed
85
86
87
88
-   Eva       [2021-10-19] New options to allow states partitioning to survive
              function returns: -eva-interprocedural-split for disjunctions
              from split annotations, and -eva-interprocedural-history for
              disjunctions from the -eva-partition-history option.
89
90
91
92
93
94
95
96
97
98
99
-   Eva       [2021-10-14] Supports the evaluation of ACSL set comprehension.
-   Eva       [2021-10-14] On a SIGINT signal (Ctrl-C), the analysis is stopped
              but partial results are saved if option -save is set.
-*  Eva       [2021-10-12] Always checks the arguments of builtin calls for
              alarms about initialization, escaping pointers and special
              floating-point values, unless -eva-warn-copy-indeterminate is set.
-*  Kernel    [2021-10-11] Fixes crashes on C integer constants overflowing
              ocaml integers.
-   Eva       [2021-10-06] Improves the precision of the octagon domain on
              unsigned variables.
-*  Eva       [2021-10-06] Fixes a soundness bug in the octagon domain on
David Bühler's avatar
David Bühler committed
100
              integer downcasts wrapping around.
101
-   Eva       [2021-09-10] Improves the symbolic-locations domain precision.
102
103
-   Kernel    [2021-09-02] 0-sized flexible array members only available in
              gcc_* machdeps, that now also support FAM in nested struct.
104
105
106
107
108
109
110
-   Eva       [2021-07-26] Removes the maximum limit of option -eva-ilevel.
-   Eva       [2021-07-26] New \tainted predicate to evaluate if the value of an
              expression is tainted according to the taint domain.
-o  Eva       [2021-07-25] Changes the Domain_builder.Complete functor to
              automatically build more abstract domain functions.
-*  Eva       [2021-06-24] Fixes a soundness bug of the bitwise domain with the
              memexec cache.
Basile Desloges's avatar
Basile Desloges committed
111
112
113
-*  Variadic  [2021-06-23] Create a fallback specialisation if there is an error
              while translating a variadic call so that no variadic call are
              left in the AST after Variadic.
114
115
116
117
118
-   Eva       [2021-06-22] Reduction of "garbled mix" values by \valid and
              \valid_read ACSL predicates.
-   Eva       [2021-06-15] New experimental multidim domain to improve analysis
              precision on arrays of structures and multidimensional arrays.
-*  Eva       [2021-06-10] Fixes a crash in the octagon domain.
Allan Blanchard's avatar
Allan Blanchard committed
119
120
o   Kernel    [2021-06-10] New module Cil_builder, simplifies C and ACSL code
                           generation.
121
o   Ptests    [2021-06-03] Add new PLUGIN directive and new predefined macros.
122
123
124
125
126
127
128
129
130
131
132
-   Eva       [2021-06-01] Annotations split and dynamic_split can be applied
              to logic predicates (in addition to terms).
-   Eva       [2021-06-01] New annotation dynamic_split, similar to split, but
              separates the analysis w.r.t. the current value of an expression
              instead of the value it had at the annotation point: the partition
              can be changed at an assignment to ensure that the expression
              always evaluates to a singleton in each analysis state.
-   Eva       [2021-05-20] New taint analysis via an experimental taint domain.
              New annotations //@ taint … (for statements) and //@ taints … (in
              function contracts) to initiate taint on lvalues.
              Tainted properties can then be seen in the future GUI Ivette.
133
134
-   Eva       [2021-05-11] Support for ACSL predicate \is_infinite.

Allan Blanchard's avatar
Allan Blanchard committed
135
136
137
138
###################################
Open Source Release 23.1 (Vanadium)
###################################

139
140
141
###################################
Open Source Release 23.0 (Vanadium)
###################################
Julien Signoles's avatar
Julien Signoles committed
142

143
144
-*  Kernel    [2021-04-26] Do not crash on _Alignof(void): accept or properly
              reject, depending on machdep. Fixes pub/frama-c#2551
145
146
147
148
149
-   Eva       [2021-04-21] Partial support for recursion:
              new option -eva-unroll-recursive-calls to precisely analyze the n
              first recursive calls, before using the function specification
              to interpret the remaining calls.
              The unsound option -eva-ignore-recursive-calls has been removed.
Julien Signoles's avatar
Julien Signoles committed
150
151
152
153
154
155
-!  RTE       [2021-04-16] -rte-initialized takes a set of functions as
                           parameter (defaults to none)
-   RTE       [2021-04-16] No more initialization warnings for full structures
                           and unions reads. Initialization warnings for other
                           types *without* trap representation. Refer to the
                           documentation for more details.
Andre Maroneze's avatar
Andre Maroneze committed
156
157
-*  Kernel    [2021-04-16] Pretty prints array formals in their original form.
              Fixes pub/frama-c#392
Allan Blanchard's avatar
Allan Blanchard committed
158
159
160
161
o!  Kernel    [2021-04-13] Removed deprecated function Filepath.pretty
o!  Kernel    [2021-04-13] Filepath directories functions now return
              Filepath.Normalized.t, Frama-C configuration and plugin
              configuration getters updated accordingly
Basile Desloges's avatar
Basile Desloges committed
162
163
o!  Kernel    [2021-04-09] Change the type of the measure from string to
              logic_info in the variant AST node.
Patrick Baudin's avatar
Patrick Baudin committed
164
165
o   Ptests    [2021-04-08] FILTER directive reads the standard input and can be
              chained.
166
167
168
169
170
171
-   Eva       [2021-04-02] Improved automatic loop unroll (-eva-auto-loop-unroll
              option) of loops with goto or continue statements, or assigning
              constant values to loop variants.
-   Libc      [2021-03-31] In math.h specifications, new behaviors for cases
              creating NaN or infinite values. These behaviors are allowed or
              forbidden according to the -warn-special-float option.
Allan Blanchard's avatar
Allan Blanchard committed
172
173
-*  Kernel    [2021-03-26] Raise an error if trying to merge a tentative
              definition with a proper definition during linking
174
175
o   Ptests    [2021-03-25] Modify MODULE directive.
o   Ptests    [2021-03-24] Add new EXIT directive.
176
177
178
179
180
181
-   Eva       [2021-03-15] Slightly more precise evaluation of ACSL quantifiers.
o!  Eva       [2021-03-01] New signature for builtins, that are now registered
              via Eva.mli instead of Db.Value.
-   Eva       [2021-02-18] New "audit mode" to track file checksums, correctness
              options and enabled warnings, via options -audit-prepare and
              -audit-check.
182
-   Aorai     [2021-02-09] New option for tracking last N states of the
183
              automaton. Easier analysis of instrumented code with Eva.
Virgile Prevosto's avatar
Virgile Prevosto committed
184
185
o!  Kernel    [2021-02-08] Avoid triggering warning 16 (unerasable optional
              argument). Implies changing some labeled functions' signatures.
186
187
188
189
190
191
192
-   ACSL      [2021-02-04] New admit annotations to express hypotheses to be
              admitted but not verified by Frama-C.
-   Eva       [2021-01-28] Improved automatic widening thresholds (widen hints):
              use constant modulo as threshold, and infer thresholds globally
              for global variables.
-   Eva       [2021-01-21] Better interpretation of logical operators && and ||
              (useful when option -keep-logical-operators is enabled).
193
194
195
o!  Kernel    [2021-01-15] Make cfields list optional. None means undefined,
              empty struct allowed only in specific machdeps.
              removed cdefined field
196
-*  RTE       [2021-01-13] Remove spurious assert when comparing function
197
              pointer to NULL (fixes #@940)
198
199
-   Kernel    [2021-01-12] Set default machdep to x86_64 (was x86_32);
              allow setting machdep via environment variable FRAMAC_MACHDEP.
200
-   Kernel    [2021-01-08] Allow -add-symbolic-path to survive saves/loads and
Andre Maroneze's avatar
Andre Maroneze committed
201
              invert argument order (path:name).
202
203
-*  Eva       [2020-12-05] Fixes a crash when subdividing the evaluation of
              pointer expressions (via option -eva-subdivide-non-linear).
204
-   Libc      [2020-12-02] Remove obsolete attribute FRAMA_C_MODEL in the libc.
205
              Fixes #@877.
206
-*  Logic     [2020-11-30] The assigns clause can't mention const locations
207
              anymore. Fixes #@855.
Andre Maroneze's avatar
Andre Maroneze committed
208
o   Kernel    [2020-11-27] Extract builtin-related functions from module Cil
209
210
              to module Cil_builtins. Code can be updated using
              `bin/migration_scripts/titanium2vanadium.sh`.
211
212
-   Eva       [2020-11-26] Allow using Eva directives Frama_C_show_each and
              Frama_C_dump_each in ghost code.
213
-   Metrics   [2020-10-27] Add json output in addition to text and html.
214

215
216
217
218
###################################
Open Source Release 22.0 (Titanium)
###################################

219
-   MdR       [2020-10-19] Update Sarif output to 2.1.0 + prettier URI
220
-   Dev       [2020-10-20] Support for OCamlGraph 2.0.0
221
-   ACSL      [2020-10-16] Allows for axiomatic blocks-like extensions
222
223
224
-   Variadic  [2020-10-14] Don't print generated function name but print
              original name and a comment with the generated name so that the
              printed code is compilable.
225
226
-   Aorai     [2020-10-13] Ya automata can set auxiliary variables during a
              transition, and use such variables in subsequent guards.
Andre Maroneze's avatar
Andre Maroneze committed
227
228
-   Kernel    [2020-10-09] Add option -print-config-json, to output Frama-C
              configuration data in JSON format.
229
-   Logic     [2020-10-14] '\from' now accepts '&v' expressions
230
231
-   Metrics   [2020-10-01] Distinguish between undefined but specified functions
              and functions with neither definition nor specification.
232
233
-*  Eva       [2020-09-28] Improved string builtins on wide strings: crash fixed,
              better performance, misaligned pointers now considered invalid.
Julien Signoles's avatar
Julien Signoles committed
234
235
236
-   Kernel    [2020-09-22] New option -autocomplete p1, ..., pn that list the
              options of plug-ins p1, ..., pn in a format suitable for
              autocompletion scripts.
Julien Signoles's avatar
Julien Signoles committed
237
238
-   Kernel    [2020-09-21] Option -permissive now allows non-existent option
              names.
Allan Blanchard's avatar
Allan Blanchard committed
239
240
-   Logic     [2020-09-11] Introduce check-only annotations for
              requires, ensures, loop invariant and lemmas
Virgile Prevosto's avatar
Virgile Prevosto committed
241
242
-   Kernel    [2020-09-08] Add option -print-cpp-commands, to print the
              preprocessing commands used by Frama-C.
David Bühler's avatar
David Bühler committed
243
244
-   Eva       [2020-09-07] Deprecates legacy options aliases -val-* in favor
              of option names -eva-*.
Andre Maroneze's avatar
Andre Maroneze committed
245
-*  Slicing   [2020-09-07] Better handling of invalid command line options.
246
247
248
249
-   Eva       [2020-07-27] Improved automatic loop unroll (-eva-auto-loop-unroll
              option) on loops with several exit conditions, conditions using
              equality operators, temporary variables introduced by the Frama-C
              normalization or goto statements.
250
-!  Kernel    [2020-07-21] OCaml version greater than or equal to 4.08.1 required.
251
252
-   Eva       [2020-05-29] New builtins for trigonometric functions acos, asin
              and atan (and their single-precision version acosf, asinf, atanf).
253
-   Kernel    [2020-05-28] Support for C11's _Thread_local storage specifier
254
255
-   Kernel    [2020-05-26] New option -explain, which provides help messages
              for options used on the command line.
256
257
258
259
260
-   Eva       [2020-05-25] New annotation eva_allocate to configure the behavior
              of an allocation builtin for a call, overriding the global option.
-   Eva       [2020-05-25] New option -eva-alloc-builtin to configure uniformly
              the behavior of allocation builtins, instead of providing several
              builtins with different behaviors for malloc/calloc/realloc.
Andre Maroneze's avatar
Andre Maroneze committed
261
-   Eva       [2020-05-20] Supports the ACSL mathematical operator \abs
262
263
-   Kernel    [2020-05-18] Support for C11's _Noreturn function specifier

264
265
266
267
###################################
Open Source Release 21.1 (Scandium)
###################################

268
269
270
271
###################################
Open Source Release 21.0 (Scandium)
###################################

272
273
274
-*  Doc       [2020-05-07] Fixes internal refs in generated pdfs (fixes #2505)
-*  Kernel    [2020-05-04] Accept UCN-encoded unicode char in ACSL (fixes #@849)
o   Kernel    [2020-04-27] Plug-ins specific dirs now use Filepath instead of
275
              mere strings.
276
-   Eva       [2020-04-10] Fixes the Memexec cache on functions with logical
277
              annotations about variables unused in the C body of the function.
278
-   Eva       [2020-04-06] New option -eva-domains-function to enable domains
279
280
281
              only on given functions. Argument <d:f> enables the domain [d]
              on function [f], while <d:f+> also enables it on all functions
              called from [f]. <d:f-> disables [d] from function [f].
282
-   Eva       [2020-04-03] New experimental builtins for dynamic allocation
283
              Frama_C_*alloc_imprecise: faster convergence, but very imprecise.
284
-   Kernel    [2020-04-01] Report user errors when keys are not bound to a
285
286
              value for command-line options that require pairs of key:value
              as arguments. Such keys were silently ignored.
287
288
289
290
*!  Kernel    [2020-03-30] Reject labels at end of blocks.
-   RTE       [2020-03-30] Emits alarm on invalid pointers when option is on
-   Eva       [2020-03-30] Emits alarm on invalid pointers when option is on
-   Kernel    [2020-03-30] New option -warn-invalid-pointer (disabled by
291
292
              default) to warn on invalid pointer arithmetics resulting in a
              pointer that does not point to an object or one past an object.
293
294
295
-   RTE       [2020-03-27] Emits alarm on pointer downcast when option is on
-   Eva       [2020-03-27] Emits alarm on pointer downcast when option is on
-   Kernel    [2020-03-27] New option -warn-pointer-downcast (activated by
296
297
              default), to warn when a conversion between pointer and integer
              might provoke a loss of precision.
298
299
-   Kernel    [2020-03-20] Add option -cpp-extra-args-per-file
-*  Kernel    [2020-03-18] Fixes #@823 (-load-module/-load-script now accept
300
              spaces in filename)
301
302
303
-*  Kernel    [2020-03-18] Fixes #@818 (term generated for downcast alarms)
-   Eva       [2020-03-17] Supports the ACSL extended quantifiers \min and \max.
-   Eva       [2020-03-17] deprecate options -eva-*-domain in favor of
Andre Maroneze's avatar
Andre Maroneze committed
304
              -eva-domains
305
306
-   ACSL      [2020-03-04] Make conversion from C ptr to logic array explicit
-   Eva       [2020-03-03] Evaluates the logic predicate memchr_off, used in
David Bühler's avatar
David Bühler committed
307
              Frama-C libc specifications.
308
-   Eva       [2020-03-03] Slightly better heuristics for the subdivision of
David Bühler's avatar
David Bühler committed
309
              evaluations (option -eva-subdivide-non-linear).
310
-   Instantiate [2020-03-02] New plug-in Instantiate, to create function
311
312
313
              specializations for specific plug-ins and functions (e.g. malloc,
              memcpy, memset), to overcome limitations due to their
              specifications.
314
315
-   Kernel    [2020-02-25] support for ghost else blocks
-   Kernel    [2020-02-18] checks that ghost code does not modify the normal
Virgile Prevosto's avatar
Virgile Prevosto committed
316
              control flow of the non-ghost program
317
-*  Kernel    [2020-02-17] fixes issue that could prevent loading plug-ins on
Virgile Prevosto's avatar
Virgile Prevosto committed
318
              Windows installation
319
-   Kernel    [2020-02-14] -constfold now takes into account value
Virgile Prevosto's avatar
Virgile Prevosto committed
320
              of const globals
321
o   ACSL      [2020-02-13] Add possibility for ACSL extensions to alter the
Virgile Prevosto's avatar
Virgile Prevosto committed
322
323
              sequence of untyped terms they receive from the parser. Make also
              possible to customize the short pretty printer of extensions.
324
o   Kernel    [2020-02-13] Deprecated:
Virgile Prevosto's avatar
Virgile Prevosto committed
325
326
327
328
                           - Logic_typing.register_*_extension
                           - Cil_printer.register_*_extension
                           - Cil.register_behavior_extension
                           Use Acsl_extension.register_* instead
329
-   Eva       [2020-02-12] New option "-eva-domains <d1>,<d2>,..." to enable
330
331
              several domains at once. The list of available domains is given
              in the help message of the option.
332
o!  Eva       [2020-02-12] Simplifies abstract domain signature by removing the
333
              Transfer functor.
334
-*  Eva       [2020-02-12] Fixes the evaluation of logic predicates involving
335
              empty sets.
336
-   Eva       [2020-02-07] Supports the logic evaluation of quantifiers
337
              introducing mathematical variables (integer or real).
338
o!  Kernel    [2020-02-04] Removed FCBuffer, FCMap and FCSet. Use directly
339
              OCaml stdlib modules Buffer, Map and Set instead.
340
-   Eva       [2020-02-04] Renamed option -eva-malloc-functions into
341
              -eva-alloc-functions. Also contains calloc and realloc by default.
342
343
-*  GUI       [2020-01-24] Fix order of globals in the source panel.
-   Eva       [2020-01-23] Adds consistency checks on return and parameters
344
              types between a builtin and the replaced C function.
345
-   Eva       [2020-01-23] Subdivisions can now be enabled locally:
346
347
348
              - through the new option -eva-subdivide-non-linear-function that
                overrides the global option for the given functions;
              - via /*@ subdivide N; */ annotations on specific statements.
Julien Signoles's avatar
Julien Signoles committed
349

350
##################################
Andre Maroneze's avatar
Andre Maroneze committed
351
Open Source Release 20.0 (Calcium)
Andre Maroneze's avatar
Andre Maroneze committed
352
##################################
Andre Maroneze's avatar
Andre Maroneze committed
353

354
-   Eva       [2019-11-25] In the summary, fixes the number of alarms by
David Bühler's avatar
David Bühler committed
355
356
              category when the RTE plugin is used, and do not count logical
              properties in dead code as proven.
357
-!  Kernel    [2019-10-31] More stringent verifications on the use of ghost
Virgile Prevosto's avatar
Virgile Prevosto committed
358
              variable in non ghost-code. Fixes #2421
359
-   MdR       [2019-10-31] New plug-in Markdown-Report (MdR) for markdown and
360
              SARIF outputs
361
-   Eva       [2019-10-23] In the summary, fixes the total number of functions
David Bühler's avatar
David Bühler committed
362
              (and thus the computed analysis coverage).
363
-   Eva       [2019-10-23] New option -eva-auto-loop-unroll N to unroll all
364
              loops whose number of iterations can be easily bounded by <N>.
365
-   Eva       [2019-10-21] New octagon domain inferring relations of the form
366
367
368
369
370
              l ≤ ±X±Y ≤ e between pairs of integer variables X and Y. Enabled
              with option -eva-octagon-domain. Only infers relations between
              pairs of scalar variables occuring in a same instruction.
              Intra-procedural by default; octagons can be propagated through
              function calls with option -eva-octagon-through-calls.
371
372
-   ACSL      [2019-10-04] Support for ghost parameters
-   Eva       [2019-10-04] Evaluates ACSL predicates \is_plus_infinity and
373
              \is_minus_infinity.
374
375
376
-   Kernel    [2019-10-04] Supports macro INFINITY and NAN.
o   Config    [2019-09-27] ocp-indent 1.7.0 is now used for indentation
o   Eva       [2019-09-16] Dynamic registration of abstract values and domains:
377
              developers of new domains no longer need to modify Eva's engine.
378
379
-*  Kernel    [2019-09-13] Fixes Hptmap on keys with id greater than 2^28.
-*  Makefile  [2019-09-12] Fixes #2378 - bytecode only compilation (patch
380
              contributed by madroach) and use -thread where needed.
381
-*  Eva       [2019-08-21] Fixes the reduction by the negation of \initialized
382
              and \dangling predicates on imprecise lvalues.
383
-*  Kernel    [2019-08-20] Fixes a rare but critical bug which occured when
Julien Signoles's avatar
Julien Signoles committed
384
385
386
387
388
389
              Frama-C internally switched the current project in presence of >2
              projects and destroyed the old current project at about the same
              time: the Frama-C internal state became inconsistent and lead to
              unsound computations and crashes. It may be revealed to the
              end-user when using a long sequence of -then-replace (at least 3
              of them).
390
-*  Kernel    [2019-08-20] Fixed sequence of -removed-projects and -then
Julien Signoles's avatar
Julien Signoles committed
391
              options.
392
o   Ptests    [2019-08-05] Add new MODULE directive for compiling and loading
393
              an auxiliary OCaml module for a test
394
395
396
-   Kernel    [2019-08-05] Add -keep-unused-types normalization option
-   Libc      [2019-08-05] Remove obsolete (and forcing cpp error) builtins.h
o!  Kernel    [2019-08-02] Functions over visitor's behaviors have been moved
Julien Signoles's avatar
Julien Signoles committed
397
398
              from Cil into a new module Visitor_behavior. Apply the migration
              script potassium2calcium.sh to update your plug-ins automatically.
399
400
401
402
403
o!  Sparecode [2019-07-26] Removed from Db. Use proper Sparecode API instead.
-!  Kernel    [2019-07-24] OCaml version greater than or equal to 4.05.0 required.
-   Kernel    [2019-07-24] Improve placeholders handling in -cpp-command
o!  Kernel    [2019-07-23] Types in Properties are now records and not tuples
-   Eva       [2019-07-09] Supports ACSL floating-point comparison operators
404
              eq_float, le_float, eq_double, le_double, etc.
405
o!  Kernel    [2019-06-28] removes AST constructors TCoerce, TCoerceE,
Julien Signoles's avatar
Julien Signoles committed
406
              PLCoercion, PLCoercionE, Psubtype and PLsubtype
407
-*  Kernel    [2019-06-20] fixes dangling ref when removing unused static local
Virgile Prevosto's avatar
Virgile Prevosto committed
408

Virgile Prevosto's avatar
Virgile Prevosto committed
409
410
411
412
####################################
Open Source Release 19.0 (Potassium)
####################################

413
414
-*  RTE       [2019-05-24] fixes a crash when visiting variable declarations
-   Eva       [2019-04-19] The new annotation /*@ split exp; */ enumerates the
415
416
417
418
              possible values of an expression and continues the analysis
              for each of these value separately, until a /*@ merge exp; */
              is encountered. It is also possible to maintain this partitioning
              at all times with the option -eva-partition-value exp.
419
-   Eva       [2019-04-19] New option -eva-partition-history N to delay the join
420
421
422
423
              of abstract states for up to N merging points, thus keeping these
              states separate longer. Useful when a reasoning depends on the
              path taken to reach a control point, but can increase the analysis
              time exponentially in N.
424
-   Eva       [2019-04-19] Loop unroll annotations now accept non-constant but
425
              bounded expressions as the maximum number of unrollings to perform.
426
427
-*  Kernel    [2019-04-09] Avoid crashing on one-letter attributes. Fixes #2432
-*  Obfuscator [2019-04-09] Also obfuscate formals in function pointer types.
428
              Fixes #2433.
429
-   Eva       [2019-04-05] Prints an analysis summary at the end, outlining the
430
431
              analysis coverage and the number of errors, warnings and emitted
              alarms. It can be disabled with the option -eva-msg-key=-summary
432
-   Eva       [2019-04-03] New option -eva-precision to globally configure the
433
434
435
              analysis from 0 (fast but imprecise) to 11 (accurate but slow).
              A precision of 5 is often a reasonable trade-off. This meta-option
              automatically sets up other options that can also be overriden.
436
437
-   Inout     [2019-04-01] Fix performance issue when initializing large arrays.
-   ACSL      [2019-03-08] Add check annotation, similar to assert except that
Virgile Prevosto's avatar
Virgile Prevosto committed
438
              it does not introduce additional hypotheses on the program state
439
-*  Makefile  [2019-03-07] Do not attempt to install .cmx on bytecode-only
Virgile Prevosto's avatar
Virgile Prevosto committed
440
              architectures. Patch by M. Dogguy backported from Debian package
441
-   Libc      [2019-03-05] Better specs and removal of half-implemented ifdef
442
              that tried to take various POSIX versions into account
443
-*  Kernel    [2019-03-05] Better detection of invalid goto in presence of VLA
Virgile Prevosto's avatar
Virgile Prevosto committed
444
              (fixes #@499)
445
-   GUI       [2019-03-04] Compatibility with lablgtk3 and improved handling of
446
              some widgets
447
-   ACSL      [2019-03-01] Clarifies which C variables are in scope under a
448
              \at(·,L) (#@575)
449
-   Libc      [2019-02-26] Ask clang not to warn about unknown FRAMA_C_MODEL
450
              attribute when pre-processing frama-c's libc
451
452
453
454
-*  Obfuscator [2019-02-26] Obfuscate logic types and logic constructors.
-*  Inout     [2019-02-21] Fixes operational input on const local initialization
o   RTE       [2019-02-21] RTE has a static API
o   Kernel    [2019-02-18] When registering extended ACSL annotations, one
455
              must now indicate whether they should have a status.
456
457
o   Kernel    [2019-02-05] Integer API moving closer to Zarith
-   Eva       [2019-01-19] New warning category for detecting loops without
458
              'unroll' directive
459
460
-   Eva       [2019-01-31] Ignore annotations with "no_eva" tag
-*  ACSL      [2019-01-19] Accept C identifiers that happen to be ACSL keywords
461
              in volatile and reads clauses
462
-   Eva       [2019-01-10] Improved precision on nested loops (by postponing
David Bühler's avatar
David Bühler committed
463
              the widening on inner loops according to -eva-widening-period).
464
-*  Aorai     [2019-01-04] Fixes #@586: avoid removing the initial state
465
              of the automaton
466
-   Kernel    [2019-01-03] Add attributes for loop statements to allow
Virgile Prevosto's avatar
Virgile Prevosto committed
467
              distinguishing between for, while and dowhile loops.
468
-!  Kernel    [2019-01-03] Add statement attributes (sattr) to the AST. They
Virgile Prevosto's avatar
Virgile Prevosto committed
469
              are not printed by default, use -kernel-msg-key printer:attrs
470
-!  Kernel    [2019-01-03] Improved precision of integer abstract bitwise
Valentin Perrelle's avatar
Valentin Perrelle committed
471
              operators.
472
-*  Eva       [2018-12-17] Fixes -eva-split-return on uninitialized or escaping
473
              function returns when -eva-warn-copy-indeterminate is disabled.
474
475
476
o   Kernel    [2018-12-11] New functions for retrieving major and minor version
-*  Kernel    [2018-12-04] Fixes AST integrity check wrt volatile accesses
-*  Kernel    [2018-11-21] Fixes #@553 - pretty-printing of basic asm template
477

478
479
480
481
################################
Open Source Release 18.0 (Argon)
################################

482
-!  Kernel    [2018-10-24] Log.error and Log.failure will eventually make
483
              Frama-C exit with a non-zero status. Fixes #@552
484
-   Kernel    [2018-10-24] More ergonomic command-line options for governing
485
              warning categories statuses.
486
-   Eva       [2018-10-24] Enable the memexec cache by default. It can be
487
              disabled by option -eva-no-memexec.
488
-   Eva       [2018-10-22] Improved performances when the symbolic locations
489
              domain and the memexec cache are enabled.
490
-   Eva       [2018-10-22] The memexec cache is now fully compatible with all
491
492
              abstract domains provided by Eva. However, the binding to the
              Apron domains disable memexec.
493
-   Eva       [2018-10-18] New experimental domain "numerors" inferring absolute
494
495
              and relative errors of floating-point computations. Enabled by the
              option -eva-numerors-domain. Does not handle loops for now.
496
-*  Kernel    [2018-10-18] Fixes parsing of compound initializers with anonymous
497
              fields. Fixes #2384
498
-*  Kernel    [2018-10-16] Consider that asm can change content of pointers
499
              used as inputs when generating assigns clauses. Fixes #@458
500
501
-   Eva       [2018-10-12] Remove option -obviously-terminates.
-   Kernel    [2018-10-05] New option -warn-invalid-bool, to warn when reading
502
              trap representations of type _Bool.
503
504
-   Eva       [2018-10-04] ACSL predicates with a "no_eva" tag are now ignored.
-   Eva       [2018-10-03] Warn about currently unsupported specifications
505
              of some libc functions.
506
507
508
509
-   Eva       [2018-10-02] Fix the gauges domain on weak bases.
-   Eva       [2018-10-02] Some fixes and improvements of the equality domain.
-*  Kernel    [2018-10-02] Rejects sizeof of an incomplete type. Fixes #@560.
-*  Kernel    [2018-09-26] Add attribute to allow writing into const lvals in
510
511
              specific (aka C++ constructors and mutable fields) circumstances.
              Fixes #2395.
512
-   Kernel    [2018-09-14] New warning (disabled by default) when multiple side
513
514
              effects are unsequenced (CERT-EXP10-C recommandation).
              Fixes #@492
515
-   Eva       [2018-09-13] Remove option -val-warn-left-shift-negative, and
516
              comply with kernel option -warn-[left|right]-shift-negative.
517
-   Kernel    [2018-09-13] New options -warn-left-shift-negative (enabled by
518
519
              default) and -warn-right-shift-negative (disabled by default),
              to control the emission of alarms on shifts on negative integers.
520
o!  Constant Propagation [2018-09-12] Removing Db API for Constant Propagation
521
522
              plug-in. Calls to !Db.Constant_Propagation should be replaced by
              calls to Constant_Propagation.Api.
523
-   Eva       [2018-09-12] Reduction of values leading to division by zero
524
              alarms, when possible.
525
-   Eva       [2018-09-11] Better reduction of floating-point values cast into
526
              integer types when an alarm is emitted.
527
-   Metrics   [2018-09-06] Add option -metrics-used-files, to help identify
528
              unnecessary files given in the command line
529
530
531
-   RTE       [2018-09-05] Remove option -rte-precond.
-   Eva       [2018-08-31] Supports the ACSL functions \min and \max.
-   Eva       [2018-08-30] Fixes the alarms on subtractions and comparisons of
532
              pointers on weak bases (created by allocations in loops).
533
-!  ACSL      [2018-08-28] Introduce extensions to global annotations and
534
535
              better characterization of each extension kind.
              See development guide for more information
536
-   Eva       [2018-08-28] All options of Eva start with -eva. Aliases to
537
              previous option names preserve backward compatibility.
538
-!  Eva       [2018-08-28] Rename plug-in shortname from 'value' to 'eva'. Eva
539
540
              is now properly named Eva in all logs, in the GUI, and as the
              emitter of the alarms.
541
-!  Kernel    [2018-08-23] Introduce Filepath dataype for more consistent
542
              normalization of filenames
543
-*  Kernel    [2018-08-23] Do not allow compound assignments to const variables
544
              Fixes #@384
545
-!  Kernel    [2018-08-23] Remove option -const-writable: const globals are
546
              unconditionally constants
547
-*  Eva       [2018-08-02] Deprecate option -val-warn-builtin-override in favor
548
              of warning category builtins:override.
549
-   Kernel    [2018-07-26] Fix compilation on OpenBSD
550
              patch contributed by madroach. Fixes #2379
551
-   Kernel    [2018-07-26] New option -remove-inlined to remove function(s)
552
553
              after -inline-calls, add category @inline to refer to all
              functions with inline attribute (for both options).
554
-   Eva       [2018-07-23] The debug category "garbled-mix" becomes a warning
555
              category. Better track of garbled mix created by specification.
556
-*  ACSL      [2018-07-23] Avoid removing cast of void ptr used as
557
              argument of function expecting a ptr with known size. Fixes #@432
558
o!  Kernel    [2018-07-23] Remove completely outdated module Dataflow.
559
              Deprecated since 3+ years. Use Dataflow2 instead.
560
-*  RTE       [2018-07-23] Stop generating spurious \initialized alarms.
Allan Blanchard's avatar
Allan Blanchard committed
561
              Fixes #@429
562
-*  Kernel    [2018-07-06] Respect relative order of labels and ACSL annots.
563
              Fixes #@524
564
565
o*  Ptests    [2018-07-02] Do not keep oracles for empty stderr. Fixes #@402
-*! ACSL      [2018-07-02] introduce ACSL operators \le_double, \ge_double, ...
566
567
              in addition to \le_float, \ge_float, ... Remove overloading of
              \le_float that made it accept double as arguments. Fixes #@502
568
-  Eva        [2018-06-28] New option -eva-report-red-statuses listing in
569
570
              a csv file the properties invalid for some states of the analysis
              (as in the "Red Alarms" panel of the GUI).
571
-  Eva        [2018-06-25] Release all builtins, including memset and memcpy,
572
              as open-source.
573
-  Eva        [2018-06-15] When a cvalue builtin is used, other domains use the
574
575
              frama-c libc specification to interpret the call without losing
              too much information.
576
-  Eva        [2018-06-14] The variables from the frama-c libc are no longer
577
              shown in the initial state print.
578
-  Eva        [2018-06-11] Improved precision of string builtins for strlen,
579
              strchr and memchr.
580
-  Eva        [2018-04-25] Renamed option -wlevel into -eva-widening-delay. New
581
582
              option -eva-widening-period to control the number of iterations
              between two widenings.
583
-  Eva        [2018-04-25] New propagation strategy that allows unrolling loops
584
585
586
587
588
              even when the slevel has been exceeded. Unroll the N first loop
              iterations via the global option -eva-min-loop-unrolling N or via
              specific code annotations /*@ loop unroll N; */. The new strategy
              may affect analyses even without loop unrolling.

589
590
591
############################################
Open Source Release 17.1 (Chlorine-20180502)
############################################
592

593
-  Libc       [2018-07-05] Fix C++ compatibility for Frama-Clang plug-in
594

595
596
597
############################################
Open Source Release 17.0 (Chlorine-20180501)
############################################
598

599
-  Eva        [2018-04-25] Added scripts and templates to help automate case
600
              studies (in $FRAMAC_SHARE/analysis-scripts)
601
-* Typing     [2018-04-23] Stronger checks w.r.t. implicit conversions in
602
603
              function pointers (must have compatible types) and assignments
              (modifiable lvalues). Fixes #@479
604
605
-  Kernel     [2018-04-23] Added option -inline-calls for syntactic inlining
-* Kernel     [2018-04-19] Avoid crash when re-declaring a function with
606
              formals after it has been called without any. Fixes #@454
607
-  Kernel     [2018-04-13] Deprecate option -warn-decimal-float in favor of
608
              warning category parser:decimal-float
609
-  Kernel     [2018-04-13] More possible statuses for warning categories.
610
              Fixes #@486
611
o  Kernel     [2018-04-13] Change Cil.typeHasAttributeDeep into
612
              Cil.typeHasAttributeMemoryBlock. Fixes #@489
613
o* Logic      [2018-04-11] properly reset logic environment in case of typing
614
              errors. Fixes #@326
615
616
-  Eva        [2018-04-10] Interpret the logic constants \pi and \e.
-  Eva        [2018-04-06] Initialization of volatile pointers now keeps the
617
              base addresses of the pointer (with arbitrary offsets).
618
-  Eva        [2018-04-06] Fix the initialization of local volatile variables,
619
              which can always have any value.
620
-  Eva        [2018-04-06] In the logic, interpret the ACSL function \sign and
621
              the constructors \Positive and \Negative.
622
-  Metrics    [2018-04-05] When the value coverage is computed, also shows the
623
              total number of statements by function in the filetree of the Gui.
624
-  Gui        [2018-04-04] Added Preferences menu (shortcut: Ctrl+P) to set
625
              themes for property bullets and external source editor
626
627
o  Lib        [2018-03-30] New Rich_text module to create message with tags
o! Kernel     [2018-03-30] Never or rarely used Log functions have been
628
              removed or deprecated
629
-  Eva        [2018-03-15] Avoid enumeration on values with too many bases —
630
              fixes a performance issue.
631
-  Gui        [2018-03-07] The preconditions of a function call can now be
632
633
              displayed before the call statement itself (click on status
              bullets with '+' or '-' to unfold/fold them)
634
635
-  Typing     [2018-03-02] Support for CERT EXP46-C
-  Eva        [2018-03-01] Fix a soundness bug in the equality domain: do not
636
637
              infer incorrect equalities between incomparable pointers,
              or between -0. and +0.
638
-  Eva        [2018-02-26] deprecate option -val-warn-on-alarms in favor of
639
              warning category alarm
640
-  Kernel     [2018-02-26] deprecate option -continue-annot-error in favor of
641
              warning category annot-error
642
-! Kernel     [2018-02-26] introduce warning categories, with various
643
              possible behaviors. Refactor management of debug categories
644
-* RTE        [2018-02-23] Do not emit spurious 'idx < 0' assert
645
              on gcc-style FAM. Fixes #@393
646
647
-* Kernel     [2018-02-23] Handle anonymous struct/union init. Fixes #@376
-  Eva        [2018-02-22] Equalities can be propagated through function calls.
648
649
              New options -eva-equality-through-calls[-function] to decide
              (globally or by function) which ones are kept from the caller.
650
-  Eva        [2018-02-21] When an lvalue lv is assigned or leaves the scope,
651
652
              the equality domain tries to replace lv by an equal term (if any)
              in the expressions depending on lv (instead of removing them).
653
o! Occurrence [2018-02-20] Removing Db API for Occurrence plug-in. Calls to
654
              !Db.Occurrence should be replaced by calls to Occurrence.Register.
655
o! Impact     [2018-02-20] Removing Db API for Impact plug-in. Calls to
656
              !Db.Impact should be replaced by calls to Impact.Register.
657
o! Users      [2018-02-20] Removing Db API for Users plug-in. Calls to
658
              !Db.Users should be replaced by calls to Users.Users_register.
659
-  Eva        [2018-02-13] Removed *_alloced_return base created for functions
660
661
              without body that return pointers. Such bases were imprecise
              and could be unsound in corner cases.
662
-  Eva        [2018-02-08] Shifts of addresses now create garbled mixes (as any
663
              other arithmetic operation).
664
665
-  Logic      [2018-02-07] Ghost code now supports /@ ... @/ annotations
-  Eva        [2018-02-06] By default, do not emit pointer_comparable alarms for
666
667
              non pointer operations. Always compute {0;1} for non pointer
              comparisons involving incomparable addresses.
668
669
-  Eva        [2018-02-01] Warn about unsupported allocates clauses.
-  Eva        [2018-01-30] The subdivision of evaluations (through the option
670
671
              -val-subdivide-non-linear) can subdivide the values of several
              lvalues simultaneously (on expressions such as x*x - 2*x*y + y*y).
672
-  Kernel     [2018-01-24] Better renaming of variables in case of name
673
              collision.
674
o! Kernel     [2018-01-24] Keep information about syntactic scope of local
675
676
              static variables. Accessed through
              Globals.Syntactic_search.find_in_scope.
677
-! Eva        [2018-01-24] Renamed option -val-malloc-returns-null to
678
              -val-alloc-returns-null, which also applies to realloc builtins.
679
-  Kernel     [2018-01-16] Added option -json-compilation-database to help with
680
              preprocessing. Requires yojson during Frama-C compilation.
681
-  Eva        [2018-01-15] New function post_analysis in abstract domains,
682
              called at the end of the analysis.
683
-  Eva        [2018-01-11] The Simple_memory functor lets builtins interpret C
684
              functions from the value of arguments to the result value.
685
-  Eva        [2018-01-11] Evaluate the preconditions of the functions for which
686
              a builtin is used; builtins do not emit alarms anymore.
687
-! Kernel     [2018-01-11] Alarms Logic_memory_access and Valid_string, that
688
              were only emitted by Eva builtins, are removed.
689
-* ACSL       [2017-12-14] Reinforce rejection of void* pointer types in the
690
691
              arguments of ACSL built-in constructs related to memory blocks
              and pointer dereferencing.
692
-* ACSL       [2017-12-14] Reinforce rejection of implicit casts from array
693
694
              types to pointer types in the arguments of ACSL built-in
              constructs related to memory blocks and pointer dereferencing.
695
-* Kernel     [2017-12-13] Clean up typechecking environment when dropping
696
              side-effects (in sizeof et al.). Fixes #@430
697
o! Kernel     [2017-12-13] Old Cil.isCharType renamed as Cil.isAnyCharType.
698
699
              New Cil.isCharType is now only true for plain char, neither signed
              nor unsigned. Derived functions (isCharPtr et al.) also updated
700
701
-  Eva        [2017-12-12] Fix a crash when using -val-stop-at-nth-alarm.
-  Eva        [2017-12-07] Eva complies with option -warn-special-float, and
702
              propagates or warns on NaN and infinite values accordingly.
703
-! Kernel     [2017-12-07] Option -warn-not-finite-float renamed into
704
              -warn-special-float and extended (accepts non-finite/nan/none).
705
-  Kernel     [2017-12-07] Make some typechecking warnings controllable with
706
              -kernel-msg-key keys.
707
-  Eva        [2017-12-07] New option -val-skip-stdlib-specs, set by default.
708
709
              When analyzing the body of a function from Frama-C's standard
              library, specifications will be skipped.
710
-  Eva        [2017-11-28] New builtins for the single-precision mathematical
711
              functions fmodf, cosf, sinf and atan2f.
712
-! Eva        [2017-11-16] In the log, messages on preconditions are now
713
              reported with the location of the call site.
714
o! Eva        [2017-11-09] The Fval module now supports NaN and infinite values.
715
716
              Major API changes in Fval, Ival and Cvalue.V (regarding casts,
              mostly)
717
718
-o Eva        [2017-11-09] Option -all-rounding-modes has been removed
-* Eva        [2017-11-09] Fix bugs in builtins for cos and sin. The results
719
              may be less precise than previously
720
-  Eva        [2017-11-09] Various improvements in the handling of
721
722
              floating-point variables: evaluation of \is_finite, computation
              of the bits of a floating-point range, etc
723
-  Eva        [2017-11-09] New panel "Red alarms" in the GUI that shows all red
724
725
              statuses emitted for some states during the analysis. They are not
              completely invalid, but should often be investigated first.
726
-* Eva        [2017-10-27] Fix bug in the handling of non-explicitly volatile
727
728
              fields inside volatile structs or unions

729
730
731
##########################################
Open Source Release 16.0 (Sulfur-20171101)
##########################################
732

733
-* Eva        [2017-10-27] Fix bugs when evaluating \ìnitialized, \dangling
734
              and \separated on addresses of bitfields
735
-* Eva        [2017-10-27] Fix bug in the handling of non-explicitly volatile
736
              fields inside volatile structs or unions
737
-  RTE        [2017-10-27] add option -rte-initialized to generate assertions
738
              over read accesses to potentially uninitialized locations.
739
-* RTE        [2017-10-16] Fix bounds of alarms emitted when downcasting to
740
              bitfields (issue #?2314)
741
742
o  Makefile   [2017-10-13] add gui-byte target to only build bytecode GUI
o  Kernel     [2017-10-11] sizeof() and alignof() applied to a function can now
743
744
              be rejected when the compiler does not support this construct,
              depending on the fields sizeof_fun and alignof_fun of the machdep
745
-* Kernel     [2017-10-11] More thorough checks on l-values with function type.
746
              Non-sensical expressions are now rejected at parsing type.
747
-  Eva        [2017-10-10] Uses assigns clauses to over-approximate the effects
748
              of assembly statements. Warns if no assigns clause is provided.
749
-* Eva        [2017-10-10] Fixes a performance issue in offsetmaps, that occured
750
              when reading or copying values smaller than cells in large arrays.
751
-  Eva        [2017-10-10] The backward propagation tries to reduce integer
752
              values by considering separately the bounds of their intervals.
753
-* Eva        [2017-10-10] Fixes an optimization issue where the reduction by a
754
              loop invariant just after widenings could impede the convergence.
755
-* Eva        [2017-10-10] Fixes a soundness bug where a loop invariant could be
756
              wrongly proved correct in some marginal cases.
757
758
+  Slicing    [2017-10-05] File slicing_types/*.ml moved into slicing subdir.
-  Gui        [2017-09-13] In the filetree, the filter menu appears on a right
759
              click on the header, while a left click sorts the tree.
760
-  Metrics    [2017-09-13] In the Gui, shows the percentage and the number of
761
              dead statements (when computed) for each function of the filetree.
762
-! Callgraph  [2017-09-01] Option -cg-init-roots replaced by -cg-service-roots
763
764
              (almost equivalent); new options -cg-function-pointers (ignore
              function pointers; unsound) and -cg-roots (compute subgraphs).
765
o! Eva        [2017-09-01] In abstract domains, compute_using_specification is
766
767
768
              replaced by logic_assign, that interprets one \assigns clause.
              Complete specification are now interpreted through successive
              calls to evaluate_predicate, reduce_by_predicate and logic_assign.
769
-  Eva        [2017-09-01] Various precision improvements in the interpretation
770
              of the behaviors of a specification.
771
-* Kernel     [2017-08-31] Fixes configure script on bytecode only architecture.
772
              Initial version of the patch by Debian. Fixes #2325
773
-* Kernel     [2017-08-31] Fix various typos in source code and user messages.
774
              Patch by Debian. Fixes #2323
775
-! Sparecode  [2017-08-31] Rename option -rm-unused-globals to
776
              -sparecode-rm-unused-globals.
777
778
o! ACSL       [2017-08-24] Refactor handling of logic labels in AST
-! Eva        [2017-08-03] Fix soundness (resp. precision) bug on big-endian
779
780
              (resp. little-endian) architectures. This bug triggered on
              low-level code, typically when using bitfields
781
-* Kernel     [2017-08-03] Strip bitfield attribute when performing integral
782
783
              promotions on bitfields of size short or char. Fixes incorrect
              attributes on the resulting expression.
784
-! ACSL       [2017-08-03] Explicitely disallow /* and */ in ACSL annotations.
785
786
787
788
789
              Allows to re-use logic parser for parsing annotations in external
              files that can use /* ... */ as comments. As a consequence,
              expressions like y/*p are thus rejected, but this was already the
              case when -pp-annot is activated (default for .c files) and can
              be fixed easily in y / *p (as it is pretty-printed)
790
-* Kernel     [2017-07-29] Fix unmarshalling of save files that contain more
791
              than 4Gb of uncompressed data. Patch from TIS-interpreter.
792
793
-* Eva        [2017-07-27] Fix performance issue with the equality domain.
-! Kernel     [2017-08-28] Fix invalid eids on code generated through loop
794
              unrolling
795
-! Slicing    [2017-08-28] Fix invalid eids on code generated through option
796
              -slicing-level >= 2
797
-! Eva        [2017-07-28] Fixed memory leak with option
798
              -val-subdivide-non-linear
799
o! Slicing    [2017-08-01] Removing Db API for Slicing plug-in. Calls to
800
              !Db.Slicing should be replaced by calls to Slicing.Api.
801
-o! Slicing   [2017-07-27] Removing deprecated '-slice-option' and related
802
803
              !Db.Slicing.Projet.print_exported_project. Minor changes into
	      !Db.Slicing.Projet.extract.
804
o! Scope      [2017-07-27] Removing Db API for Scope plug-in. Calls to
805
              !Db.Scope should be replaced by calls to Scope.
806
o! Report     [2017-07-24] Removing Db API for Report plug-in. Calls to
807
808
              !Db.Report.print should be replaced by calls to
              Report.Register.print.
809
-  RTE        [2017-07-17] Emits overflow alarms on unsigned left shift when
810
              -warn-unsigned-overflow is enabled.
811
-  Eva        [2017-07-17] Emits overflow alarms on unsigned left shift when
812
              -warn-unsigned-overflow is enabled.
813
-  Kernel     [2017-07-10] Composite types are now required to have equal tags
814
              as per the C standard; no more support for isomorphic structs.
815
-  Eva        [2017-07-01] In the GUI, the "Values" panel displays the values
816
              computed by using the properties inferred by all enabled domains.
817
-! Eva        [2017-06-30] Better handling of function alloca(), via builtin
818
              Frama_C_alloca.
819
-* Eva        [2017-06-28] The cvalue states saved after each statement are now
820
              properly deleted when an Eva parameter is changed in the GUI.
821
o  Eva        [2017-06-26] New functor in domains/simple_memory.ml to build a
822
823
              complete domain from a value abstraction. The abstract states link
              each scalar variable of a program to an abstract value.
824
825
-  Eva        [2017-06-26] New sign domain for demonstration purposes only.
-* Kernel     [2017-06-09] Parser now handle mixed concatenation of
826
              string and wstring. Fixes #@1467
827
-  Eva        [2017-06-07] The subdivision of the evaluation of non-linear
828
829
              expressions (through the -val-subdivide-non-linear option) also
              applies to the new evaluations requested by the equality domain.
830
-* Eva        [2017-06-14] Fix a crash when downcasting pointer values with
831
              the option -val-warn-signed-converted-downcast enabled.
832
833
-* Eva        [2017-06-14] Fix missing alarms when downcasting pointer values.
-o Eva        [2017-05-24] The argument ~with_alarms for functions of Db.Value
834
              is now optional, and will be removed in a later version.
835
*  Eva        [2017-05-24] Fix soundness bug in string builtins where some
836
              invalid offsets did not generate alarms.
837
-  Eva        [2017-05-22] Removes all effects of the special functions
838
839
              Frama_C_[dump|show]_each on the analyses: no alarms are emitted
              and the states are never reduced on these calls.
840
-  Eva        [2017-05-22] Frama_C_dump_each prints the state of each available
841
              domain whose log category is enabled.
842
-  Eva        [2017-05-22] New directive Frama_C_domain_show_each prints the
843
844
              internal properties about the arguments inferred by each available
              domain whose log category is enabled.
845
o! Eva        [2017-05-22] Abstract domains have to provide a log category and
846
847
              a function show_expr that prints the internal properties inferred
              about an expression.
848
849
-  Kernel     [2017-05-18] Added option -print-return to inline gotos to return
-  RTE        [2017-05-12] add -warn-not-finite-float for checking
850
              that infinite and NaN floats are not produced.
851
-! Kernel     [2017-05-17] qualifiers are dropped from the return type of