Retroactively updates the Changelog with major Eva changes for Potassium.

Changelog

@@ -21,9 +21,28 @@ Open Source Release <next-release>
 Open Source Release 19.0 (Potassium)
 ####################################
 
+-   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