Changelog 249 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 17 18
##################################
Open Source Release <next-release>
##################################
Julien Signoles's avatar
Julien Signoles committed
19

20 21
-   Metrics   [2020-10-27] Add json output in addition to text and html

22 23 24 25
###################################
Open Source Release 22.0 (Titanium)
###################################

26
-   MdR       [2020-10-19] Update Sarif output to 2.1.0 + prettier URI
27
-   Dev       [2020-10-20] Support for OCamlGraph 2.0.0
28
-   ACSL      [2020-10-16] Allows for axiomatic blocks-like extensions
29 30 31
-   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.
32 33
-   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
34 35
-   Kernel    [2020-10-09] Add option -print-config-json, to output Frama-C
              configuration data in JSON format.
36
-   Logic     [2020-10-14] '\from' now accepts '&v' expressions
37 38
-   Metrics   [2020-10-01] Distinguish between undefined but specified functions
              and functions with neither definition nor specification.
39 40
-*  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
41 42 43
-   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
44 45
-   Kernel    [2020-09-21] Option -permissive now allows non-existent option
              names.
Allan Blanchard's avatar
Allan Blanchard committed
46 47
-   Logic     [2020-09-11] Introduce check-only annotations for
              requires, ensures, loop invariant and lemmas
Virgile Prevosto's avatar
Virgile Prevosto committed
48 49
-   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
50 51
-   Eva       [2020-09-07] Deprecates legacy options aliases -val-* in favor
              of option names -eva-*.
Andre Maroneze's avatar
Andre Maroneze committed
52
-*  Slicing   [2020-09-07] Better handling of invalid command line options.
53 54 55 56
-   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.
57
-!  Kernel    [2020-07-21] OCaml version greater than or equal to 4.08.1 required.
58 59
-   Eva       [2020-05-29] New builtins for trigonometric functions acos, asin
              and atan (and their single-precision version acosf, asinf, atanf).
60
-   Kernel    [2020-05-28] Support for C11's _Thread_local storage specifier
61 62
-   Kernel    [2020-05-26] New option -explain, which provides help messages
              for options used on the command line.
63 64 65 66 67
-   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
68
-   Eva       [2020-05-20] Supports the ACSL mathematical operator \abs
69 70
-   Kernel    [2020-05-18] Support for C11's _Noreturn function specifier

71 72 73 74
###################################
Open Source Release 21.1 (Scandium)
###################################

75 76 77 78
###################################
Open Source Release 21.0 (Scandium)
###################################

79 80 81
-*  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
82
              mere strings.
83
-   Eva       [2020-04-10] Fixes the Memexec cache on functions with logical
84
              annotations about variables unused in the C body of the function.
85
-   Eva       [2020-04-06] New option -eva-domains-function to enable domains
86 87 88
              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].
89
-   Eva       [2020-04-03] New experimental builtins for dynamic allocation
90
              Frama_C_*alloc_imprecise: faster convergence, but very imprecise.
91
-   Kernel    [2020-04-01] Report user errors when keys are not bound to a
92 93
              value for command-line options that require pairs of key:value
              as arguments. Such keys were silently ignored.
94 95 96 97
*!  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
98 99
              default) to warn on invalid pointer arithmetics resulting in a
              pointer that does not point to an object or one past an object.
100 101 102
-   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
103 104
              default), to warn when a conversion between pointer and integer
              might provoke a loss of precision.
105 106
-   Kernel    [2020-03-20] Add option -cpp-extra-args-per-file
-*  Kernel    [2020-03-18] Fixes #@823 (-load-module/-load-script now accept
107
              spaces in filename)
108 109 110
-*  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
111
              -eva-domains
112 113
-   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
114
              Frama-C libc specifications.
115
-   Eva       [2020-03-03] Slightly better heuristics for the subdivision of
David Bühler's avatar
David Bühler committed
116
              evaluations (option -eva-subdivide-non-linear).
117
-   Instantiate [2020-03-02] New plug-in Instantiate, to create function
118 119 120
              specializations for specific plug-ins and functions (e.g. malloc,
              memcpy, memset), to overcome limitations due to their
              specifications.
121 122
-   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
123
              control flow of the non-ghost program
124
-*  Kernel    [2020-02-17] fixes issue that could prevent loading plug-ins on
Virgile Prevosto's avatar
Virgile Prevosto committed
125
              Windows installation
126
-   Kernel    [2020-02-14] -constfold now takes into account value
Virgile Prevosto's avatar
Virgile Prevosto committed
127
              of const globals
128
o   ACSL      [2020-02-13] Add possibility for ACSL extensions to alter the
Virgile Prevosto's avatar
Virgile Prevosto committed
129 130
              sequence of untyped terms they receive from the parser. Make also
              possible to customize the short pretty printer of extensions.
131
o   Kernel    [2020-02-13] Deprecated:
Virgile Prevosto's avatar
Virgile Prevosto committed
132 133 134 135
                           - Logic_typing.register_*_extension
                           - Cil_printer.register_*_extension
                           - Cil.register_behavior_extension
                           Use Acsl_extension.register_* instead
136
-   Eva       [2020-02-12] New option "-eva-domains <d1>,<d2>,..." to enable
137 138
              several domains at once. The list of available domains is given
              in the help message of the option.
139
o!  Eva       [2020-02-12] Simplifies abstract domain signature by removing the
140
              Transfer functor.
141
-*  Eva       [2020-02-12] Fixes the evaluation of logic predicates involving
142
              empty sets.
143
-   Eva       [2020-02-07] Supports the logic evaluation of quantifiers
144
              introducing mathematical variables (integer or real).
145
o!  Kernel    [2020-02-04] Removed FCBuffer, FCMap and FCSet. Use directly
146
              OCaml stdlib modules Buffer, Map and Set instead.
147
-   Eva       [2020-02-04] Renamed option -eva-malloc-functions into
148
              -eva-alloc-functions. Also contains calloc and realloc by default.
149 150
-*  GUI       [2020-01-24] Fix order of globals in the source panel.
-   Eva       [2020-01-23] Adds consistency checks on return and parameters
151
              types between a builtin and the replaced C function.
152
-   Eva       [2020-01-23] Subdivisions can now be enabled locally:
153 154 155
              - 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
156

157
##################################
Andre Maroneze's avatar
Andre Maroneze committed
158
Open Source Release 20.0 (Calcium)
Andre Maroneze's avatar
Andre Maroneze committed
159
##################################
Andre Maroneze's avatar
Andre Maroneze committed
160

161
-   Eva       [2019-11-25] In the summary, fixes the number of alarms by
David Bühler's avatar
David Bühler committed
162 163
              category when the RTE plugin is used, and do not count logical
              properties in dead code as proven.
164
-!  Kernel    [2019-10-31] More stringent verifications on the use of ghost
Virgile Prevosto's avatar
Virgile Prevosto committed
165
              variable in non ghost-code. Fixes #2421
166
-   MdR       [2019-10-31] New plug-in Markdown-Report (MdR) for markdown and
167
              SARIF outputs
168
-   Eva       [2019-10-23] In the summary, fixes the total number of functions
David Bühler's avatar
David Bühler committed
169
              (and thus the computed analysis coverage).
170
-   Eva       [2019-10-23] New option -eva-auto-loop-unroll N to unroll all
171
              loops whose number of iterations can be easily bounded by <N>.
172
-   Eva       [2019-10-21] New octagon domain inferring relations of the form
173 174 175 176 177
              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.
178 179
-   ACSL      [2019-10-04] Support for ghost parameters
-   Eva       [2019-10-04] Evaluates ACSL predicates \is_plus_infinity and
180
              \is_minus_infinity.
181 182 183
-   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:
184
              developers of new domains no longer need to modify Eva's engine.
185 186
-*  Kernel    [2019-09-13] Fixes Hptmap on keys with id greater than 2^28.
-*  Makefile  [2019-09-12] Fixes #2378 - bytecode only compilation (patch
187
              contributed by madroach) and use -thread where needed.
188
-*  Eva       [2019-08-21] Fixes the reduction by the negation of \initialized
189
              and \dangling predicates on imprecise lvalues.
190
-*  Kernel    [2019-08-20] Fixes a rare but critical bug which occured when
Julien Signoles's avatar
Julien Signoles committed
191 192 193 194 195 196
              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).
197
-*  Kernel    [2019-08-20] Fixed sequence of -removed-projects and -then
Julien Signoles's avatar
Julien Signoles committed
198
              options.
199
o   Ptests    [2019-08-05] Add new MODULE directive for compiling and loading
200
              an auxiliary OCaml module for a test
201 202 203
-   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
204 205
              from Cil into a new module Visitor_behavior. Apply the migration
              script potassium2calcium.sh to update your plug-ins automatically.
206 207 208 209 210
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
211
              eq_float, le_float, eq_double, le_double, etc.
212
o!  Kernel    [2019-06-28] removes AST constructors TCoerce, TCoerceE,
Julien Signoles's avatar
Julien Signoles committed
213
              PLCoercion, PLCoercionE, Psubtype and PLsubtype
214
-*  Kernel    [2019-06-20] fixes dangling ref when removing unused static local
Virgile Prevosto's avatar
Virgile Prevosto committed
215

Virgile Prevosto's avatar
Virgile Prevosto committed
216 217 218 219
####################################
Open Source Release 19.0 (Potassium)
####################################

220 221
-*  RTE       [2019-05-24] fixes a crash when visiting variable declarations
-   Eva       [2019-04-19] The new annotation /*@ split exp; */ enumerates the
222 223 224 225
              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.
226
-   Eva       [2019-04-19] New option -eva-partition-history N to delay the join
227 228 229 230
              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.
231
-   Eva       [2019-04-19] Loop unroll annotations now accept non-constant but
232
              bounded expressions as the maximum number of unrollings to perform.
233 234
-*  Kernel    [2019-04-09] Avoid crashing on one-letter attributes. Fixes #2432
-*  Obfuscator [2019-04-09] Also obfuscate formals in function pointer types.
235
              Fixes #2433.
236
-   Eva       [2019-04-05] Prints an analysis summary at the end, outlining the
237 238
              analysis coverage and the number of errors, warnings and emitted
              alarms. It can be disabled with the option -eva-msg-key=-summary
239
-   Eva       [2019-04-03] New option -eva-precision to globally configure the
240 241 242
              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.
243 244
-   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
245
              it does not introduce additional hypotheses on the program state
246
-*  Makefile  [2019-03-07] Do not attempt to install .cmx on bytecode-only
Virgile Prevosto's avatar
Virgile Prevosto committed
247
              architectures. Patch by M. Dogguy backported from Debian package
248
-   Libc      [2019-03-05] Better specs and removal of half-implemented ifdef
249
              that tried to take various POSIX versions into account
250
-*  Kernel    [2019-03-05] Better detection of invalid goto in presence of VLA
Virgile Prevosto's avatar
Virgile Prevosto committed
251
              (fixes #@499)
252
-   GUI       [2019-03-04] Compatibility with lablgtk3 and improved handling of
253
              some widgets
254
-   ACSL      [2019-03-01] Clarifies which C variables are in scope under a
255
              \at(·,L) (#@575)
256
-   Libc      [2019-02-26] Ask clang not to warn about unknown FRAMA_C_MODEL
257
              attribute when pre-processing frama-c's libc
258 259 260 261
-*  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
262
              must now indicate whether they should have a status.
263 264
o   Kernel    [2019-02-05] Integer API moving closer to Zarith
-   Eva       [2019-01-19] New warning category for detecting loops without
265
              'unroll' directive
266 267
-   Eva       [2019-01-31] Ignore annotations with "no_eva" tag
-*  ACSL      [2019-01-19] Accept C identifiers that happen to be ACSL keywords
268
              in volatile and reads clauses
269
-   Eva       [2019-01-10] Improved precision on nested loops (by postponing
David Bühler's avatar
David Bühler committed
270
              the widening on inner loops according to -eva-widening-period).
271
-*  Aorai     [2019-01-04] Fixes #@586: avoid removing the initial state
272
              of the automaton
273
-   Kernel    [2019-01-03] Add attributes for loop statements to allow
Virgile Prevosto's avatar
Virgile Prevosto committed
274
              distinguishing between for, while and dowhile loops.
275
-!  Kernel    [2019-01-03] Add statement attributes (sattr) to the AST. They
Virgile Prevosto's avatar
Virgile Prevosto committed
276
              are not printed by default, use -kernel-msg-key printer:attrs
277
-!  Kernel    [2019-01-03] Improved precision of integer abstract bitwise
Valentin Perrelle's avatar
Valentin Perrelle committed
278
              operators.
279
-*  Eva       [2018-12-17] Fixes -eva-split-return on uninitialized or escaping
280
              function returns when -eva-warn-copy-indeterminate is disabled.
281 282 283
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
284

285 286 287 288
################################
Open Source Release 18.0 (Argon)
################################

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

396 397 398
############################################
Open Source Release 17.1 (Chlorine-20180502)
############################################
399

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

402 403 404
############################################
Open Source Release 17.0 (Chlorine-20180501)
############################################
405

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

536 537 538
##########################################
Open Source Release 16.0 (Sulfur-20171101)
##########################################
539

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

669 670 671
##############################################
Open Source Release 15.0 (Phosphorus-20170501)
##############################################
672

673
-* Eva        [2017-05-08] Fix widening in the gauges domain, in particular with
674 675
              nested loops and pointers that change base address through
              iterations
676 677
-* Eva        [2017-04-25] Perform widening in the symbolic locations domain.
-* Eva        [2017-04-24] Fixes a crash when backward-propagating an imprecise
678 679
              value on a 32-bits floating point addition. A non-single precision
              value was erroneously returned.
680
-* Eva        [2017-04-05] Fixes a crash with the -val-subdivide-non-linear
681
              option, on subdivisions of evaluations involving pointer values.
682
-! Eva        [2017-03-31] Renamed dynamic allocation builtins for
683 684
              improved consistency. In particular, Frama_C_alloc_size
              becomes Frama_C_malloc_fresh.
685 686
-  Eva        [2017-03-31] New option -val-builtins-list
-* Scope      [2017-03-31] Fix bug in the functions of Db.Scope in presence of
687 688
              alarms refering to volatile memory locations, or to variables
              that leave scope. Also impacts Eva option -remove-redundant-alarms
689 690
-  Eva        [2017-03-31] Activate option -remove-redundant-alarms by default.
-  Inout      [2017-03-28] Option -inout-callwise is now always active, and will
691
              be removed in a later version
692