-
Augustin Lemesle authoredAugustin Lemesle authored
changelog.html 297.63 KiB
---
layout: changelog
title: Changelog
css: changelog
---
<h3 class="release">Future Release <span class="hversion">[svn]</span></h3>
<div class="release">
<h2>Frama-C General</h2>
<ul class="entries">
<li class="dev-break"><span class="kernel">[Kernel]</span>  removes AST constructors TCoerce, TCoerceE, PLCoercion, PLCoercionE, Psubtype and PLsubtype</li>
<li class="bugfix"><span class="kernel">[Kernel]</span>  fixes dangling ref when removing unused static local<br/><br/></li>
</ul>
</div>
<hr><div><a id="Potassium-19.0" href="#Potassium-19.0"></a></div><h3 class="release">Potassium Release <span class="hversion">[19.0]</span></h3>
<div class="release">
<h2>Frama-C General</h2>
<h4>New Features</h4>
<ul class="entries">
<li class="user"><span class="kernel">[ACSL]</span>  Clarifies which C variables are in scope under a <tt>\at</tt>(·,L) (<a class="private" href="https://git.frama-c.com/frama-c/frama-c/issues/575">#575</a>)</li>
<li class="user"><span class="kernel">[ACSL]</span>  Add check annotation, similar to assert except that it does not introduce additional hypotheses on the program state</li>
<li class="user-break"><span class="kernel">[Kernel]</span>  Improved precision of integer abstract bitwise operators.</li>
<li class="user-break"><span class="kernel">[Kernel]</span>  Add statement attributes (sattr) to the AST. They are not printed by default, use <tt>-kernel-msg-key</tt> printer:attrs</li>
<li class="user"><span class="kernel">[Kernel]</span>  Add attributes for loop statements to allow distinguishing between for, while and dowhile loops.</li>
<li class="user"><span class="kernel">[Libc]</span>  Ask clang not to warn about unknown FRAMA_C_MODEL attribute when pre-processing frama-c's libc</li>
<li class="user"><span class="kernel">[Libc]</span>  Better specs and removal of half-implemented ifdef that tried to take various POSIX versions into account</li>
</ul>
<h4>Bug Fixes</h4>
<ul class="entries">
<li class="bugfix"><span class="kernel">[ACSL]</span>  Accept C identifiers that happen to be ACSL keywords in volatile and reads clauses</li>
<li class="bugfix"><span class="kernel">[Kernel]</span>  Fixes <a class="private" href="https://git.frama-c.com/frama-c/frama-c/issues/553">#553</a> - pretty-printing of basic asm template<br/><br/></li>
<li class="bugfix"><span class="kernel">[Kernel]</span>  Fixes AST integrity check wrt volatile accesses</li>
<li class="bugfix"><span class="kernel">[Kernel]</span>  Better detection of invalid goto in presence of VLA (fixes <a class="private" href="https://git.frama-c.com/frama-c/frama-c/issues/499">#499</a>)</li>
<li class="bugfix"><span class="kernel">[Kernel]</span>  Avoid crashing on one-letter attributes. Fixes <a class="public" href="http://bts.frama-c.com/view.php?id=2432">#2432</a></li>
<li class="bugfix"><span class="kernel">[Makefile]</span>  Do not attempt to install .cmx on bytecode-only architectures. Patch by M. Dogguy backported from Debian package</li>
</ul>
<h4>Developers Only</h4>
<ul class="entries">
<li class="dev"><span class="kernel">[Kernel]</span>  New functions for retrieving major and minor version</li>
<li class="dev"><span class="kernel">[Kernel]</span>  Integer API moving closer to Zarith</li>
<li class="dev"><span class="kernel">[Kernel]</span>  When registering extended ACSL annotations, one must now indicate whether they should have a status.</li>
</ul>
<h2>Frama-C GUI</h2>
<ul class="entries">
<li class="user"><span class="kernel">[Gui]</span>  Compatibility with lablgtk3 and improved handling of some widgets</li>
</ul>
<h2>Plugin Aorai</h2>
<ul class="entries">
<li class="bugfix"> Fixes <a class="private" href="https://git.frama-c.com/frama-c/frama-c/issues/586">#586</a>: avoid removing the initial state of the automaton</li>
</ul>
<h2>Plugin Eva</h2>
<h4>New Features</h4>
<ul class="entries">
<li class="user"> Improved precision on nested loops (by postponing the widening on inner loops according to <tt>-eva-widening-period</tt>).</li>
<li class="user"> Ignore annotations with <tt>"no_eva"</tt> tag</li>
<li class="user"> New warning category for detecting loops without 'unroll' directive</li>
<li class="user"> New option <tt>-eva-precision</tt> 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.</li>
<li class="user"> 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 <tt>-eva-msg-key</tt>=<tt>-summary</tt></li>
<li class="user"> Loop unroll annotations now accept non-constant but bounded expressions as the maximum number of unrollings to perform.</li>
<li class="user"> New option <tt>-eva-partition-history</tt> 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.</li>
<li class="user"> 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 <tt>-eva-partition-value</tt> exp.</li>
</ul>
<h4>Bug Fix</h4>
<ul class="entries">
<li class="bugfix"> Fixes <tt>-eva-split-return</tt> on uninitialized or escaping function returns when <tt>-eva-warn-copy-indeterminate</tt> is disabled.</li>
</ul>
<h2>Plugin Inout</h2>
<ul class="entries">
<li class="user"> Fix performance issue when initializing large arrays.</li>
<li class="bugfix"> Fixes operational input on const local initialization</li>