Changelog

###############################################################################
# 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                                               #
###############################################################################

##################################
Open Source Release <next-release>
##################################

-*  Kernel    [2019/06/20] fixes dangling ref when removing unused static local

####################################
Open Source Release 19.0 (Potassium)
####################################

-*  RTE       [2019/05/24] fixes a crash when visiting variable declarations
-   Eva       [2019/04/19] The new annotation /*@ split exp; */ enumerates the
              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.
-   Eva       [2019/04/19] New option -eva-partition-history N to delay the join
              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.
-   Eva       [2019/04/19] Loop unroll annotations now accept non-constant but
              bounded expressions as the maximum number of unrollings to perform.
-*  Kernel    [2019/04/09] Avoid crashing on one-letter attributes. Fixes #2432
-*  Obfuscator [2019/04/09] Also obfuscate formals in function pointer types.
              Fixes #2433.
-   Eva       [2019/04/05] Prints an analysis summary at the end, outlining the
              analysis coverage and the number of errors, warnings and emitted
              alarms. It can be disabled with the option -eva-msg-key=-summary
-   Eva       [2019/04/03] New option -eva-precision to globally configure the
              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.
-   Inout     [2019/04/01] Fix performance issue when initializing large arrays.
-   ACSL      [2019/03/08] Add check annotation, similar to assert except that
              it does not introduce additional hypotheses on the program state
-*  Makefile  [2019/03/07] Do not attempt to install .cmx on bytecode-only
              architectures. Patch by M. Dogguy backported from Debian package
-   Libc      [2019/03/05] Better specs and removal of half-implemented ifdef
              that tried to take various POSIX versions into account
-*  Kernel    [2019/03/05] Better detection of invalid goto in presence of VLA
              (fixes #@499)
-   GUI       [2019/03/04] Compatibility with lablgtk3 and improved handling of
              some widgets
-   ACSL      [2019/03/01] Clarifies which C variables are in scope under a
              \at(·,L) (#@575)
-   Libc      [2019/02/26] Ask clang not to warn about unknown FRAMA_C_MODEL
              attribute when pre-processing frama-c's libc
-*  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
              must now indicate whether they should have a status.
o   Kernel    [2019/02/05] Integer API moving closer to Zarith
-   Eva       [2019/01/19] New warning category for detecting loops without
              'unroll' directive
-   Eva       [2019/01/31] Ignore annotations with "no_eva" tag
-*  ACSL      [2019/01/19] Accept C identifiers that happen to be ACSL keywords
              in volatile and reads clauses
-   Eva       [2019/01/10] Improved precision on nested loops (by postponing
              the widening on inner loops according to -eva-widening-period).
-*  Aorai     [2019/01/04] Fixes #@586: avoid removing the initial state
              of the automaton
-   Kernel    [2019/01/03] Add attributes for loop statements to allow
              distinguishing between for, while and dowhile loops.
-!  Kernel    [2019/01/03] Add statement attributes (sattr) to the AST. They
              are not printed by default, use -kernel-msg-key printer:attrs
-!  Kernel    [2019/01/03] Improved precision of integer abstract bitwise
              operators.
-*  Eva       [2018/12/17] Fixes -eva-split-return on uninitialized or escaping
              function returns when -eva-warn-copy-indeterminate is disabled.
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

################################
Open Source Release 18.0 (Argon)
################################

-!  Kernel    [2018/10/24] Log.error and Log.failure will eventually make
              Frama-C exit with a non-zero status. Fixes #@552
-   Kernel    [2018/10/24] More ergonomic command-line options for governing
              warning categories statuses.
-   Eva       [2018/10/24] Enable the memexec cache by default. It can be
              disabled by option -eva-no-memexec.
-   Eva       [2018/10/22] Improved performances when the symbolic locations
              domain and the memexec cache are enabled.
-   Eva       [2018/10/22] The memexec cache is now fully compatible with all
              abstract domains provided by Eva. However, the binding to the
              Apron domains disable memexec.
-   Eva       [2018/10/18] New experimental domain "numerors" inferring absolute
              and relative errors of floating-point computations. Enabled by the
              option -eva-numerors-domain. Does not handle loops for now.
-*  Kernel    [2018/10/18] Fixes parsing of compound initializers with anonymous
              fields. Fixes #2384
-*  Kernel    [2018/10/16] Consider that asm can change content of pointers
              used as inputs when generating assigns clauses. Fixes #@458
-   Eva       [2018/10/12] Remove option -obviously-terminates.
-   Kernel    [2018/10/05] New option -warn-invalid-bool, to warn when reading
              trap representations of type _Bool.
-   Eva       [2018/10/04] ACSL predicates with a "no_eva" tag are now ignored.
-   Eva       [2018/10/03] Warn about currently unsupported specifications
              of some libc functions.
-   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
              specific (aka C++ constructors and mutable fields) circumstances.
              Fixes #2395.
-   Kernel    [2018/09/14] New warning (disabled by default) when multiple side
              effects are unsequenced (CERT-EXP10-C recommandation).
              Fixes #@492
-   Eva       [2018/09/13] Remove option -val-warn-left-shift-negative, and
              comply with kernel option -warn-[left|right]-shift-negative.
-   Kernel    [2018/09/13] New options -warn-left-shift-negative (enabled by
              default) and -warn-right-shift-negative (disabled by default),
              to control the emission of alarms on shifts on negative integers.
o!  Constant Propagation [2018/09/12] Removing Db API for Constant Propagation
              plug-in. Calls to !Db.Constant_Propagation should be replaced by
              calls to Constant_Propagation.Api.
-   Eva       [2018/09/12] Reduction of values leading to division by zero
              alarms, when possible.
-   Eva       [2018/09/11] Better reduction of floating-point values cast into
              integer types when an alarm is emitted.
-   Metrics   [2018/09/06] Add option -metrics-used-files, to help identify
              unnecessary files given in the command line
-   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
              pointers on weak bases (created by allocations in loops).
-!  ACSL      [2018/08/28] Introduce extensions to global annotations and
              better characterization of each extension kind.
              See development guide for more information
-   Eva       [2018/08/28] All options of Eva start with -eva. Aliases to
              previous option names preserve backward compatibility.
-!  Eva       [2018/08/28] Rename plug-in shortname from 'value' to 'eva'. Eva
              is now properly named Eva in all logs, in the GUI, and as the
              emitter of the alarms.
-!  Kernel    [2018/08/23] Introduce Filepath dataype for more consistent
              normalization of filenames
-*  Kernel    [2018/08/23] Do not allow compound assignments to const variables
              Fixes #@384
-!  Kernel    [2018/08/23] Remove option -const-writable: const globals are
              unconditionally constants
-*  Eva       [2018/08/02] Deprecate option -val-warn-builtin-override in favor
              of warning category builtins:override.
-   Kernel    [2018/07/26] Fix compilation on OpenBSD
              patch contributed by madroach. Fixes #2379
-   Kernel    [2018/07/26] New option -remove-inlined to remove function(s)
              after -inline-calls, add category @inline to refer to all
              functions with inline attribute (for both options).
-   Eva       [2018/07/23] The debug category "garbled-mix" becomes a warning
              category. Better track of garbled mix created by specification.
-*  ACSL      [2018/07/23] Avoid removing cast of void ptr used as
              argument of function expecting a ptr with known size. Fixes #@432
o!  Kernel    [2018/07/23] Remove completely outdated module Dataflow.
              Deprecated since 3+ years. Use Dataflow2 instead.
-*  RTE       [2018/07/23] Stop generating spurious \initialized alarms.
              Fixes #@429  
-*  Kernel    [2018/07/06] Respect relative order of labels and ACSL annots.
              Fixes #@524
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, ...
              in addition to \le_float, \ge_float, ... Remove overloading of
              \le_float that made it accept double as arguments. Fixes #@502
-  Eva        [2018/06/28] New option -eva-report-red-statuses listing in
              a csv file the properties invalid for some states of the analysis
              (as in the "Red Alarms" panel of the GUI).
-  Eva        [2018/06/25] Release all builtins, including memset and memcpy,
              as open-source.
-  Eva        [2018/06/15] When a cvalue builtin is used, other domains use the
              frama-c libc specification to interpret the call without losing
              too much information.
-  Eva        [2018/06/14] The variables from the frama-c libc are no longer
              shown in the initial state print.
-  Eva        [2018/06/11] Improved precision of string builtins for strlen,
              strchr and memchr.
-  Eva        [2018/04/25] Renamed option -wlevel into -eva-widening-delay. New
              option -eva-widening-period to control the number of iterations
              between two widenings.
-  Eva        [2018/04/25] New propagation strategy that allows unrolling loops
              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.

#####################################
Open Source Release Chlorine-20180502
#####################################

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

#####################################
Open Source Release Chlorine-20180501
#####################################

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

###################################
Open Source Release Sulfur-20171101
###################################

-* Eva        [2017/10/27] Fix bugs when evaluating \ìnitialized, \dangling
              and \separated on addresses of bitfields
-* Eva        [2017/10/27] Fix bug in the handling of non-explicitly volatile
              fields inside volatile structs or unions
-  RTE        [2017/10/27] add option -rte-initialized to generate assertions
              over read accesses to potentially uninitialized locations.
-* RTE        [2017/10/16] Fix bounds of alarms emitted when downcasting to
              bitfields (issue #?2314)
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
              be rejected when the compiler does not support this construct,
              depending on the fields sizeof_fun and alignof_fun of the machdep
-* Kernel     [2017/10/11] More thorough checks on l-values with function type.
              Non-sensical expressions are now rejected at parsing type.
-  Eva        [2017/10/10] Uses assigns clauses to over-approximate the effects
              of assembly statements. Warns if no assigns clause is provided.
-* Eva        [2017/10/10] Fixes a performance issue in offsetmaps, that occured
              when reading or copying values smaller than cells in large arrays.
-  Eva        [2017/10/10] The backward propagation tries to reduce integer
              values by considering separately the bounds of their intervals.
-* Eva        [2017/10/10] Fixes an optimization issue where the reduction by a
              loop invariant just after widenings could impede the convergence.
-* Eva        [2017/10/10] Fixes a soundness bug where a loop invariant could be
              wrongly proved correct in some marginal cases.
+  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
              click on the header, while a left click sorts the tree.
-  Metrics    [2017/09/13] In the Gui, shows the percentage and the number of
              dead statements (when computed) for each function of the filetree.
-! Callgraph  [2017/09/01] Option -cg-init-roots replaced by -cg-service-roots
              (almost equivalent); new options -cg-function-pointers (ignore
              function pointers; unsound) and -cg-roots (compute subgraphs).
o! Eva        [2017/09/01] In abstract domains, compute_using_specification is
              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.
-  Eva        [2017/09/01] Various precision improvements in the interpretation
              of the behaviors of a specification.
-* Kernel     [2017/08/31] Fixes configure script on bytecode only architecture.
              Initial version of the patch by Debian. Fixes #2325
-* Kernel     [2017/08/31] Fix various typos in source code and user messages.
              Patch by Debian. Fixes #2323
-! Sparecode  [2017/08/31] Rename option -rm-unused-globals to
              -sparecode-rm-unused-globals.
o! ACSL       [2017/08/24] Refactor handling of logic labels in AST
-! Eva        [2017/08/03] Fix soundness (resp. precision) bug on big-endian
              (resp. little-endian) architectures. This bug triggered on
              low-level code, typically when using bitfields
-* Kernel     [2017/08/03] Strip bitfield attribute when performing integral
              promotions on bitfields of size short or char. Fixes incorrect
              attributes on the resulting expression.
-! ACSL       [2017/08/03] Explicitely disallow /* and */ in ACSL annotations.
              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)
-* Kernel     [2017/07/29] Fix unmarshalling of save files that contain more
              than 4Gb of uncompressed data. Patch from TIS-interpreter.
-* Eva        [2017/07/27] Fix performance issue with the equality domain.
-! Kernel     [2017/08/28] Fix invalid eids on code generated through loop
              unrolling
-! Slicing    [2017/08/28] Fix invalid eids on code generated through option
              -slicing-level >= 2
-! Eva        [2017/07/28] Fixed memory leak with option
              -val-subdivide-non-linear
o! Slicing    [2017/08/01] Removing Db API for Slicing plug-in. Calls to
              !Db.Slicing should be replaced by calls to Slicing.Api.
-o! Slicing   [2017/07/27] Removing deprecated '-slice-option' and related
              !Db.Slicing.Projet.print_exported_project. Minor changes into
	      !Db.Slicing.Projet.extract.
o! Scope      [2017/07/27] Removing Db API for Scope plug-in. Calls to
              !Db.Scope should be replaced by calls to Scope.
o! Report     [2017/07/24] Removing Db API for Report plug-in. Calls to
              !Db.Report.print should be replaced by calls to
              Report.Register.print.
-  RTE        [2017/07/17] Emits overflow alarms on unsigned left shift when
              -warn-unsigned-overflow is enabled.
-  Eva        [2017/07/17] Emits overflow alarms on unsigned left shift when
              -warn-unsigned-overflow is enabled.
-  Kernel     [2017/07/10] Composite types are now required to have equal tags
              as per the C standard; no more support for isomorphic structs.
-  Eva        [2017/07/01] In the GUI, the "Values" panel displays the values
              computed by using the properties inferred by all enabled domains.
-! Eva        [2017/06/30] Better handling of function alloca(), via builtin
              Frama_C_alloca.
-* Eva        [2017/06/28] The cvalue states saved after each statement are now
              properly deleted when an Eva parameter is changed in the GUI.
o  Eva        [2017/06/26] New functor in domains/simple_memory.ml to build a
              complete domain from a value abstraction. The abstract states link
              each scalar variable of a program to an abstract value.
-  Eva        [2017/06/26] New sign domain for demonstration purposes only.
-* Kernel     [2017/06/09] Parser now handle mixed concatenation of
              string and wstring. Fixes #@1467
-  Eva        [2017/06/07] The subdivision of the evaluation of non-linear
              expressions (through the -val-subdivide-non-linear option) also
              applies to the new evaluations requested by the equality domain.
-* Eva        [2017/06/14] Fix a crash when downcasting pointer values with
              the option -val-warn-signed-converted-downcast enabled.
-* 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
              is now optional, and will be removed in a later version.
*  Eva        [2017/05/24] Fix soundness bug in string builtins where some
              invalid offsets did not generate alarms.
-  Eva        [2017/05/22] Removes all effects of the special functions
              Frama_C_[dump|show]_each on the analyses: no alarms are emitted
              and the states are never reduced on these calls.
-  Eva        [2017/05/22] Frama_C_dump_each prints the state of each available
              domain whose log category is enabled.
-  Eva        [2017/05/22] New directive Frama_C_domain_show_each prints the
              internal properties about the arguments inferred by each available
              domain whose log category is enabled.
o! Eva        [2017/05/22] Abstract domains have to provide a log category and
              a function show_expr that prints the internal properties inferred
              about an expression.
-  Kernel     [2017/05/18] Added option -print-return to inline gotos to return
-  RTE        [2017/05/12] add -warn-not-finite-float for checking
              that infinite and NaN floats are not produced.
-! Kernel     [2017/05/17] qualifiers are dropped from the return type of
              functions, as they make no real sense
-* Kernel     [2017/04/27] stop removing const attribute on local variables.
              Fixes #@301
o! Kernel     [2017/04/27] Remove needless repetition of declared logic labels
              in Tapp and Papp nodes. Fixes #@274
o! Kernel     [2017/04/27] Completely separate types between Cil_types and
              Logic_ptree, removing needless polymorphism
-  Eva        [2017/04/06] More precise evaluation of \initialized and
              \dangling predicates.

#######################################
Open Source Release Phosphorus-20170501
#######################################

-* Eva        [2017/05/08] Fix widening in the gauges domain, in particular with
              nested loops and pointers that change base address through
              iterations
-* Eva        [2017/04/25] Perform widening in the symbolic locations domain.
-* Eva        [2017/04/24] Fixes a crash when backward-propagating an imprecise
              value on a 32-bits floating point addition. A non-single precision
              value was erroneously returned.
-* Eva        [2017/04/05] Fixes a crash with the -val-subdivide-non-linear
              option, on subdivisions of evaluations involving pointer values.
-! Eva        [2017/03/31] Renamed dynamic allocation builtins for
              improved consistency. In particular, Frama_C_alloc_size
              becomes Frama_C_malloc_fresh.
-  Eva        [2017/03/31] New option -val-builtins-list
-* Scope      [2017/03/31] Fix bug in the functions of Db.Scope in presence of
              alarms refering to volatile memory locations, or to variables
              that leave scope. Also impacts Eva option -remove-redundant-alarms
-  Eva        [2017/03/31] Activate option -remove-redundant-alarms by default.
-  Inout      [2017/03/28] Option -inout-callwise is now always active, and will
              be removed in a later version
-* Inout      [2017/03/28] Prevent formal variables of functions with only a
              specification from leaking into results
-  Kernel     [2017/03/28] Dynlink is now mandatory, no degraded static mode.
o! Eva        [2017/03/17] Incompatible API changes in module Cvalue.Model.
              Functions named 'unspecified' have been renamed into
              'indeterminate', and some arguments have been removed.
o! Gui        [2017/03/10] Signature change for constructor
              Pretty_source.PVDecl
-! Kernel     [2017/03/10] Explicit AST nodes to mark local variables
              initialization.
-! Kernel     [2017/03/10] Better handling of VLA (use explicit function calls
              to mark deallocation of VLA at appropriate program points)
-* 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
              now depends on all relevant options, including kernel options
              -warn-...
-! Variadic   [2017/03/08] Change of command line argument names for the
              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.
-! Value      [2017/03/07] Support for the legacy value analysis has been
              abandoned, Eva is now always active. Option -no-eva has been
              removed.
-* Eva        [2017/03/07] Unsound support for recursion, through option
              -val-ignore-recursive-calls. The support of recursion through
              the use of 'assigns' clauses, previously available in Value,
              was unsound and has been removed
-! Kernel     [2017/03/01] Zarith library is now required
-* Kernel     [2017/02/24] Fix crash when loading a saved file without a plug-in
              which has previously emitted a status with a tuning parameter.
-  Eva        [2017/02/06] New (internal) mechanism to handle C functions'
              return values. Messages now mention \result<foo> for the
              value returned by 'foo'.
-  Variadic   [2017/02/08] The plugin is now enabled by default. Use the
              option -variadic-no-translation to keep the original behaviour.
              The specification generated for the fprintf function family is
              now more accurate.
-  Kernel     [2017/01/26] New option -print-libc, to expand include directives
              for files in the Frama-C stdlib (no longer expanded by default).
-* 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
              statement contract and absence of return. See #@255 and #2235.
-  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
              types are now refused. The resulting expression is typed as
              ptrdiff_t instead of int.
-  Value      [2016/11/18] Widen hints directives @widen_hints now accept
              arbitrary l-values (evaluated at analysis time) in place of
              variables.
-* Kernel     [2016/11/17] Fixed some issues with #pragma pack() behavior,
              in both GCC and MSVC machdeps. Also fixed some related issues
              with __aligned__ and __packed__ attributes (including bts #2249).
-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
              -no-dynlink); mostly for internal use.
-! Kernel     [2016/10/19] Stricter verification for extern, static and inline
              specifiers (support for CERT DCL-36-C coding rule)
o* Eva        [2016/10/22] Functions Db.Value.fun_set_args and
              Db.Value.globals_set_initial_state are now compatible with Eva.

######################################
Open Source Release Silicon-20161101
######################################

-*! Eva       [2016/10/29] Fix soundness bug on statements with RTE or
              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.
-* Eva        [2016/10/20] Fix bug in the bitwise domain, on some applications
              of the & and | operators
-  Value      [2016/10/20] New (experimental) option -val-builtins-auto, to
              automatically replace known C functions by builtins. Will
              be set by default in Phosphorus.
-* Value      [2016/10/19] Frama_C_cos and Frama_C_sin builtins are now
              precise by default. The former Frama_C_cos / Frama_Csin_precise
              have been removed
-* Kernel     [2016/10/18] Fix bug when pretty printing an ACSL term
              "divisor / *p" (bts #2250).
-  Eva        [2016/10/18] New experimental Gauges domain, that relates
              integer variable to loop counters.
-! Kernel     [2016/10/15] Fix major bug in the backward dataflow of module
              Dataflows
-! Scope      [2016/10/15] Fix bug that might lead to unsoundness and / or
              looping in 'Datascope' functionality (#!235)
-* Eva        [2016/10/11] Prevent incorrect reductions on memory locations
              with volatile qualifier
-! Value      [2016/10/11] Option -val-warn-copy-indeterminate is now set by
              default. See command-line help if you want to deactivate it.
-  Kernel     [2016/10/07] Fix bug that may occur when modifying several times
              command line-options taking functions as argument (issue #@109)
-! Libc       [2016/10/07] Functions in share/libc.c have been inlined into
              the proper .c files under share/libc
-  Eva        [2016/10/07] More systematic backward-propagation between
              actual parameters and formals
-  Nonterm    [2016/10/05] overall increase in precision, especially on
              compound statements (if, switch, loops...). Verbosity has been
              decreased
-  Nonterm    [2016/10/05] New options -nonterm-ignore f1,..,fn (to
              ignore calls to functions f1,..,fn) and -nonterm-dead-code
              (to warn about syntactically dead code)
-  Value      [2016/09/23] Extended support for syntactic widening hints
              (@widen_hints - see the Value user manual for more details)
-  Value      [2016/09/20] New builtins for string-related functions:
              Frama_C_strlen, Frama_C_strchr, Frama_C_strnlen,
              Frama_C_memchr and Frama_C_rawmemchr
-  Value      [2016/09/20] valid_string and valid_read_string predicates
              are now evaluated by Value
-* Eva        [2016/09/18] Fix bug in equality domain, after assignements
              lv = e where the modified locations intersect those involved in
              computing lv
-* Eva        [2016/09/18] fix performance bug in the equality domain,
              especially visible on programs with many local variables.
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,
              use Format.asprintf instead.
-! Logic      [2016/08/31] Refactoring of ACSL extensions + allow extensions
              in loop annotations
-! Libc       [2016/08/29] New file share/libc/string.c, with simple
              implementations for C99 functions defined in string.h.
              Duplicate implementations were removed from share/libc.c.
-* Kernel     [2016/08/12] Fix bug #2239 about unsoundness of callgraph's
              services computation (bug introduced in Frama-C Magnesium).
o! Kernel     [2016/07/26] Suppress return_stmt field of kernel_function type.
              Use Kernel_function.find_return instead.
-* Kernel     [2016/07/31] Scripts that use Gtk can again be loaded using
              option -load-script (bug report:
              http://stackoverflow.com/questions/38677256/)
-! From       [2016/07/28] Removed options -experimental-path-deps and
              -experimental-mem-deps.
-! Value      [2016/06/26] Do not compute the sizeof of a function when
              evaluating a function call through a pointer. This avoids some
              warnings in MSVC mode.
-! Value      [2016/06/26] Option -val-show-time has been removed. Options
              -val-show-perf or -val-flamegraph offer more information
-  Value      [2016/06/26] New option -val-flamegraph, to dump information about
              analysis times as a Flamegraph
-* Value      [2016/06/26] Option -val-show-perf now properly takes into
              account the time taken by the main function itself (without its
              callees)
-! Kernel     [2016/06/14] OCamlGraph is no longer packaged within Frama-C,
              and must be installed to build Frama-C from source
o! Kernel     [2016/06/14] Remove class Filecheck.check from API.
              Use Filecheck.check_ast that provides the correct encapsulation.
-  Eva        [2016/06/11] Various improvements to experimental Apron domain
-  Value      [2016/06/11] Pointers to functions with an incompatible type are
              now handled in a more stringent manner. Previously, arguments
              with incompatibles types but equal size were reported with an
              orange status. Now, any mismatch (e.g. int/float or
              signed/unsigned) causes a red alarm.
-* Eva        [2016/06/06] Setting option -val-warn-copy-indeterminate now
              forces lvalue copies to perform a full evaluation. This includes
              converting the copied value to the proper type, and emitting
              alarms if it is indeterminate. This option should not be set
              for memcpy-like functions, or for functions that copy bits
              of pointers
-! Value      [2016/06/05] API changes in modules Lmap and Cvalue.Model. All
              occurrences of `Map in returned value should be replaced by
              `Value
-! Value      [2016/06/03] Several warnings emitted by Value are now properly
              prefixed by [value] instead of [kernel]
-  Value      [2016/05/31] New message key 'garbled-mix', to track garbled mix
              generated during the analysis
-* Value      [2016/05/30] Garbled mix created when analyzing assigns / from
              clauses are now tagged as having "Library function" origin
-  Value      [2016/05/30] New option -val-warn-on-alarms, which governs
              whether alarms are printed as warnings or text.
-* Kernel     [2016/05/23] Side-effect free instructions such as 'e;' are now
              translated as 'tmp = e;' instead of 'if (e) {}' (which was
              incorrect when e did not have a scalar type)
-  Eva        [2016/05/27] Improvements to option -val-subdivide-non-linear for
              high number of subdivisions 
-* Value      [2016/05/23] Option -val-show-initial-state has been removed.
              Instead, -value-msg-key=-initial-state can be used
-  Value      [2016/05/23] New message key final-states, that can be used
              to deactivate the printing of the abstract states at the end of
              each function
o* Kernel     [2016/05/18] Fixes merging of contract when using
              Annotations.add_code_annot
-  Rte        [2016/05/15] New option -rte-pointer-call, to generate
              annotations for calls through function pointers
-* Value      [2016/05/15] Fix crash when extracting bits of a long double
              value. (Issue 92 on TIS-interpreter, reported by ch3root.).
-  Value      [2016/05/14] Builtins are now available for malloc:
              Frama_C_alloc_size (one new base each time, may diverge) and
              Frama_C_alloc_by_stack (one base by stack, may end up performing
              weak updates).
-! Cil        [2016/05/12] Conversions between a bit-field lvalue and the
              (integral) type of the bitfield are now always made explicit
              through casts; the attribute FRAMA_C_BITFIELD_SIZE is present on
              the type of the cast if needed.
-  Libc       [2016/05/03] Implementations of some functions of the standard
              library are now available in share/libc/*.c
-* Makefile   [2016/04/27] Fix compilation of plug-ins which depends on
              another plug-ins when compiled outside Frama-C.
-  Gui        [2016/04/24] Different filters for user assertions and RTEs
              are now available.
-  Eva        [2016/04/05] Improvements to option -val-subdivide-non-linear on
              expressions such as x*x+y*y, or t[i*i].
-  Eva        [2016/04/01] Support for options -warn-signed-downcast and
              -warn-unsigned-downcast.
-! Kernel     [2016/03/31] OCaml version greater or equal than 4.02.3 required.
o  Makefile   [2016/03/31] Warnings and warn-error are activated only if a file
              .for_devel is present along side the Makefile (also for plugins)
o! Kernel     [2016/03/29] Functions Integer.pgcd and Integer.ppcm are now
              guaranteed to return a positive result.

######################################
Open Source Release Aluminium-20160502
######################################

-  Value      [2016/04/19] Support for evaluation of predicate
              \valid_read_string on constant strings.
-* Sparecode  [2016/04/11] Fix crash when an entire function becomes spare.
              (issue #@157).
-  Eva        [2016/03/30] New experimental domain that improves precision on
              bitwise operations, for example on pointers. Activated by option
              -eva-bitwise-domain.
o! Value      [2016/03/30] API change in functor Lmap.Make.
-  LoopAnalysis [2016/03/29] New plug-in 'LoopAnalysis' which estimates loop
              bounds and -slevel-function parameters. Invoked using option
              -loop.
-* ACSL       [2016/03/30] Fixes precedence uncompliance within ACSL Manual of
              some bitwise operators and more aggressive checks of consistent
              relation chains.
-* Metrics    [2016/03/24] Fix list of undefined functions; functions that
              are never called were not reported.
-* Metrics    [2016/03/24] Fix option -metrics-value-cover when option
              -metrics-libc is not set.
-! Metrics    [2016/03/24] Global variables defined in Frama-C standard library
              are no longer counted when option -metrics-libc is not set.
-  Variadic   [2016/03/17] New plug-in 'Variadic' which translates variadic
              functions, calls and macros to allow analyses to handle them more
              easily. Invoked using the -va option.
-  Nonterm    [2016/03/09] New plug-in 'nonterm' for detection of definite
              non-termination based on Value.
!o Kernel     [2016/02/29] Do not raise Invalid_arg and Failure exn but use
              custom exceptions instead. Prevents warning 52 in OCaml 4.03.0
              Functions raising new exceptions are:
              - Db.From.find_deps_term_no_transitivity_state
              - Db.Interp.*
-  Kernel     [2016/02/24] New option -<plugin>-log to copy the output of
              plug-ins into one or several text files
              (described in the User Manual).
-* ACSL       [2016/02/23] Fixes implicit logic label generation on recursive
              definitions. Fixes bug #2158.
-  Eva        [2016/02/22] Experimental domain dedicated to storing and
              learning information from syntactic equalities
              (option -eva-equality-domain).
-  Eva        [2016/02/22] Improvements to backward propagation, on memory
              accsses and bitwise operations.
-* Value      [2016/02/17] Fix handling of functions without a body that
              return a pointer. The pointer was aligned on an incorrect
              frontier.
-* Value      [2016/02/17] Fix crashes when analysing a function (without a
              body) that returns an empty struct, or a pointer to an empty
              struct. Bugs reported by TrustInSoft.
-  Kernel     [2016/02/10] Registering twice the same machdep is now accepted.
-  Cil        [2016/02/10] Add proper support for empty aggregate initializers
              in GCC mode.
-  Cil        [2016/02/08] Operator ! applied to constant expression is no
              longer simplified when not required.
-  Value      [2016/02/05] Informative messages about inactive behaviors are
              now emitted only at verbosity level 2.
-  Value      [2016/02/05] Messages on ACSL predicates with Unknown/Invalid
              status are now emitted with a 'warning' severity, consistently
              with the emission of alarms. 'True' statuses are hidden if option
              -val-show-progress is unset.
-  From       [2016/02/03] Option -from-verify-assigns takes into account
              direct and indirect dependencies.
-  Value      [2016/02/03] Distinguish direct and indirect dependencies in
              'from' clauses to compute the effecst of an 'assigns/from' clause.
              See section 7.2 of the manual.
-* Libc       [2016/02/02] Fix specifications of memchr and strncpy.
-* ACSL       [2016/01/27] Fixes example of logic label use. Fixes bug #2203.
-* Logic      [2016/01/17] Meaningless assigns clauses are now rejected more
              aggressively. Fixes bug #1790.
o  Kernel     [2016/01/08] Several incompatible changes in module Property.
-  Kernel     [2016/01/08] Automatic generation of assigns from GCC's extended
              asm.
-* Value      [2016/01/06] Evaluation of ACSL ranges takes into account option
              -safe-arrays. In particular t[..] remains within the bounds
              of t. Fixes bug #!1639.
-* Value      [2016/01/05] Take into account 'volatile' qualifiers on struct
              typedefs, which were previously ignored. Fixes issue #@102.
-  Value      [2016/01/03] Support for \valid_function predicate during
              evaluation.
-  ACSL       [2016/01/03] New predicate \valid_function, requiring the
              compatibility between the type of the pointer and the function
              being pointed.
-* Eva        [2016/01/01] Fixed some bugs related to 0. vs. -0. in conditions.
-  Eva        [2016/01/01] More aggressive reductions in complex conditions
              such as if(a+3 < 10).
-*! Value     [2016/01/01] Reimplementation of all the upper layers of the
              plugin. Compatibility with the legacy version is almost complete,
              save for some text messages and a few functions of the API.
              Use option -no-eva to switch back to the legacy version.
              Changelog entries labelled 'Eva' refer to this new version.
              Entries labelled 'Value' apply to both versions.
o! Value      [2015/12/02] Base.base_max_offset has been removed. Part of its
              functionality is still available via Base.valid_range, whose
              return type is now more expressive.
-* RTE        [2015/12/09] Fix unsoundness for overflows on binary operations
              when one or two operands were constant.
-* RTE        [2015/12/09] Fix unsoundness on unary minus expressions when
              option -rte-trivial-annotations is active.
-! Cil        [2015/12/02] Changes in the handling of incomplete structs and
              zero-length arrays. Initialization of incomplete (completely
              undefined) structs is now duly rejected. Several compiler
              extensions to the C99 standard (empty initializers,
              zero-length arrays, etc.) now require a GCC or MSVC machdep
              (e.g. -machdep gcc_x86_32).
-! Cil        [2015/12/02] Better handling of C99 flexible array members (FAMs).
              Static initialization of FAMs (a GCC extension) is no longer
              supported.
o! Gui        [2015/12/01] Refactor GUI Helpers.
              (Toolbox and (partially) Gtk_helper moved
              to Wutil,Widget, Wform, Wtext and Wtable).
-! Value      [2015/11/26] Widening hints now includes signed and unsigned
              limits for the bitsize of the value being widened, but does not
              include arbitrary limits anymore. The convergence is generally
              faster but results may be more or less precises depending on
              the case.
-! Value      [2015/11/26] Better propagation strategy for nested loops.
              Results are usually much more predictable (and often more
              precise) when the loops are not fully unrolled by slevel.
-! Makefile   [2015/11/26] Target 'make rebuild' has been renamed into
              'make clean-rebuild'.
-* Value      [2015/11/24] The preconditions of functions overridden by builtins
              no longer receive an 'Unreachable status for calls within dead
              code: the specification is ignored everywhere. Fixes bug #!1956.
-! Cil        [2015/11/23] Incorrect return statements (return void on non-void
              functions and vice-versa) now generate errors instead of warnings.
-  Value      [2015/11/23] New option -val-warn-undefined-pointer-comparison.
-  ACSL       [2015/11/23] Add built-in operators for lists.
-  ACSL       [2015/11/23] Add notation '{ x, y, z }' for defining sets.
o  Makefile   [2015/11/19] New option PLUGIN_EXTRA_DIRS for multi-dir plugins.
-* Kernel     [2015/11/18] do not crash when loading statuses depending from
              non existing parameter. Fixes issue #!2181.
o! Makefile   [2015/11/12] Get rid of FRAMAC_MAKE variable. Use FRAMAC_INTERNAL
              instead for distinguishing internal and external mode.
-  Kernel     [2015/10/28] Option -collect-messages is obsolete and will be
              removed in a future version; messages are now always collected.
o! Kernel     [2015/10/19] Removed function State_selection.list_state_union.
              Use State_selection.of_list or State_selection.list_union instead.
-* Kernel     [2015/10/15] Avoid comment duplications on generated code.
-* Kernel     [2015/10/15] Comments are preserved even when loops are unrolled.
              Fixes issue #!2176.
-! Kernel     [2015/10/15] Option -warn-undeclared-callee changed to
              -implicit-function-declaration, which receives an argument
              (ignore, warn or error) specifying what to do when an undeclared
              function is called.
-! GUI        [2015/10/15] Signature change for function
              Design.register_source_highlighter; the first argument of the
              callback has now type Design.reactive_buffer, which can be coerced
              back to a GSourceView2.source_buffer using method buffer.
-  Value      [2015/10/13] During the evaluation of  ACSL 'assert', intermediate
              statuses (e.g. True, then Unknown, then True) are now reported
              in the console.
o! Kernel     [2015/12/09] API change for function Alarms.register. See .mli
              for details.
-  Cil        [2015/10/09] Add support for parsing digraphs.
o! Cil        [2015/10/09] Buggy record Cil.miscState has been removed.
              Customization must be done directly in Cil_printer.state.
-  Value      [2015/09/30] Better precision for calls through function pointers
              when multiple functions are possible. The abstract state now
              contains the information of which function was called.
o! Value      [2015/09/20] Functions filter_le_ge_lt_gt_* have been renamed
              into backward_comp_*. Evaluation and reduction functions
              for comparisons now use and return dedicated types, in
              Abstract_interp.Comp.
-  Cil        [2015/09/20] Double pointer casts on the NULL pointer are now
              simplified.
-! Cil        [2015/09/20] Typing within comparisons is now more strict,
              or made more explicit through casts.
-  Kernel     [2015/09/20] The untyped AST is no longer removed by basic program
              transformations such as loop unrolling.
o  Ptests     [2015/07/29] New EXEC: directive.
-  Kernel     [2015/07/01] New options -then-last and -then-replace.
-  Kernel     [2015/07/01] New option -remove-projects.
-  Kernel     [2015/06/30] New option -set-project-as-default.

######################################
Open Source Release Magnesium-20151002
######################################

o! Kernel     [2016/01/03] Modules Dataflow is deprecated, and will be removed
              in Aluminium. Module Dataflow2 offers a very similar but simpler
              API.
-  Doc        [2015/11/16] Fixed typo in the manual (Thx Mihaela Sighireanu).
-* Kernel     [2015/10/12] Fix clearing of old statuses and hypotheses when a
              new status is emitted or an annotation is removed.
-* Libc       [2015/09/29] Removed obsolete file machine.h (along with other
              similar files) from the Frama-C share folder. Fixes bug #2171
-! Kernel     [2015/09/07] Removed support for OCaml 3.12.1
-  Value      [2015/09/03] Assertions containing \at(P, L), where L is a C
              label, can now be evaluated. Evaluation is done once Value has
               run; thus, it ignores option -slevel.
-* Value      [2015/09/03] pointer_comparable alarms are now emitted with
              arguments properly cast to void* or void (*)().
-  Value      [2015/08/10] The alarms raised when evaluating a global
              initializer that leads to an undefined behavior are now marked
              with an "Invalid" status.
-  Report     [2015/08/10] Reports in csv format now honor option
              -report-specialized (previously, preconditions at a
              callsite were always skipped).
-* Libc       [2015/08/26] Fix bug in the specifications of readir, opendir,
              closedir and fopen functions, that would cause incorrect analysis
              in -lib-entry-mode.
-  Gui        [2015/08/14] When a call statement is selected, the statuses of
              the preconditions of the called functions are displayed in the
              'information' panel.
o! Gui        [2015/08/14] Minor API changes regarding Design.reactive_buffer.
              Some values that used to have an option type are now guaranteed
              to be present.
-  Gui        [2015/08/12] Internal ids (for statements, code annotations, etc.)
              are now hidden by default. Start the GUI in debug mode if you want
              to see them.
-* Gui        [2015/08/10] Filenames in the GUI file tree (top-left panel)
              are now sorted correctly. Fixes bug #2173.
-! Value      [2015/08/03] WIDEN_HINTS directive are now cumulative with
              automatically inferred bounds. Fixes bug #876.
-* Cil        [2015/08/03] Fix bug #1553, related to nested initialisations
              of structures containing pointers.
-! Value      [2015/08/03] All plugins that depend on Value, plus Value itself
              are now dynamic. Custom plugins must specify in their Makefile the
              plugins they depend on (e.g. PLUGIN_DEPENDENCIES:=Inout Value).
-* Cil        [2015/07/29] Cil transformation can introduce assertion to ensure
              that size expressions in an array declarations evaluated at
              program execution time are positive and do not overflow.
o  Ptests     [2015/07/29] New LOG: directive.
-  Value      [2015/07/19] Garbled mix origins now include at most one source
              location.
-  Report     [2015/07/19] New option -report-proven to control the display
              of proven properties.
-  Report     [2015/07/19] New export format (.csv), through option -report-csv.
o! Callgraph  [2015/07/16] Remove Cil.Callgraph, Db.Syntactic_callgraph and
              Db.Semantic_callgraph which are all replaced by the single
              plug-in Callgraph. See Changelog_detailled.md for further detail
              about this change.
-! Callgraph  [2015/07/16] New plug-in callgraph which merges the old
              Syntactic_callgraph and Semantic_callgraph plug-ins (now
              removed). Either this plug-in uses Value if already computed, or
              computes the syntactic callgraph otherwise. This new plug-in
              unifies the behavior of its two ancestors. In particular,
              the edges of callgraph computed with the help of Value are
              now directed in the same way as the syntactic callgraph (was
              reversed before) and so the computed services are now
              equivalent. Also, the uncalled functions are now displayed
              by default. For plug-in developers, the callgraph is easily
              accessible via an API (bts #755).
-! Value      [2015/07/14] Float operations that are guaranteed to lead
              to +/-infty (e.g. x = FLT_MAX*10.) now stop propagation.
              Previous behavior was to continue with an imprecise value for x.
-  Kernel     [2015-07-09] New option -custom-char-annot for changing the
              character introducing ACSL annotations (instead of '@').
-  Value      [2015/07/09] Do not emit pointer_comparable alarms on valid
              pointer comparisons involving objects of size 0.
-  Value      [2015/07/07] The semantics of copying a lvalue has been changed
              when a type mismatch occurs between the destination and the copied
              value. A bitwise reinterpretation of the value to the destination
              type is now performed during the copy.
o! Kernel     [2015/07/01] Ival.Float_abstract renamed to Fval.
              Fval.inject_r now may raise Fval.Non_finite instead of the old
              Float_abstract.Bottom.
-  Value      [2015/06/29] Option -val-split-return-auto now always split
              between NULL/non-NULL pointers.
-* Value      [2015/06/26] Check the validity of the operands of the ACSL
              operators /, %, << and >> when evaluating a predicate.
o! Value      [2015/06/25] Remove duplicate values Ival.singleton_zero and
              Ival.singleton_one. Use script sodium2magnesium.sh for automatic
              migration.
-*  Parsing   [2015/06/22] Black-list gcc's builtin macros for logic
              pre-processing to avoid warnings for duplication. Fixes bug #2161.
-*  Logic     [2015/06/15] Fix typing bug when converting into a term an
              expression containing a pointer subtraction.
-* Value      [2015/06/09] Pointer comparisons using relational operators (<,
              >=, etc) between a pointer and NULL is now flagged as undefined.
o! Kernel     [2015/06/09] Remove support of plug-ins without .mli.
              Fixes bug #!1825.
-*  Cil       [2015/05/29] Better typing of '?' operator. Fixes bug #2117.
o! Kernel     [2015/05/29] Remove long-obsoleted functions Cfg.computeCFGInfo
              Cfg.printCfgFilename, and Cfg.printCfgChannel.
-  Value      [2015/05/28] Functions call using a function pointer are now
              treated more leniently when too many arguments are supplied. An
              alarm is emitted, but execution continues with the right number
              of arguments.
-  Value      [2015/05/12] Improved reduction by predicate \initialized when
              the left argument is a range of locations.
-  Impact     [2015/05/12] Removed function Db.Impact.slice, that was actually
              unrelated to Impact. You can use the functions contained in
              Db.Slicing.Select, in particular Db.Slicing.Select.select_stmt,
              to obtain the same result.
-  Makefile   [2015/05/06] Dynamic plug-ins are now declared as Findlib
              packages. Use variables PLUGIN_REQUIRES and PLUGIN_DEPENDENCIES.
              Loading a plug-in automatically loads all necessary dependencies.
              Plugin "MyPlugin" is register under "frama-c-myplugin" package.