Changelog 246 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
###############################################################################
# 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.    #
# '#nnn'   : BTS entry #nnn                                                   #
# '#!nnn'  : BTS private entry #nnn                                           #
# '#@nnn'  : Gitlab frama-c/frama-c issue                                     #
# For compatibility with old change log formats:                              #
# '#?nnn'  : OLD-BTS entry #nnn                                               #
###############################################################################

Andre Maroneze's avatar
Andre Maroneze committed
16
##################################
Andre Maroneze's avatar
Andre Maroneze committed
17
Open Source Release 21.1 (Scandium)
Andre Maroneze's avatar
Andre Maroneze committed
18
19
##################################

20
21
22
23
###################################
Open Source Release 21.0 (Scandium)
###################################

24
25
26
27
-*  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
o   Kernel    [2020-04-27] Plug-ins specific dirs now use Filepath instead of
28
              mere strings.
29
-   Eva       [2020-04-10] Fixes the Memexec cache on functions with logical
30
              annotations about variables unused in the C body of the function.
31
-   Eva       [2020-04-06] New option -eva-domains-function to enable domains
32
33
34
              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].
35
-   Eva       [2020-04-03] New experimental builtins for dynamic allocation
36
              Frama_C_*alloc_imprecise: faster convergence, but very imprecise.
37
-   Kernel    [2020-04-01] Report user errors when keys are not bound to a
38
39
              value for command-line options that require pairs of key:value
              as arguments. Such keys were silently ignored.
40
41
42
43
*!  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
44
45
              default) to warn on invalid pointer arithmetics resulting in a
              pointer that does not point to an object or one past an object.
46
47
48
-   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
49
50
              default), to warn when a conversion between pointer and integer
              might provoke a loss of precision.
51
52
-   Kernel    [2020-03-20] Add option -cpp-extra-args-per-file
-*  Kernel    [2020-03-18] Fixes #@823 (-load-module/-load-script now accept
53
              spaces in filename)
54
55
56
-*  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
57
              -eva-domains
58
59
-   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
60
              Frama-C libc specifications.
61
-   Eva       [2020-03-03] Slightly better heuristics for the subdivision of
David Bühler's avatar
David Bühler committed
62
              evaluations (option -eva-subdivide-non-linear).
63
-   Instantiate [2020-03-02] New plug-in Instantiate, to create function
64
65
66
              specializations for specific plug-ins and functions (e.g. malloc,
              memcpy, memset), to overcome limitations due to their
              specifications.
67
68
-   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
69
              control flow of the non-ghost program
70
-*  Kernel    [2020-02-17] fixes issue that could prevent loading plug-ins on
Virgile Prevosto's avatar
Virgile Prevosto committed
71
              Windows installation
72
-   Kernel    [2020-02-14] -constfold now takes into account value
Virgile Prevosto's avatar
Virgile Prevosto committed
73
              of const globals
74
o   ACSL      [2020-02-13] Add possibility for ACSL extensions to alter the
Virgile Prevosto's avatar
Virgile Prevosto committed
75
76
              sequence of untyped terms they receive from the parser. Make also
              possible to customize the short pretty printer of extensions.
77
o   Kernel    [2020-02-13] Deprecated:
Virgile Prevosto's avatar
Virgile Prevosto committed
78
79
80
81
                           - Logic_typing.register_*_extension
                           - Cil_printer.register_*_extension
                           - Cil.register_behavior_extension
                           Use Acsl_extension.register_* instead
82
-   Eva       [2020-02-12] New option "-eva-domains <d1>,<d2>,..." to enable
83
84
              several domains at once. The list of available domains is given
              in the help message of the option.
85
o!  Eva       [2020-02-12] Simplifies abstract domain signature by removing the
86
              Transfer functor.
87
-*  Eva       [2020-02-12] Fixes the evaluation of logic predicates involving
88
              empty sets.
89
-   Eva       [2020-02-07] Supports the logic evaluation of quantifiers
90
              introducing mathematical variables (integer or real).
91
o!  Kernel    [2020-02-04] Removed FCBuffer, FCMap and FCSet. Use directly
92
              OCaml stdlib modules Buffer, Map and Set instead.
93
-   Eva       [2020-02-04] Renamed option -eva-malloc-functions into
94
              -eva-alloc-functions. Also contains calloc and realloc by default.
95
96
-*  GUI       [2020-01-24] Fix order of globals in the source panel.
-   Eva       [2020-01-23] Adds consistency checks on return and parameters
97
              types between a builtin and the replaced C function.
98
-   Eva       [2020-01-23] Subdivisions can now be enabled locally:
99
100
101
              - 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
102

103
##################################
Andre Maroneze's avatar
Andre Maroneze committed
104
Open Source Release 20.0 (Calcium)
Andre Maroneze's avatar
Andre Maroneze committed
105
##################################
Andre Maroneze's avatar
Andre Maroneze committed
106

107
-   Eva       [2019-11-25] In the summary, fixes the number of alarms by
David Bühler's avatar
David Bühler committed
108
109
              category when the RTE plugin is used, and do not count logical
              properties in dead code as proven.
110
-!  Kernel    [2019-10-31] More stringent verifications on the use of ghost
Virgile Prevosto's avatar
Virgile Prevosto committed
111
              variable in non ghost-code. Fixes #2421
112
-   MdR       [2019-10-31] New plug-in Markdown-Report (MdR) for markdown and
113
              SARIF outputs
114
-   Eva       [2019-10-23] In the summary, fixes the total number of functions
David Bühler's avatar
David Bühler committed
115
              (and thus the computed analysis coverage).
116
-   Eva       [2019-10-23] New option -eva-auto-loop-unroll N to unroll all
117
              loops whose number of iterations can be easily bounded by <N>.
118
-   Eva       [2019-10-21] New octagon domain inferring relations of the form
119
120
121
122
123
              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.
124
125
-   ACSL      [2019-10-04] Support for ghost parameters
-   Eva       [2019-10-04] Evaluates ACSL predicates \is_plus_infinity and
126
              \is_minus_infinity.
127
128
129
-   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:
130
              developers of new domains no longer need to modify Eva's engine.
131
132
-*  Kernel    [2019-09-13] Fixes Hptmap on keys with id greater than 2^28.
-*  Makefile  [2019-09-12] Fixes #2378 - bytecode only compilation (patch
133
              contributed by madroach) and use -thread where needed.
134
-*  Eva       [2019-08-21] Fixes the reduction by the negation of \initialized
135
              and \dangling predicates on imprecise lvalues.
136
-*  Kernel    [2019-08-20] Fixes a rare but critical bug which occured when
Julien Signoles's avatar
Julien Signoles committed
137
138
139
140
141
142
              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).
143
-*  Kernel    [2019-08-20] Fixed sequence of -removed-projects and -then
Julien Signoles's avatar
Julien Signoles committed
144
              options.
145
o   Ptests    [2019-08-05] Add new MODULE directive for compiling and loading
146
              an auxiliary OCaml module for a test
147
148
149
-   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
150
151
              from Cil into a new module Visitor_behavior. Apply the migration
              script potassium2calcium.sh to update your plug-ins automatically.
152
153
154
155
156
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
157
              eq_float, le_float, eq_double, le_double, etc.
158
o!  Kernel    [2019-06-28] removes AST constructors TCoerce, TCoerceE,
Julien Signoles's avatar
Julien Signoles committed
159
              PLCoercion, PLCoercionE, Psubtype and PLsubtype
160
-*  Kernel    [2019-06-20] fixes dangling ref when removing unused static local
Virgile Prevosto's avatar
Virgile Prevosto committed
161

Virgile Prevosto's avatar
Virgile Prevosto committed
162
163
164
165
####################################
Open Source Release 19.0 (Potassium)
####################################

166
167
-*  RTE       [2019-05-24] fixes a crash when visiting variable declarations
-   Eva       [2019-04-19] The new annotation /*@ split exp; */ enumerates the
168
169
170
171
              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.
172
-   Eva       [2019-04-19] New option -eva-partition-history N to delay the join
173
174
175
176
              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.
177
-   Eva       [2019-04-19] Loop unroll annotations now accept non-constant but
178
              bounded expressions as the maximum number of unrollings to perform.
179
180
-*  Kernel    [2019-04-09] Avoid crashing on one-letter attributes. Fixes #2432
-*  Obfuscator [2019-04-09] Also obfuscate formals in function pointer types.
181
              Fixes #2433.
182
-   Eva       [2019-04-05] Prints an analysis summary at the end, outlining the
183
184
              analysis coverage and the number of errors, warnings and emitted
              alarms. It can be disabled with the option -eva-msg-key=-summary
185
-   Eva       [2019-04-03] New option -eva-precision to globally configure the
186
187
188
              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.
189
190
-   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
191
              it does not introduce additional hypotheses on the program state
192
-*  Makefile  [2019-03-07] Do not attempt to install .cmx on bytecode-only
Virgile Prevosto's avatar
Virgile Prevosto committed
193
              architectures. Patch by M. Dogguy backported from Debian package
194
-   Libc      [2019-03-05] Better specs and removal of half-implemented ifdef
195
              that tried to take various POSIX versions into account
196
-*  Kernel    [2019-03-05] Better detection of invalid goto in presence of VLA
Virgile Prevosto's avatar
Virgile Prevosto committed
197
              (fixes #@499)
198
-   GUI       [2019-03-04] Compatibility with lablgtk3 and improved handling of
199
              some widgets
200
-   ACSL      [2019-03-01] Clarifies which C variables are in scope under a
201
              \at(·,L) (#@575)
202
-   Libc      [2019-02-26] Ask clang not to warn about unknown FRAMA_C_MODEL
203
              attribute when pre-processing frama-c's libc
204
205
206
207
-*  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
208
              must now indicate whether they should have a status.
209
210
o   Kernel    [2019-02-05] Integer API moving closer to Zarith
-   Eva       [2019-01-19] New warning category for detecting loops without
211
              'unroll' directive
212
213
-   Eva       [2019-01-31] Ignore annotations with "no_eva" tag
-*  ACSL      [2019-01-19] Accept C identifiers that happen to be ACSL keywords
214
              in volatile and reads clauses
215
-   Eva       [2019-01-10] Improved precision on nested loops (by postponing
David Bühler's avatar
David Bühler committed
216
              the widening on inner loops according to -eva-widening-period).
217
-*  Aorai     [2019-01-04] Fixes #@586: avoid removing the initial state
218
              of the automaton
219
-   Kernel    [2019-01-03] Add attributes for loop statements to allow
Virgile Prevosto's avatar
Virgile Prevosto committed
220
              distinguishing between for, while and dowhile loops.
221
-!  Kernel    [2019-01-03] Add statement attributes (sattr) to the AST. They
Virgile Prevosto's avatar
Virgile Prevosto committed
222
              are not printed by default, use -kernel-msg-key printer:attrs
223
-!  Kernel    [2019-01-03] Improved precision of integer abstract bitwise
Valentin Perrelle's avatar
Valentin Perrelle committed
224
              operators.
225
-*  Eva       [2018-12-17] Fixes -eva-split-return on uninitialized or escaping
226
              function returns when -eva-warn-copy-indeterminate is disabled.
227
228
229
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
230

231
232
233
234
################################
Open Source Release 18.0 (Argon)
################################

235
-!  Kernel    [2018-10-24] Log.error and Log.failure will eventually make
236
              Frama-C exit with a non-zero status. Fixes #@552
237
-   Kernel    [2018-10-24] More ergonomic command-line options for governing
238
              warning categories statuses.
239
-   Eva       [2018-10-24] Enable the memexec cache by default. It can be
240
              disabled by option -eva-no-memexec.
241
-   Eva       [2018-10-22] Improved performances when the symbolic locations
242
              domain and the memexec cache are enabled.
243
-   Eva       [2018-10-22] The memexec cache is now fully compatible with all
244
245
              abstract domains provided by Eva. However, the binding to the
              Apron domains disable memexec.
246
-   Eva       [2018-10-18] New experimental domain "numerors" inferring absolute
247
248
              and relative errors of floating-point computations. Enabled by the
              option -eva-numerors-domain. Does not handle loops for now.
249
-*  Kernel    [2018-10-18] Fixes parsing of compound initializers with anonymous
250
              fields. Fixes #2384
251
-*  Kernel    [2018-10-16] Consider that asm can change content of pointers
252
              used as inputs when generating assigns clauses. Fixes #@458
253
254
-   Eva       [2018-10-12] Remove option -obviously-terminates.
-   Kernel    [2018-10-05] New option -warn-invalid-bool, to warn when reading
255
              trap representations of type _Bool.
256
257
-   Eva       [2018-10-04] ACSL predicates with a "no_eva" tag are now ignored.
-   Eva       [2018-10-03] Warn about currently unsupported specifications
258
              of some libc functions.
259
260
261
262
-   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
263
264
              specific (aka C++ constructors and mutable fields) circumstances.
              Fixes #2395.
265
-   Kernel    [2018-09-14] New warning (disabled by default) when multiple side
266
267
              effects are unsequenced (CERT-EXP10-C recommandation).
              Fixes #@492
268
-   Eva       [2018-09-13] Remove option -val-warn-left-shift-negative, and
269
              comply with kernel option -warn-[left|right]-shift-negative.
270
-   Kernel    [2018-09-13] New options -warn-left-shift-negative (enabled by
271
272
              default) and -warn-right-shift-negative (disabled by default),
              to control the emission of alarms on shifts on negative integers.
273
o!  Constant Propagation [2018-09-12] Removing Db API for Constant Propagation
274
275
              plug-in. Calls to !Db.Constant_Propagation should be replaced by
              calls to Constant_Propagation.Api.
276
-   Eva       [2018-09-12] Reduction of values leading to division by zero
277
              alarms, when possible.
278
-   Eva       [2018-09-11] Better reduction of floating-point values cast into
279
              integer types when an alarm is emitted.
280
-   Metrics   [2018-09-06] Add option -metrics-used-files, to help identify
281
              unnecessary files given in the command line
282
283
284
-   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
285
              pointers on weak bases (created by allocations in loops).
286
-!  ACSL      [2018-08-28] Introduce extensions to global annotations and
287
288
              better characterization of each extension kind.
              See development guide for more information
289
-   Eva       [2018-08-28] All options of Eva start with -eva. Aliases to
290
              previous option names preserve backward compatibility.
291
-!  Eva       [2018-08-28] Rename plug-in shortname from 'value' to 'eva'. Eva
292
293
              is now properly named Eva in all logs, in the GUI, and as the
              emitter of the alarms.
294
-!  Kernel    [2018-08-23] Introduce Filepath dataype for more consistent
295
              normalization of filenames
296
-*  Kernel    [2018-08-23] Do not allow compound assignments to const variables
297
              Fixes #@384
298
-!  Kernel    [2018-08-23] Remove option -const-writable: const globals are
299
              unconditionally constants
300
-*  Eva       [2018-08-02] Deprecate option -val-warn-builtin-override in favor
301
              of warning category builtins:override.
302
-   Kernel    [2018-07-26] Fix compilation on OpenBSD
303
              patch contributed by madroach. Fixes #2379
304
-   Kernel    [2018-07-26] New option -remove-inlined to remove function(s)
305
306
              after -inline-calls, add category @inline to refer to all
              functions with inline attribute (for both options).
307
-   Eva       [2018-07-23] The debug category "garbled-mix" becomes a warning
308
              category. Better track of garbled mix created by specification.
309
-*  ACSL      [2018-07-23] Avoid removing cast of void ptr used as
310
              argument of function expecting a ptr with known size. Fixes #@432
311
o!  Kernel    [2018-07-23] Remove completely outdated module Dataflow.
312
              Deprecated since 3+ years. Use Dataflow2 instead.
313
-*  RTE       [2018-07-23] Stop generating spurious \initialized alarms.
314
              Fixes #@429  
315
-*  Kernel    [2018-07-06] Respect relative order of labels and ACSL annots.
316
              Fixes #@524
317
318
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, ...
319
320
              in addition to \le_float, \ge_float, ... Remove overloading of
              \le_float that made it accept double as arguments. Fixes #@502
321
-  Eva        [2018-06-28] New option -eva-report-red-statuses listing in
322
323
              a csv file the properties invalid for some states of the analysis
              (as in the "Red Alarms" panel of the GUI).
324
-  Eva        [2018-06-25] Release all builtins, including memset and memcpy,
325
              as open-source.
326
-  Eva        [2018-06-15] When a cvalue builtin is used, other domains use the
327
328
              frama-c libc specification to interpret the call without losing
              too much information.
329
-  Eva        [2018-06-14] The variables from the frama-c libc are no longer
330
              shown in the initial state print.
331
-  Eva        [2018-06-11] Improved precision of string builtins for strlen,
332
              strchr and memchr.
333
-  Eva        [2018-04-25] Renamed option -wlevel into -eva-widening-delay. New
334
335
              option -eva-widening-period to control the number of iterations
              between two widenings.
336
-  Eva        [2018-04-25] New propagation strategy that allows unrolling loops
337
338
339
340
341
              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.

342
343
344
############################################
Open Source Release 17.1 (Chlorine-20180502)
############################################
345

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

348
349
350
############################################
Open Source Release 17.0 (Chlorine-20180501)
############################################
351

352
-  Eva        [2018-04-25] Added scripts and templates to help automate case
353
              studies (in $FRAMAC_SHARE/analysis-scripts)
354
-* Typing     [2018-04-23] Stronger checks w.r.t. implicit conversions in
355
356
              function pointers (must have compatible types) and assignments
              (modifiable lvalues). Fixes #@479
357
358
-  Kernel     [2018-04-23] Added option -inline-calls for syntactic inlining
-* Kernel     [2018-04-19] Avoid crash when re-declaring a function with
359
              formals after it has been called without any. Fixes #@454
360
-  Kernel     [2018-04-13] Deprecate option -warn-decimal-float in favor of
361
              warning category parser:decimal-float
362
-  Kernel     [2018-04-13] More possible statuses for warning categories.
363
              Fixes #@486
364
o  Kernel     [2018-04-13] Change Cil.typeHasAttributeDeep into
365
              Cil.typeHasAttributeMemoryBlock. Fixes #@489
366
o* Logic      [2018-04-11] properly reset logic environment in case of typing
367
              errors. Fixes #@326
368
369
-  Eva        [2018-04-10] Interpret the logic constants \pi and \e.
-  Eva        [2018-04-06] Initialization of volatile pointers now keeps the
370
              base addresses of the pointer (with arbitrary offsets).
371
-  Eva        [2018-04-06] Fix the initialization of local volatile variables,
372
              which can always have any value.
373
-  Eva        [2018-04-06] In the logic, interpret the ACSL function \sign and
374
              the constructors \Positive and \Negative.
375
-  Metrics    [2018-04-05] When the value coverage is computed, also shows the
376
              total number of statements by function in the filetree of the Gui.
377
-  Gui        [2018-04-04] Added Preferences menu (shortcut: Ctrl+P) to set
378
              themes for property bullets and external source editor
379
380
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
381
              removed or deprecated
382
-  Eva        [2018-03-15] Avoid enumeration on values with too many bases —
383
              fixes a performance issue.
384
-  Gui        [2018-03-07] The preconditions of a function call can now be
385
386
              displayed before the call statement itself (click on status
              bullets with '+' or '-' to unfold/fold them)
387
388
-  Typing     [2018-03-02] Support for CERT EXP46-C
-  Eva        [2018-03-01] Fix a soundness bug in the equality domain: do not
389
390
              infer incorrect equalities between incomparable pointers,
              or between -0. and +0.
391
-  Eva        [2018-02-26] deprecate option -val-warn-on-alarms in favor of
392
              warning category alarm
393
-  Kernel     [2018-02-26] deprecate option -continue-annot-error in favor of
394
              warning category annot-error
395
-! Kernel     [2018-02-26] introduce warning categories, with various
396
              possible behaviors. Refactor management of debug categories
397
-* RTE        [2018-02-23] Do not emit spurious 'idx < 0' assert
398
              on gcc-style FAM. Fixes #@393
399
400
-* Kernel     [2018-02-23] Handle anonymous struct/union init. Fixes #@376
-  Eva        [2018-02-22] Equalities can be propagated through function calls.
401
402
              New options -eva-equality-through-calls[-function] to decide
              (globally or by function) which ones are kept from the caller.
403
-  Eva        [2018-02-21] When an lvalue lv is assigned or leaves the scope,
404
405
              the equality domain tries to replace lv by an equal term (if any)
              in the expressions depending on lv (instead of removing them).
406
o! Occurrence [2018-02-20] Removing Db API for Occurrence plug-in. Calls to
407
              !Db.Occurrence should be replaced by calls to Occurrence.Register.
408
o! Impact     [2018-02-20] Removing Db API for Impact plug-in. Calls to
409
              !Db.Impact should be replaced by calls to Impact.Register.
410
o! Users      [2018-02-20] Removing Db API for Users plug-in. Calls to
411
              !Db.Users should be replaced by calls to Users.Users_register.
412
-  Eva        [2018-02-13] Removed *_alloced_return base created for functions
413
414
              without body that return pointers. Such bases were imprecise
              and could be unsound in corner cases.
415
-  Eva        [2018-02-08] Shifts of addresses now create garbled mixes (as any
416
              other arithmetic operation).
417
418
-  Logic      [2018-02-07] Ghost code now supports /@ ... @/ annotations
-  Eva        [2018-02-06] By default, do not emit pointer_comparable alarms for
419
420
              non pointer operations. Always compute {0;1} for non pointer
              comparisons involving incomparable addresses.
421
422
-  Eva        [2018-02-01] Warn about unsupported allocates clauses.
-  Eva        [2018-01-30] The subdivision of evaluations (through the option
423
424
              -val-subdivide-non-linear) can subdivide the values of several
              lvalues simultaneously (on expressions such as x*x - 2*x*y + y*y).
425
-  Kernel     [2018-01-24] Better renaming of variables in case of name
426
              collision.
427
o! Kernel     [2018-01-24] Keep information about syntactic scope of local
428
429
              static variables. Accessed through
              Globals.Syntactic_search.find_in_scope.
430
-! Eva        [2018-01-24] Renamed option -val-malloc-returns-null to
431
              -val-alloc-returns-null, which also applies to realloc builtins.
432
-  Kernel     [2018-01-16] Added option -json-compilation-database to help with
433
              preprocessing. Requires yojson during Frama-C compilation.
434
-  Eva        [2018-01-15] New function post_analysis in abstract domains,
435
              called at the end of the analysis.
436
-  Eva        [2018-01-11] The Simple_memory functor lets builtins interpret C
437
              functions from the value of arguments to the result value.
438
-  Eva        [2018-01-11] Evaluate the preconditions of the functions for which
439
              a builtin is used; builtins do not emit alarms anymore.
440
-! Kernel     [2018-01-11] Alarms Logic_memory_access and Valid_string, that
441
              were only emitted by Eva builtins, are removed.
442
-* ACSL       [2017-12-14] Reinforce rejection of void* pointer types in the
443
444
              arguments of ACSL built-in constructs related to memory blocks
              and pointer dereferencing.
445
-* ACSL       [2017-12-14] Reinforce rejection of implicit casts from array
446
447
              types to pointer types in the arguments of ACSL built-in
              constructs related to memory blocks and pointer dereferencing.
448
-* Kernel     [2017-12-13] Clean up typechecking environment when dropping
449
              side-effects (in sizeof et al.). Fixes #@430
450
o! Kernel     [2017-12-13] Old Cil.isCharType renamed as Cil.isAnyCharType.
451
452
              New Cil.isCharType is now only true for plain char, neither signed
              nor unsigned. Derived functions (isCharPtr et al.) also updated
453
454
-  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
455
              propagates or warns on NaN and infinite values accordingly.
456
-! Kernel     [2017-12-07] Option -warn-not-finite-float renamed into
457
              -warn-special-float and extended (accepts non-finite/nan/none).
458
-  Kernel     [2017-12-07] Make some typechecking warnings controllable with
459
              -kernel-msg-key keys.
460
-  Eva        [2017-12-07] New option -val-skip-stdlib-specs, set by default.
461
462
              When analyzing the body of a function from Frama-C's standard
              library, specifications will be skipped.
463
-  Eva        [2017-11-28] New builtins for the single-precision mathematical
464
              functions fmodf, cosf, sinf and atan2f.
465
-! Eva        [2017-11-16] In the log, messages on preconditions are now
466
              reported with the location of the call site.
467
o! Eva        [2017-11-09] The Fval module now supports NaN and infinite values.
468
469
              Major API changes in Fval, Ival and Cvalue.V (regarding casts,
              mostly)
470
471
-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
472
              may be less precise than previously
473
-  Eva        [2017-11-09] Various improvements in the handling of
474
475
              floating-point variables: evaluation of \is_finite, computation
              of the bits of a floating-point range, etc
476
-  Eva        [2017-11-09] New panel "Red alarms" in the GUI that shows all red
477
478
              statuses emitted for some states during the analysis. They are not
              completely invalid, but should often be investigated first.
479
-* Eva        [2017-10-27] Fix bug in the handling of non-explicitly volatile
480
481
              fields inside volatile structs or unions

482
483
484
##########################################
Open Source Release 16.0 (Sulfur-20171101)
##########################################
485

486
-* Eva        [2017-10-27] Fix bugs when evaluating \ìnitialized, \dangling
487
              and \separated on addresses of bitfields
488
-* Eva        [2017-10-27] Fix bug in the handling of non-explicitly volatile
489
              fields inside volatile structs or unions
490
-  RTE        [2017-10-27] add option -rte-initialized to generate assertions
491
              over read accesses to potentially uninitialized locations.
492
-* RTE        [2017-10-16] Fix bounds of alarms emitted when downcasting to
493
              bitfields (issue #?2314)
494
495
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
496
497
              be rejected when the compiler does not support this construct,
              depending on the fields sizeof_fun and alignof_fun of the machdep
498
-* Kernel     [2017-10-11] More thorough checks on l-values with function type.
499
              Non-sensical expressions are now rejected at parsing type.
500
-  Eva        [2017-10-10] Uses assigns clauses to over-approximate the effects
501
              of assembly statements. Warns if no assigns clause is provided.
502
-* Eva        [2017-10-10] Fixes a performance issue in offsetmaps, that occured
503
              when reading or copying values smaller than cells in large arrays.
504
-  Eva        [2017-10-10] The backward propagation tries to reduce integer
505
              values by considering separately the bounds of their intervals.
506
-* Eva        [2017-10-10] Fixes an optimization issue where the reduction by a
507
              loop invariant just after widenings could impede the convergence.
508
-* Eva        [2017-10-10] Fixes a soundness bug where a loop invariant could be
509
              wrongly proved correct in some marginal cases.
510
511
+  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
512
              click on the header, while a left click sorts the tree.
513
-  Metrics    [2017-09-13] In the Gui, shows the percentage and the number of
514
              dead statements (when computed) for each function of the filetree.
515
-! Callgraph  [2017-09-01] Option -cg-init-roots replaced by -cg-service-roots
516
517
              (almost equivalent); new options -cg-function-pointers (ignore
              function pointers; unsound) and -cg-roots (compute subgraphs).
518
o! Eva        [2017-09-01] In abstract domains, compute_using_specification is
519
520
521
              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.
522
-  Eva        [2017-09-01] Various precision improvements in the interpretation
523
              of the behaviors of a specification.
524
-* Kernel     [2017-08-31] Fixes configure script on bytecode only architecture.
525
              Initial version of the patch by Debian. Fixes #2325
526
-* Kernel     [2017-08-31] Fix various typos in source code and user messages.
527
              Patch by Debian. Fixes #2323
528
-! Sparecode  [2017-08-31] Rename option -rm-unused-globals to
529
              -sparecode-rm-unused-globals.
530
531
o! ACSL       [2017-08-24] Refactor handling of logic labels in AST
-! Eva        [2017-08-03] Fix soundness (resp. precision) bug on big-endian
532
533
              (resp. little-endian) architectures. This bug triggered on
              low-level code, typically when using bitfields
534
-* Kernel     [2017-08-03] Strip bitfield attribute when performing integral
535
536
              promotions on bitfields of size short or char. Fixes incorrect
              attributes on the resulting expression.
537
-! ACSL       [2017-08-03] Explicitely disallow /* and */ in ACSL annotations.
538
539
540
541
542
              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)
543
-* Kernel     [2017-07-29] Fix unmarshalling of save files that contain more
544
              than 4Gb of uncompressed data. Patch from TIS-interpreter.
545
546
-* Eva        [2017-07-27] Fix performance issue with the equality domain.
-! Kernel     [2017-08-28] Fix invalid eids on code generated through loop
547
              unrolling
548
-! Slicing    [2017-08-28] Fix invalid eids on code generated through option
549
              -slicing-level >= 2
550
-! Eva        [2017-07-28] Fixed memory leak with option
551
              -val-subdivide-non-linear
552
o! Slicing    [2017-08-01] Removing Db API for Slicing plug-in. Calls to
553
              !Db.Slicing should be replaced by calls to Slicing.Api.
554
-o! Slicing   [2017-07-27] Removing deprecated '-slice-option' and related
555
556
              !Db.Slicing.Projet.print_exported_project. Minor changes into
	      !Db.Slicing.Projet.extract.
557
o! Scope      [2017-07-27] Removing Db API for Scope plug-in. Calls to
558
              !Db.Scope should be replaced by calls to Scope.
559
o! Report     [2017-07-24] Removing Db API for Report plug-in. Calls to
560
561
              !Db.Report.print should be replaced by calls to
              Report.Register.print.
562
-  RTE        [2017-07-17] Emits overflow alarms on unsigned left shift when
563
              -warn-unsigned-overflow is enabled.
564
-  Eva        [2017-07-17] Emits overflow alarms on unsigned left shift when
565
              -warn-unsigned-overflow is enabled.
566
-  Kernel     [2017-07-10] Composite types are now required to have equal tags
567
              as per the C standard; no more support for isomorphic structs.
568
-  Eva        [2017-07-01] In the GUI, the "Values" panel displays the values
569
              computed by using the properties inferred by all enabled domains.
570
-! Eva        [2017-06-30] Better handling of function alloca(), via builtin
571
              Frama_C_alloca.
572
-* Eva        [2017-06-28] The cvalue states saved after each statement are now
573
              properly deleted when an Eva parameter is changed in the GUI.
574
o  Eva        [2017-06-26] New functor in domains/simple_memory.ml to build a
575
576
              complete domain from a value abstraction. The abstract states link
              each scalar variable of a program to an abstract value.
577
578
-  Eva        [2017-06-26] New sign domain for demonstration purposes only.
-* Kernel     [2017-06-09] Parser now handle mixed concatenation of
579
              string and wstring. Fixes #@1467
580
-  Eva        [2017-06-07] The subdivision of the evaluation of non-linear
581
582
              expressions (through the -val-subdivide-non-linear option) also
              applies to the new evaluations requested by the equality domain.
583
-* Eva        [2017-06-14] Fix a crash when downcasting pointer values with
584
              the option -val-warn-signed-converted-downcast enabled.
585
586
-* 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
587
              is now optional, and will be removed in a later version.
588
*  Eva        [2017-05-24] Fix soundness bug in string builtins where some
589
              invalid offsets did not generate alarms.
590
-  Eva        [2017-05-22] Removes all effects of the special functions
591
592
              Frama_C_[dump|show]_each on the analyses: no alarms are emitted
              and the states are never reduced on these calls.
593
-  Eva        [2017-05-22] Frama_C_dump_each prints the state of each available
594
              domain whose log category is enabled.
595
-  Eva        [2017-05-22] New directive Frama_C_domain_show_each prints the
596
597
              internal properties about the arguments inferred by each available
              domain whose log category is enabled.
598
o! Eva        [2017-05-22] Abstract domains have to provide a log category and
599
600
              a function show_expr that prints the internal properties inferred
              about an expression.
601
602
-  Kernel     [2017-05-18] Added option -print-return to inline gotos to return
-  RTE        [2017-05-12] add -warn-not-finite-float for checking
603
              that infinite and NaN floats are not produced.
604
-! Kernel     [2017-05-17] qualifiers are dropped from the return type of
605
              functions, as they make no real sense
606
-* Kernel     [2017-04-27] stop removing const attribute on local variables.
607
              Fixes #@301
608
o! Kernel     [2017-04-27] Remove needless repetition of declared logic labels
609
              in Tapp and Papp nodes. Fixes #@274
610
o! Kernel     [2017-04-27] Completely separate types between Cil_types and
611
              Logic_ptree, removing needless polymorphism
612
-  Eva        [2017-04-06] More precise evaluation of \initialized and
613
614
              \dangling predicates.

615
616
617
##############################################
Open Source Release 15.0 (Phosphorus-20170501)
##############################################
618

619
-* Eva        [2017-05-08] Fix widening in the gauges domain, in particular with
620
621
              nested loops and pointers that change base address through
              iterations
622
623
-* Eva        [2017-04-25] Perform widening in the symbolic locations domain.
-* Eva        [2017-04-24] Fixes a crash when backward-propagating an imprecise
624
625
              value on a 32-bits floating point addition. A non-single precision
              value was erroneously returned.
626
-* Eva        [2017-04-05] Fixes a crash with the -val-subdivide-non-linear
627
              option, on subdivisions of evaluations involving pointer values.
628
-! Eva        [2017-03-31] Renamed dynamic allocation builtins for
629
630
              improved consistency. In particular, Frama_C_alloc_size
              becomes Frama_C_malloc_fresh.
631
632
-  Eva        [2017-03-31] New option -val-builtins-list
-* Scope      [2017-03-31] Fix bug in the functions of Db.Scope in presence of
633
634
              alarms refering to volatile memory locations, or to variables
              that leave scope. Also impacts Eva option -remove-redundant-alarms
635
636
-  Eva        [2017-03-31] Activate option -remove-redundant-alarms by default.
-  Inout      [2017-03-28] Option -inout-callwise is now always active, and will
637
              be removed in a later version
638
-* Inout      [2017-03-28] Prevent formal variables of functions with only a
639
              specification from leaking into results
640
641
-  Kernel     [2017-03-28] Dynlink is now mandatory, no degraded static mode.
o! Eva        [2017-03-17] Incompatible API changes in module Cvalue.Model.
642
643
              Functions named 'unspecified' have been renamed into
              'indeterminate', and some arguments have been removed.
644
o! Gui        [2017-03-10] Signature change for constructor
645
              Pretty_source.PVDecl
646
-! Kernel     [2017-03-10] Explicit AST nodes to mark local variables
647
              initialization.
648
-! Kernel     [2017-03-10] Better handling of VLA (use explicit function calls
649
              to mark deallocation of VLA at appropriate program points)
650
651
652
-* Callgraph  [2017-03-10] Fixes inverted callers/callee in indirect calls
-! Eva        [2017-03-09] Option -val-show-progress is now unset by default
-* Eva        [2017-03-08] Fix bug #2277. The initial state of the analysis
653
654
              now depends on all relevant options, including kernel options
              -warn-...
655
-! Variadic   [2017-03-08] Change of command line argument names for the
656
657
658
              plugin Variadic. The new names are more expressive and avoid
              confusions with the plugin Value. Use -variadic-translation or
              -variadic-no-translation instead of -va or -no-va.
659
-! Value      [2017-03-07] Support for the legacy value analysis has been
660
661
              abandoned, Eva is now always active. Option -no-eva has been
              removed.
662
-* Eva        [2017-03-07] Unsound support for recursion, through option
663
664
665
              -val-ignore-recursive-calls. The support of recursion through
              the use of 'assigns' clauses, previously available in Value,
              was unsound and has been removed
666
667
-! Kernel     [2017-03-01] Zarith library is now required
-* Kernel     [2017-02-24] Fix crash when loading a saved file without a plug-in
668
              which has previously emitted a status with a tuning parameter.
669
-  Eva        [2017-02-06] New (internal) mechanism to handle C functions'
670
671
              return values. Messages now mention \result<foo> for the
              value returned by 'foo'.
672
-  Variadic   [2017-02-08] The plugin is now enabled by default. Use the
673
674
675
              option -variadic-no-translation to keep the original behaviour.
              The specification generated for the fprintf function family is
              now more accurate.
676
-  Kernel     [2017-01-26] New option -print-libc, to expand include directives
677
              for files in the Frama-C stdlib (no longer expanded by default).
678
679
680
-* Obfuscator [2017-01-19] Fix typo in help message (bts #2269).
-  Kernel     [2017-01-09] Bash completion for Frama-C options. See #@154.
-* Kernel     [2016-12-09] Fixes oneret normalization in presence of
681
              statement contract and absence of return. See #@255 and #2235.
682
683
684
-  Kernel     [2016-12-06] New option -print-machdep (help group).
-  Rte        [2016-11-25] Remove option -rte-all.
-* Cil        [2016-11-20] Pointer subtractions with arguments of incompatible
685
686
              types are now refused. The resulting expression is typed as
              ptrdiff_t instead of int.
687
-  Value      [2016-11-18] Widen hints directives @widen_hints now accept
688
689
              arbitrary l-values (evaluated at analysis time) in place of
              variables.
690
-* Kernel     [2016-11-17] Fixed some issues with #pragma pack() behavior,
691
692
              in both GCC and MSVC machdeps. Also fixed some related issues
              with __aligned__ and __packed__ attributes (including bts #2249).
693
694
695
-o Kernel     [2016-11-17] Utility API for checking volatile attribute in Cil.
-  Metrics    [2016-11-17] Programmatic API for some functions via Metrics.mli.
-  Kernel     [2016-11-07] New option -no-autoload-plugins (equivalent to old
696
              -no-dynlink); mostly for internal use.
697
-! Kernel     [2016-10-19] Stricter verification for extern, static and inline
698
              specifiers (support for CERT DCL-36-C coding rule)
699
o* Eva        [2016-10-22] Functions Db.Value.fun_set_args and
700
701
              Db.Value.globals_set_initial_state are now compatible with Eva.

702
703
704
###########################################
Open Source Release 14.0 (Silicon-20161101)
###########################################
705

706
-*! Eva       [2016-10-29] Fix soundness bug on statements with RTE or
707
708
709
710
711
              programmatically-added user assertions (bts #2258). This
              leads to minor changes in the way states are propagated when
              all slevel has been consumed. Also, consolidated states now
              return the abstraction before any reduction by assertions or
              alarms.
712
-* Eva        [2016-10-20] Fix bug in the bitwise domain, on some applications
713
              of the & and | operators
714
-  Value      [2016-10-20] New (experimental) option -val-builtins-auto, to
715
716
              automatically replace known C functions by builtins. Will
              be set by default in Phosphorus.
717
-* Value      [2016-10-19] Frama_C_cos and Frama_C_sin builtins are now
718
719
              precise by default. The former Frama_C_cos / Frama_Csin_precise
              have been removed
720
-* Kernel     [2016-10-18] Fix bug when pretty printing an ACSL term
721
              "divisor / *p" (bts #2250).
722
-  Eva        [2016-10-18] New experimental Gauges domain, that relates
723
              integer variable to loop counters.
724
-! Kernel     [2016-10-15] Fix major bug in the backward dataflow of module
725
              Dataflows
726
-! Scope      [2016-10-15] Fix bug that might lead to unsoundness and / or
727
              looping in 'Datascope' functionality (#!235)
728
-* Eva        [2016-10-11] Prevent incorrect reductions on memory locations
729
              with volatile qualifier
730
-! Value      [2016-10-11] Option -val-warn-copy-indeterminate is now set by
731
              default. See command-line help if you want to deactivate it.
732
-  Kernel     [2016-10-07] Fix bug that may occur when modifying several times
733
              command line-options taking functions as argument (issue #@109)
734
-! Libc       [2016-10-07] Functions in share/libc.c have been inlined into
735
              the proper .c files under share/libc
736
-  Eva        [2016-10-07] More systematic backward-propagation between
737
              actual parameters and formals
738
-  Nonterm    [2016-10-05] overall increase in precision, especially on
739
740
              compound statements (if, switch, loops...). Verbosity has been
              decreased
741
-  Nonterm    [2016-10-05] New options -nonterm-ignore f1,..,fn (to
742
743
              ignore calls to functions f1,..,fn) and -nonterm-dead-code
              (to warn about syntactically dead code)
744
-  Value      [2016-09-23] Extended support for syntactic widening hints
745
              (@widen_hints - see the Value user manual for more details)
746
-  Value      [2016-09-20] New builtins for string-related functions:
747
748
              Frama_C_strlen, Frama_C_strchr, Frama_C_strnlen,
              Frama_C_memchr and Frama_C_rawmemchr
749
-  Value      [2016-09-20] valid_string and valid_read_string predicates
750
              are now evaluated by Value
751
-* Eva        [2016-09-18] Fix bug in equality domain, after assignements
752
753
              lv = e where the modified locations intersect those involved in
              computing lv
754
-* Eva        [2016-09-18] fix performance bug in the equality domain,
755
              especially visible on programs with many local variables.
756
757
758
o! Kernel     [2016-09-16] Rename some types of the logic AST for more coherence
-  Kernel     [2016-09-13] Support for C11 redefinition of typedefs
-  Kernel     [2016-09-06] Deprecated Pretty_utils.sfprintf,
759
              use Format.asprintf instead.
760
-! Logic      [2016-08-31] Refactoring of ACSL extensions + allow extensions
761
              in loop annotations
762
-! Libc       [2016-08-29] New file share/libc/string.c, with simple
763
764
              implementations for C99 functions defined in string.h.
              Duplicate implementations were removed from share/libc.c.
765
-* Kernel     [2016-08-12] Fix bug #2239 about unsoundness of callgraph's
766
              services computation (bug introduced in Frama-C Magnesium).