diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 5c9bcd612f28b2c78c02ece2b341c35ceb6ef2f3..6fb7a3700d6078cc72fadbde2dc43cf92c43a17c 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -15,15 +15,17 @@ before_script: - ruby -v # Print out ruby version for debugging - gem install bundler -v '2.0.2' - bundle install -j $(nproc) --path vendor +- cd generator +- chmod +x ./generate +- curl https://git.frama-c.com/api/v4/projects/780/repository/files/Changelog/raw?ref=master > ../assets/Changelog +- curl https://git.frama-c.com/api/v4/projects/780/repository/files/src%2Fplugins%2Fe-acsl%2Fdoc%2FChangelog/raw?ref=master >> ../assets/Changelog +- curl https://git.frama-c.com/api/v4/projects/780/repository/files/src%2Fplugins%2Fwp%2FChangelog/raw?ref=master >> ../assets/Changelog +- ./generate ../assets/Changelog -o ../html/changelog.html +- cd .. test: stage: test script: - - cd generator - - chmod +x ./generate - - curl https://git.frama-c.com/api/v4/projects/780/repository/files/Changelog/raw?ref=master > ../assets/Changelog - - ./generate ../assets/Changelog -o ../html/changelog.html - - cd .. - bundle exec jekyll build -d test --future artifacts: paths: @@ -37,11 +39,6 @@ test: pages: stage: deploy script: - - cd generator - - chmod +x ./generate - - curl https://git.frama-c.com/api/v4/projects/780/repository/files/Changelog/raw?ref=master > ../assets/Changelog - - ./generate ../assets/Changelog -o ../html/changelog.html - - cd .. - bundle exec jekyll build -d public --future artifacts: paths: diff --git a/generator/changelog.html b/generator/changelog.html deleted file mode 100755 index 28edb6c4191b06bd4988faa9096caa0f008d505f..0000000000000000000000000000000000000000 --- a/generator/changelog.html +++ /dev/null @@ -1,3058 +0,0 @@ ---- -layout: changelog ---- -<h3 class="release">Future Release <span class="hversion">[git]</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> -</ul> -<h2>Plugin Obfuscator</h2> -<ul class="entries"> -<li class="bugfix"> Also obfuscate formals in function pointer types. Fixes <a class="public" href="http://bts.frama-c.com/view.php?id=2433">#2433</a>.</li> -<li class="bugfix"> Obfuscate logic types and logic constructors.</li> -</ul> -<h2>Plugin RTE</h2> -<ul class="entries"> -<li class="bugfix"> fixes a crash when visiting variable declarations</li> -<li class="dev"> RTE has a static API</li> -</ul> -</div> -<hr><div><a id="Argon-18.0" href="#Argon-18.0"></a></div><h3 class="release">Argon Release <span class="hversion">[18.0]</span></h3> - -<div class="release"> -<h2>Frama-C General</h2> -<h4>New Features</h4> -<ul class="entries"> -<li class="user-break"><span class="kernel">[ACSL]</span>  Introduce extensions to global annotations and better characterization of each extension kind. See development guide for more information</li> -<li class="user"><span class="kernel">[Kernel]</span>  New option <tt>-remove-inlined</tt> to remove function(s) after <tt>-inline-calls</tt>, add category @inline to refer to all functions with inline attribute (for both options).</li> -<li class="user"><span class="kernel">[Kernel]</span>  Fix compilation on OpenBSD patch contributed by madroach. Fixes <a class="public" href="http://bts.frama-c.com/view.php?id=2379">#2379</a></li> -<li class="user-break"><span class="kernel">[Kernel]</span>  Remove option <tt>-const-writable</tt>: const globals are unconditionally constants</li> -<li class="user-break"><span class="kernel">[Kernel]</span>  Introduce Filepath dataype for more consistent normalization of filenames</li> -<li class="user"><span class="kernel">[Kernel]</span>  New options <tt>-warn-left-shift-negative</tt> (enabled by default) and <tt>-warn-right-shift-negative</tt> (disabled by default), to control the emission of alarms on shifts on negative integers.</li> -<li class="user"><span class="kernel">[Kernel]</span>  New warning (disabled by default) when multiple side effects are unsequenced (CERT-EXP10<tt>-C</tt> recommandation). Fixes <a class="private" href="https://git.frama-c.com/frama-c/frama-c/issues/492">#492</a></li> -<li class="user"><span class="kernel">[Kernel]</span>  New option <tt>-warn-invalid-bool</tt>, to warn when reading trap representations of type _Bool.</li> -<li class="user"><span class="kernel">[Kernel]</span>  More ergonomic command-line options for governing warning categories statuses.</li> -<li class="user-break"><span class="kernel">[Kernel]</span>  <tt>Log.error</tt> and <tt>Log.failure</tt> will eventually make Frama-C exit with a non-zero status. Fixes <a class="private" href="https://git.frama-c.com/frama-c/frama-c/issues/552">#552</a></li> -</ul> -<h4>Bug Fixes</h4> -<ul class="entries"> -<li class="bug-break"><span class="kernel">[ACSL]</span>  introduce ACSL operators <tt>\le_double</tt>, <tt>\ge_double</tt>, ... in addition to <tt>\le_float</tt>, <tt>\ge_float</tt>, ... Remove overloading of <tt>\le_float</tt> that made it accept double as arguments. Fixes <a class="private" href="https://git.frama-c.com/frama-c/frama-c/issues/502">#502</a></li> -<li class="bugfix"><span class="kernel">[ACSL]</span>  Avoid removing cast of void ptr used as argument of function expecting a ptr with known size. Fixes <a class="private" href="https://git.frama-c.com/frama-c/frama-c/issues/432">#432</a></li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Respect relative order of labels and ACSL annots. Fixes <a class="private" href="https://git.frama-c.com/frama-c/frama-c/issues/524">#524</a></li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Do not allow compound assignments to const variables Fixes <a class="private" href="https://git.frama-c.com/frama-c/frama-c/issues/384">#384</a></li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Add attribute to allow writing into const lvals in specific (aka C++ constructors and mutable fields) circumstances. Fixes <a class="public" href="http://bts.frama-c.com/view.php?id=2395">#2395</a>.</li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Rejects sizeof of an incomplete type. Fixes <a class="private" href="https://git.frama-c.com/frama-c/frama-c/issues/560">#560</a>.</li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Consider that asm can change content of pointers used as inputs when generating assigns clauses. Fixes <a class="private" href="https://git.frama-c.com/frama-c/frama-c/issues/458">#458</a></li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Fixes parsing of compound initializers with anonymous fields. Fixes <a class="public" href="http://bts.frama-c.com/view.php?id=2384">#2384</a></li> -</ul> -<h4>Developers Only</h4> -<ul class="entries"> -<li class="dev-break"><span class="kernel">[Kernel]</span>  Remove completely outdated module Dataflow. Deprecated since 3+ years. Use Dataflow2 instead.</li> -<li class="dev"><span class="kernel">[Ptests]</span>  Do not keep oracles for empty stderr. Fixes <a class="private" href="https://git.frama-c.com/frama-c/frama-c/issues/402">#402</a></li> -</ul> -<h2>Plugin Constant</h2> -<ul class="entries"> -<li class="dev-break"> Propagation Removing Db API for Constant Propagation plug-in. Calls to <tt>!Db.Constant_Propagation</tt> should be replaced by calls to <tt>Constant_Propagation.Api</tt>.</li> -</ul> -<h2>Plugin Eva</h2> -<h4>New Features</h4> -<ul class="entries"> -<li class="user"> New propagation strategy that allows unrolling loops even when the slevel has been exceeded. Unroll the N first loop iterations via the global option <tt>-eva-min-loop-unrolling</tt> N or via specific code annotations /*@ loop unroll N; */. The new strategy may affect analyses even without loop unrolling.<br/><br/></li> -<li class="user"> Renamed option <tt>-wlevel</tt> into <tt>-eva-widening-delay</tt>. New option <tt>-eva-widening-period</tt> to control the number of iterations between two widenings.</li> -<li class="user"> Improved precision of string builtins for strlen, strchr and memchr.</li> -<li class="user"> The variables from the frama-c libc are no longer shown in the initial state print.</li> -<li class="user"> When a cvalue builtin is used, other domains use the frama-c libc specification to interpret the call without losing too much information.</li> -<li class="user"> Release all builtins, including memset and memcpy, as open-source.</li> -<li class="user"> New option <tt>-eva-report-red-statuses</tt> listing in a csv file the properties invalid for some states of the analysis (as in the <tt>"Red Alarms"</tt> panel of the GUI).</li> -<li class="user"> The debug category <tt>"garbled-mix"</tt> becomes a warning category. Better track of garbled mix created by specification.</li> -<li class="user-break"> 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.</li> -<li class="user"> All options of Eva start with <tt>-eva</tt>. Aliases to previous option names preserve backward compatibility.</li> -<li class="user"> Fixes the alarms on subtractions and comparisons of pointers on weak bases (created by allocations in loops).</li> -<li class="user"> Supports the ACSL functions <tt>\min</tt> and <tt>\max</tt>.</li> -<li class="user"> Better reduction of floating-point values cast into integer types when an alarm is emitted.</li> -<li class="user"> Reduction of values leading to division by zero alarms, when possible.</li> -<li class="user"> Remove option <tt>-val-warn-left-shift-negative</tt>, and comply with kernel option <tt>-warn-</tt>[left|right]<tt>-shift-negative</tt>.</li> -<li class="user"> Some fixes and improvements of the equality domain.</li> -<li class="user"> Fix the gauges domain on weak bases.</li> -<li class="user"> Warn about currently unsupported specifications of some libc functions.</li> -<li class="user"> ACSL predicates with a <tt>"no_eva"</tt> tag are now ignored.</li> -<li class="user"> Remove option <tt>-obviously-terminates</tt>.</li> -<li class="user"> New experimental domain <tt>"numerors"</tt> inferring absolute and relative errors of floating-point computations. Enabled by the option <tt>-eva-numerors-domain</tt>. Does not handle loops for now.</li> -<li class="user"> The memexec cache is now fully compatible with all abstract domains provided by Eva. However, the binding to the Apron domains disable memexec.</li> -<li class="user"> Improved performances when the symbolic locations domain and the memexec cache are enabled.</li> -<li class="user"> Enable the memexec cache by default. It can be disabled by option <tt>-eva-no-memexec</tt>.</li> -</ul> -<h4>Bug Fix</h4> -<ul class="entries"> -<li class="bugfix"> Deprecate option <tt>-val-warn-builtin-override</tt> in favor of warning category builtins:override.</li> -</ul> -<h2>Plugin Metrics</h2> -<ul class="entries"> -<li class="user"> Add option <tt>-metrics-used-files</tt>, to help identify unnecessary files given in the command line</li> -</ul> -<h2>Plugin RTE</h2> -<ul class="entries"> -<li class="user"> Remove option <tt>-rte-precond</tt>.</li> -<li class="bugfix"> Stop generating spurious <tt>\initialized</tt> alarms. Fixes <a class="private" href="https://git.frama-c.com/frama-c/frama-c/issues/429">#429</a> </li> -</ul> -</div> -<hr><div><a id="Chlorine-17.1" href="#Chlorine-17.1"></a></div><h3 class="release">Chlorine Release <span class="hversion">[17.1]</span></h3> - -<div class="release"> -<h2>Frama-C General</h2> -<ul class="entries"> -<li class="user"><span class="kernel">[Libc]</span>  Fix C++ compatibility for Frama-Clang plug-in<br/><br/></li> -</ul> -</div> -<hr><div><a id="Chlorine-17.0" href="#Chlorine-17.0"></a></div><h3 class="release">Chlorine Release <span class="hversion">[17.0]</span></h3> - -<div class="release"> -<h2>Frama-C General</h2> -<h4>New Features</h4> -<ul class="entries"> -<li class="user"><span class="kernel">[Kernel]</span>  Make some typechecking warnings controllable with <tt>-kernel-msg-key</tt> keys.</li> -<li class="user-break"><span class="kernel">[Kernel]</span>  Option <tt>-warn-not-finite-float</tt> renamed into <tt>-warn-special-float</tt> and extended (accepts <tt>non-finite/nan/none</tt>).</li> -<li class="user-break"><span class="kernel">[Kernel]</span>  Alarms Logic_memory_access and Valid_string, that were only emitted by Eva builtins, are removed.</li> -<li class="user"><span class="kernel">[Kernel]</span>  Added option <tt>-json-compilation-database</tt> to help with preprocessing. Requires yojson during Frama-C compilation.</li> -<li class="user"><span class="kernel">[Kernel]</span>  Better renaming of variables in case of name collision.</li> -<li class="user-break"><span class="kernel">[Kernel]</span>  introduce warning categories, with various possible behaviors. Refactor management of debug categories</li> -<li class="user"><span class="kernel">[Kernel]</span>  deprecate option <tt>-continue-annot-error</tt> in favor of warning category annot-error</li> -<li class="user"><span class="kernel">[Kernel]</span>  More possible statuses for warning categories. Fixes <a class="private" href="https://git.frama-c.com/frama-c/frama-c/issues/486">#486</a></li> -<li class="user"><span class="kernel">[Kernel]</span>  Deprecate option <tt>-warn-decimal-float</tt> in favor of warning category parser:decimal-float</li> -<li class="user"><span class="kernel">[Kernel]</span>  Added option <tt>-inline-calls</tt> for syntactic inlining</li> -<li class="user"><span class="kernel">[Logic]</span>  Ghost code now supports /@ ... @/ annotations</li> -<li class="user"><span class="kernel">[Typing]</span>  Support for CERT EXP46<tt>-C</tt></li> -</ul> -<h4>Bug Fixes</h4> -<ul class="entries"> -<li class="bugfix"><span class="kernel">[ACSL]</span>  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.</li> -<li class="bugfix"><span class="kernel">[ACSL]</span>  Reinforce rejection of void* pointer types in the arguments of ACSL built-in constructs related to memory blocks and pointer dereferencing.</li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Clean up typechecking environment when dropping side-effects (in sizeof et al.). Fixes <a class="private" href="https://git.frama-c.com/frama-c/frama-c/issues/430">#430</a></li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Handle anonymous <tt>struct/union</tt> init. Fixes <a class="private" href="https://git.frama-c.com/frama-c/frama-c/issues/376">#376</a></li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Avoid crash when re-declaring a function with formals after it has been called without any. Fixes <a class="private" href="https://git.frama-c.com/frama-c/frama-c/issues/454">#454</a></li> -<li class="bugfix"><span class="kernel">[Typing]</span>  Stronger checks <tt>w.r</tt>.t. implicit conversions in function pointers (must have compatible types) and assignments (modifiable lvalues). Fixes <a class="private" href="https://git.frama-c.com/frama-c/frama-c/issues/479">#479</a></li> -</ul> -<h4>Developers Only</h4> -<ul class="entries"> -<li class="dev-break"><span class="kernel">[Kernel]</span>  Old <tt>Cil.isCharType</tt> renamed as <tt>Cil.isAnyCharType</tt>. New <tt>Cil.isCharType</tt> is now only true for plain char, neither signed nor unsigned. Derived functions (isCharPtr et al.) also updated</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  Keep information about syntactic scope of local static variables. Accessed through <tt>Globals.Syntactic_search.find_in_scope</tt>.</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  Never or rarely used Log functions have been removed or deprecated</li> -<li class="dev"><span class="kernel">[Kernel]</span>  Change <tt>Cil.typeHasAttributeDeep</tt> into <tt>Cil.typeHasAttributeMemoryBlock</tt>. Fixes <a class="private" href="https://git.frama-c.com/frama-c/frama-c/issues/489">#489</a></li> -<li class="dev"><span class="kernel">[Lib]</span>  New Rich_text module to create message with tags</li> -<li class="dev"><span class="kernel">[Logic]</span>  properly reset logic environment in case of typing errors. Fixes <a class="private" href="https://git.frama-c.com/frama-c/frama-c/issues/326">#326</a></li> -</ul> -<h2>Frama-C GUI</h2> -<ul class="entries"> -<li class="user"><span class="kernel">[Gui]</span>  Added Preferences menu (shortcut: Ctrl+P) to set themes for property bullets and external source editor</li> -<li class="user"><span class="kernel">[Gui]</span>  The preconditions of a function call can now be displayed before the call statement itself (click on status bullets with '+' or '-' to <tt>unfold/fold</tt> them)</li> -</ul> -<h2>Plugin Eva</h2> -<h4>New Features</h4> -<ul class="entries"> -<li class="user"> New panel <tt>"Red alarms"</tt> 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.</li> -<li class="user"> Various improvements in the handling of floating-point variables: evaluation of <tt>\is_finite</tt>, computation of the bits of a floating-point range, etc</li> -<li class="user-break"> In the log, messages on preconditions are now reported with the location of the call site.</li> -<li class="user"> New builtins for the single-precision mathematical functions fmodf, cosf, sinf and atan2f.</li> -<li class="user"> New option <tt>-val-skip-stdlib-specs</tt>, set by default. When analyzing the body of a function from Frama-C's standard library, specifications will be skipped.</li> -<li class="user"> Eva complies with option <tt>-warn-special-float</tt>, and propagates or warns on NaN and infinite values accordingly.</li> -<li class="user"> Fix a crash when using <tt>-val-stop-at-nth-alarm</tt>.</li> -<li class="user"> Evaluate the preconditions of the functions for which a builtin is used; builtins do not emit alarms anymore.</li> -<li class="user"> The Simple_memory functor lets builtins interpret C functions from the value of arguments to the result value.</li> -<li class="user"> New function post_analysis in abstract domains, called at the end of the analysis.</li> -<li class="user-break"> Renamed option <tt>-val-malloc-returns-null</tt> to <tt>-val-alloc-returns-null</tt>, which also applies to realloc builtins.</li> -<li class="user"> The subdivision of evaluations (through the option <tt>-val-subdivide-non-linear</tt>) can subdivide the values of several lvalues simultaneously (on expressions such as x*x - 2*x*y + y*y).</li> -<li class="user"> Warn about unsupported allocates clauses.</li> -<li class="user"> By default, do not emit pointer_comparable alarms for non pointer operations. Always compute {{ "{" }}0;1} for non pointer comparisons involving incomparable addresses.</li> -<li class="user"> Shifts of addresses now create garbled mixes (as any other arithmetic operation).</li> -<li class="user"> Removed *_alloced_return base created for functions without body that return pointers. Such bases were imprecise and could be unsound in corner cases.</li> -<li class="user"> 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).</li> -<li class="user"> Equalities can be propagated through function calls. New options <tt>-eva-equality-through-calls</tt>[<tt>-function</tt>] to decide (globally or by function) which ones are kept from the caller.</li> -<li class="user"> deprecate option <tt>-val-warn-on-alarms</tt> in favor of warning category alarm</li> -<li class="user"> Fix a soundness bug in the equality domain: do not infer incorrect equalities between incomparable pointers, or between -0. and +0.</li> -<li class="user"> Avoid enumeration on values with too many bases — fixes a performance issue.</li> -<li class="user"> In the logic, interpret the ACSL function <tt>\sign</tt> and the constructors <tt>\Positive</tt> and <tt>\Negative</tt>.</li> -<li class="user"> Fix the initialization of local volatile variables, which can always have any value.</li> -<li class="user"> Initialization of volatile pointers now keeps the base addresses of the pointer (with arbitrary offsets).</li> -<li class="user"> Interpret the logic constants <tt>\pi</tt> and <tt>\e</tt>.</li> -<li class="user"> Added scripts and templates to help automate case studies (in $<tt>FRAMAC_SHARE/analysis-scripts</tt>)</li> -</ul> -<h4>Bug Fixes</h4> -<ul class="entries"> -<li class="bugfix"> Fix bug in the handling of non-explicitly volatile fields inside volatile structs or unions<br/><br/></li> -<li class="bugfix"> Fix bugs in builtins for cos and sin. The results may be less precise than previously</li> -</ul> -<h4>Developers Only</h4> -<ul class="entries"> -<li class="dev"> Option <tt>-all-rounding-modes</tt> has been removed</li> -<li class="dev-break"> The Fval module now supports NaN and infinite values. Major API changes in Fval, Ival and <tt>Cvalue.V</tt> (regarding casts, mostly)</li> -</ul> -<h2>Plugin Impact</h2> -<ul class="entries"> -<li class="dev-break"> Removing Db API for Impact plug-in. Calls to <tt>!Db.Impact</tt> should be replaced by calls to <tt>Impact.Register</tt>.</li> -</ul> -<h2>Plugin Metrics</h2> -<ul class="entries"> -<li class="user"> When the value coverage is computed, also shows the total number of statements by function in the filetree of the Gui.</li> -</ul> -<h2>Plugin Occurrence</h2> -<ul class="entries"> -<li class="dev-break"> Removing Db API for Occurrence plug-in. Calls to <tt>!Db.Occurrence</tt> should be replaced by calls to <tt>Occurrence.Register</tt>.</li> -</ul> -<h2>Plugin RTE</h2> -<ul class="entries"> -<li class="bugfix"> Do not emit spurious 'idx < 0' assert on gcc-style FAM. Fixes <a class="private" href="https://git.frama-c.com/frama-c/frama-c/issues/393">#393</a></li> -</ul> -<h2>Plugin Users</h2> -<ul class="entries"> -<li class="dev-break"> Removing Db API for Users plug-in. Calls to <tt>!Db.Users</tt> should be replaced by calls to <tt>Users.Users_register</tt>.</li> -</ul> -</div> -<hr><div><a id="Sulfur-16.0" href="#Sulfur-16.0"></a></div><h3 class="release">Sulfur Release <span class="hversion">[16.0]</span></h3> - -<div class="release"> -<h2>Frama-C General</h2> -<h4>New Features</h4> -<ul class="entries"> -<li class="user-break"><span class="kernel">[ACSL]</span>  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 <tt>-pp-annot</tt> is activated (default for .c files) and can be fixed easily in y / *p (as it is pretty-printed)</li> -<li class="user-break"><span class="kernel">[Kernel]</span>  qualifiers are dropped from the return type of functions, as they make no real sense</li> -<li class="user"><span class="kernel">[Kernel]</span>  Added option <tt>-print-return</tt> to inline gotos to return</li> -<li class="user"><span class="kernel">[Kernel]</span>  Composite types are now required to have equal tags as per the C standard; no more support for isomorphic structs.</li> -<li class="user-break"><span class="kernel">[Kernel]</span>  Fix invalid eids on code generated through loop unrolling</li> -</ul> -<h4>Bug Fixes</h4> -<ul class="entries"> -<li class="bugfix"><span class="kernel">[Kernel]</span>  stop removing const attribute on local variables. Fixes <a class="private" href="https://git.frama-c.com/frama-c/frama-c/issues/301">#301</a></li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Parser now handle mixed concatenation of string and wstring. Fixes <a class="private" href="https://git.frama-c.com/frama-c/frama-c/issues/1467">#1467</a></li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Fix unmarshalling of save files that contain more than 4Gb of uncompressed data. Patch from TIS-interpreter.</li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Strip bitfield attribute when performing integral promotions on bitfields of size short or char. Fixes incorrect attributes on the resulting expression.</li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Fix various typos in source code and user messages. Patch by Debian. Fixes <a class="public" href="http://bts.frama-c.com/view.php?id=2323">#2323</a></li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Fixes configure script on bytecode only architecture. Initial version of the patch by Debian. Fixes <a class="public" href="http://bts.frama-c.com/view.php?id=2325">#2325</a></li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  More thorough checks on l-values with function type. Non-sensical expressions are now rejected at parsing type.</li> -</ul> -<h4>Developers Only</h4> -<ul class="entries"> -<li class="dev-break"><span class="kernel">[ACSL]</span>  Refactor handling of logic labels in AST</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  Completely separate types between Cil_types and Logic_ptree, removing needless polymorphism</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  Remove needless repetition of declared logic labels in Tapp and Papp nodes. Fixes <a class="private" href="https://git.frama-c.com/frama-c/frama-c/issues/274">#274</a></li> -<li class="dev"><span class="kernel">[Kernel]</span>  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</li> -<li class="dev"><span class="kernel">[Makefile]</span>  add gui-byte target to only build bytecode GUI</li> -</ul> -<h2>Frama-C GUI</h2> -<ul class="entries"> -<li class="user"><span class="kernel">[Gui]</span>  In the filetree, the filter menu appears on a right click on the header, while a left click sorts the tree.</li> -</ul> -<h2>Plugin Callgraph</h2> -<ul class="entries"> -<li class="user-break"> Option <tt>-cg-init-roots</tt> replaced by <tt>-cg-service-roots</tt> (almost equivalent); new options <tt>-cg-function-pointers</tt> (ignore function pointers; unsound) and <tt>-cg-roots</tt> (compute subgraphs).</li> -</ul> -<h2>Plugin Eva</h2> -<h4>New Features</h4> -<ul class="entries"> -<li class="user"> More precise evaluation of <tt>\initialized</tt> and <tt>\dangling</tt> predicates.<br/><br/></li> -<li class="user"> New directive Frama_C_domain_show_each prints the internal properties about the arguments inferred by each available domain whose log category is enabled.</li> -<li class="user"> Frama_C_dump_each prints the state of each available domain whose log category is enabled.</li> -<li class="user"> 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.</li> -<li class="user"> The subdivision of the evaluation of non-linear expressions (through the <tt>-val-subdivide-non-linear</tt> option) also applies to the new evaluations requested by the equality domain.</li> -<li class="user"> New sign domain for demonstration purposes only.</li> -<li class="user-break"> Better handling of function alloca(), via builtin Frama_C_alloca.</li> -<li class="user"> In the GUI, the <tt>"Values"</tt> panel displays the values computed by using the properties inferred by all enabled domains.</li> -<li class="user"> Emits overflow alarms on unsigned left shift when <tt>-warn-unsigned-overflow</tt> is enabled.</li> -<li class="user-break"> Fixed memory leak with option <tt>-val-subdivide-non-linear</tt></li> -<li class="user-break"> Fix soundness (resp. precision) bug on big-endian (resp. little-endian) architectures. This bug triggered on low-level code, typically when using bitfields</li> -<li class="user"> Various precision improvements in the interpretation of the behaviors of a specification.</li> -<li class="user"> The backward propagation tries to reduce integer values by considering separately the bounds of their intervals.</li> -<li class="user"> Uses assigns clauses to over-approximate the effects of assembly statements. Warns if no assigns clause is provided.</li> -</ul> -<h4>Bug Fixes</h4> -<ul class="entries"> -<li class="bugfix"> Fix soundness bug in string builtins where some invalid offsets did not generate alarms.</li> -<li class="bugfix"> Fix missing alarms when downcasting pointer values.</li> -<li class="bugfix"> Fix a crash when downcasting pointer values with the option <tt>-val-warn-signed-converted-downcast</tt> enabled.</li> -<li class="bugfix"> The cvalue states saved after each statement are now properly deleted when an Eva parameter is changed in the GUI.</li> -<li class="bugfix"> Fix performance issue with the equality domain.</li> -<li class="bugfix"> Fixes a soundness bug where a loop invariant could be wrongly proved correct in some marginal cases.</li> -<li class="bugfix"> Fixes an optimization issue where the reduction by a loop invariant just after widenings could impede the convergence.</li> -<li class="bugfix"> Fixes a performance issue in offsetmaps, that occured when reading or copying values smaller than cells in large arrays.</li> -<li class="bugfix"> Fix bug in the handling of non-explicitly volatile fields inside volatile structs or unions</li> -<li class="bugfix"> Fix bugs when evaluating \ìnitialized, <tt>\dangling</tt> and <tt>\separated</tt> on addresses of bitfields</li> -</ul> -<h4>Developers Only</h4> -<ul class="entries"> -<li class="dev-break"> Abstract domains have to provide a log category and a function show_expr that prints the internal properties inferred about an expression.</li> -<li class="dev"> The argument <tt>~with_alarms</tt> for functions of <tt>Db.Value</tt> is now optional, and will be removed in a later version.</li> -<li class="dev"> New functor in <tt>domains/simple_memory.ml</tt> to build a complete domain from a value abstraction. The abstract states link each scalar variable of a program to an abstract value.</li> -<li class="dev-break"> In abstract domains, compute_using_specification is replaced by logic_assign, that interprets one <tt>\assigns</tt> clause. Complete specification are now interpreted through successive calls to evaluate_predicate, reduce_by_predicate and logic_assign.</li> -</ul> -<h2>Plugin Metrics</h2> -<ul class="entries"> -<li class="user"> In the Gui, shows the percentage and the number of dead statements (when computed) for each function of the filetree.</li> -</ul> -<h2>Plugin Report</h2> -<ul class="entries"> -<li class="dev-break"> Removing Db API for Report plug-in. Calls to <tt>!Db.Report.print</tt> should be replaced by calls to <tt>Report.Register.print</tt>.</li> -</ul> -<h2>Plugin RTE</h2> -<ul class="entries"> -<li class="user"> add option <tt>-rte-initialized</tt> to generate assertions over read accesses to potentially uninitialized locations.</li> -<li class="bugfix"> Fix bounds of alarms emitted when downcasting to bitfields (issue <tt>'2314'</tt>)</li> -<li class="user"> Emits overflow alarms on unsigned left shift when <tt>-warn-unsigned-overflow</tt> is enabled.</li> -<li class="user"> add <tt>-warn-not-finite-float</tt> for checking that infinite and NaN floats are not produced.</li> -</ul> -<h2>Plugin Scope</h2> -<ul class="entries"> -<li class="dev-break"> Removing Db API for Scope plug-in. Calls to <tt>!Db.Scope</tt> should be replaced by calls to Scope.</li> -</ul> -<h2>Plugin Slicing</h2> -<ul class="entries"> -<li class="user-break"> Fix invalid eids on code generated through option <tt>-slicing-level</tt> >= 2</li> -<li class="dev-break"> Removing Db API for Slicing plug-in. Calls to <tt>!Db.Slicing</tt> should be replaced by calls to <tt>Slicing.Api</tt>.</li> -<li class="dev-break"> Removing deprecated '<tt>-slice-option</tt>' and related <tt>!Db.Slicing.Projet.print_exported_project</tt>. Minor changes into <tt>!Db.Slicing.Projet.extract</tt>.</li> -</ul> -<h2>Plugin Sparecode</h2> -<ul class="entries"> -<li class="user-break"> Rename option <tt>-rm-unused-globals</tt> to <tt>-sparecode-rm-unused-globals</tt>.</li> -</ul> -</div> -<hr><div><a id="Phosphorus-15.0" href="#Phosphorus-15.0"></a></div><h3 class="release">Phosphorus Release <span class="hversion">[15.0]</span></h3> - -<div class="release"> -<h2>Frama-C General</h2> -<h4>New Features</h4> -<ul class="entries"> -<li class="user-break"><span class="kernel">[Kernel]</span>  Stricter verification for extern, static and inline specifiers (support for CERT DCL-36<tt>-C</tt> coding rule)</li> -<li class="user"><span class="kernel">[Kernel]</span>  New option <tt>-no-autoload-plugins</tt> (equivalent to old <tt>-no-dynlink</tt>); mostly for internal use.</li> -<li class="user"><span class="kernel">[Kernel]</span>  New option <tt>-print-machdep</tt> (help group).</li> -<li class="user"><span class="kernel">[Kernel]</span>  Bash completion for Frama-C options. See <a class="private" href="https://git.frama-c.com/frama-c/frama-c/issues/154">#154</a>.</li> -<li class="user"><span class="kernel">[Kernel]</span>  New option <tt>-print-libc</tt>, to expand include directives for files in the Frama-C stdlib (no longer expanded by default).</li> -<li class="user-break"><span class="kernel">[Kernel]</span>  Zarith library is now required</li> -<li class="user-break"><span class="kernel">[Kernel]</span>  Better handling of VLA (use explicit function calls to mark deallocation of VLA at appropriate program points)</li> -<li class="user-break"><span class="kernel">[Kernel]</span>  Explicit AST nodes to mark local variables initialization.</li> -<li class="user"><span class="kernel">[Kernel]</span>  Dynlink is now mandatory, no degraded static mode.</li> -</ul> -<h4>Bug Fixes</h4> -<ul class="entries"> -<li class="bugfix"><span class="kernel">[Cil]</span>  Pointer subtractions with arguments of incompatible types are now refused. The resulting expression is typed as ptrdiff_t instead of int.</li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  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 <a class="public" href="http://bts.frama-c.com/view.php?id=2249">#2249</a>).</li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Fixes oneret normalization in presence of statement contract and absence of return. See <a class="private" href="https://git.frama-c.com/frama-c/frama-c/issues/255">#255</a> and <a class="public" href="http://bts.frama-c.com/view.php?id=2235">#2235</a>.</li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Fix crash when loading a saved file without a plug-in which has previously emitted a status with a tuning parameter.</li> -</ul> -<h4>Developers Only</h4> -<ul class="entries"> -<li class="dev"><span class="kernel">[Kernel]</span>  Utility API for checking volatile attribute in Cil.</li> -</ul> -<h2>Frama-C GUI</h2> -<ul class="entries"> -<li class="dev-break"><span class="kernel">[Gui]</span>  Signature change for constructor <tt>Pretty_source.PVDecl</tt></li> -</ul> -<h2>Plugin Callgraph</h2> -<ul class="entries"> -<li class="bugfix"> Fixes inverted <tt>callers/callee</tt> in indirect calls</li> -</ul> -<h2>Plugin Eva</h2> -<h4>New Features</h4> -<ul class="entries"> -<li class="user"> New (internal) mechanism to handle C functions' return values. Messages now mention <tt>\result</tt><foo> for the value returned by 'foo'.</li> -<li class="user-break"> Option <tt>-val-show-progress</tt> is now unset by default</li> -<li class="user"> Activate option <tt>-remove-redundant-alarms</tt> by default.</li> -<li class="user"> New option <tt>-val-builtins-list</tt></li> -<li class="user-break"> Renamed dynamic allocation builtins for improved consistency. In particular, Frama_C_alloc_size becomes Frama_C_malloc_fresh.</li> -</ul> -<h4>Bug Fixes</h4> -<ul class="entries"> -<li class="bugfix"> Unsound support for recursion, through option <tt>-val-ignore-recursive-calls</tt>. The support of recursion through the use of 'assigns' clauses, previously available in Value, was unsound and has been removed</li> -<li class="bugfix"> Fix bug <a class="public" href="http://bts.frama-c.com/view.php?id=2277">#2277</a>. The initial state of the analysis now depends on all relevant options, including kernel options <tt>-warn-</tt>...</li> -<li class="bugfix"> Fixes a crash with the <tt>-val-subdivide-non-linear</tt> option, on subdivisions of evaluations involving pointer values.</li> -<li class="bugfix"> Fixes a crash when backward-propagating an imprecise value on a 32<tt>-bits</tt> floating point addition. A non-single precision value was erroneously returned.</li> -<li class="bugfix"> Perform widening in the symbolic locations domain.</li> -<li class="bugfix"> Fix widening in the gauges domain, in particular with nested loops and pointers that change base address through iterations</li> -</ul> -<h4>Developers Only</h4> -<ul class="entries"> -<li class="dev"> Functions <tt>Db.Value.fun_set_args</tt> and <tt>Db.Value.globals_set_initial_state</tt> are now compatible with Eva.<br/><br/></li> -<li class="dev-break"> Incompatible API changes in module <tt>Cvalue.Model</tt>. Functions named 'unspecified' have been renamed into 'indeterminate', and some arguments have been removed.</li> -</ul> -<h2>Plugin Inout</h2> -<ul class="entries"> -<li class="user"> Option <tt>-inout-callwise</tt> is now always active, and will be removed in a later version</li> -<li class="bugfix"> Prevent formal variables of functions with only a specification from leaking into results</li> -</ul> -<h2>Plugin Metrics</h2> -<ul class="entries"> -<li class="user"> Programmatic API for some functions via <tt>Metrics.mli</tt>.</li> -</ul> -<h2>Plugin Obfuscator</h2> -<ul class="entries"> -<li class="bugfix"> Fix typo in help message (bts <a class="public" href="http://bts.frama-c.com/view.php?id=2269">#2269</a>).</li> -</ul> -<h2>Plugin Rte</h2> -<ul class="entries"> -<li class="user"> Remove option <tt>-rte-all</tt>.</li> -</ul> -<h2>Plugin Scope</h2> -<ul class="entries"> -<li class="bugfix"> Fix bug in the functions of <tt>Db.Scope</tt> in presence of alarms refering to volatile memory locations, or to variables that leave scope. Also impacts Eva option <tt>-remove-redundant-alarms</tt></li> -</ul> -<h2>Plugin Value</h2> -<ul class="entries"> -<li class="user-break"> Support for the legacy value analysis has been abandoned, Eva is now always active. Option <tt>-no-eva</tt> has been removed.</li> -<li class="user"> Widen hints directives @widen_hints now accept arbitrary l-values (evaluated at analysis time) in place of variables.</li> -</ul> -<h2>Plugin Variadic</h2> -<ul class="entries"> -<li class="user-break"> Change of command line argument names for the plugin Variadic. The new names are more expressive and avoid confusions with the plugin Value. Use <tt>-variadic-translation</tt> or <tt>-variadic-no-translation</tt> instead of <tt>-va</tt> or <tt>-no-va</tt>.</li> -<li class="user"> The plugin is now enabled by default. Use the option <tt>-variadic-no-translation</tt> to keep the original behaviour. The specification generated for the fprintf function family is now more accurate.</li> -</ul> -</div> -<hr><div><a id="Silicon-14.0" href="#Silicon-14.0"></a></div><h3 class="release">Silicon Release <span class="hversion">[14.0]</span></h3> - -<div class="release"> -<h2>Frama-C General</h2> -<h4>New Features</h4> -<ul class="entries"> -<li class="user-break"><span class="kernel">[Cil]</span>  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.</li> -<li class="user-break"><span class="kernel">[Kernel]</span>  OCaml version greater or equal than <tt>4.02</tt>.3 required.</li> -<li class="user-break"><span class="kernel">[Kernel]</span>  OCamlGraph is no longer packaged within Frama-C, and must be installed to build Frama-C from source</li> -<li class="user"><span class="kernel">[Kernel]</span>  Deprecated <tt>Pretty_utils.sfprintf</tt>, use <tt>Format.asprintf</tt> instead.</li> -<li class="user"><span class="kernel">[Kernel]</span>  Support for C11 redefinition of typedefs</li> -<li class="user"><span class="kernel">[Kernel]</span>  Fix bug that may occur when modifying several times command line-options taking functions as argument (issue <a class="private" href="https://git.frama-c.com/frama-c/frama-c/issues/109">#109</a>)</li> -<li class="user-break"><span class="kernel">[Kernel]</span>  Fix major bug in the backward dataflow of module Dataflows</li> -<li class="user"><span class="kernel">[Libc]</span>  Implementations of some functions of the standard library are now available in <tt>share/libc/</tt>*.c</li> -<li class="user-break"><span class="kernel">[Libc]</span>  New file <tt>share/libc/string.c</tt>, with simple implementations for C99 functions defined in <tt>string.h</tt>. Duplicate implementations were removed from <tt>share/libc.c</tt>.</li> -<li class="user-break"><span class="kernel">[Libc]</span>  Functions in <tt>share/libc.c</tt> have been inlined into the proper .c files under <tt>share/libc</tt></li> -<li class="user-break"><span class="kernel">[Logic]</span>  Refactoring of ACSL extensions + allow extensions in loop annotations</li> -</ul> -<h4>Bug Fixes</h4> -<ul class="entries"> -<li class="bugfix"><span class="kernel">[Kernel]</span>  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)</li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Scripts that use Gtk can again be loaded using option <tt>-load-script</tt> (bug report: http://<tt>stackoverflow.com</tt>/<tt>questions/38677256/</tt>)</li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Fix bug <a class="public" href="http://bts.frama-c.com/view.php?id=2239">#2239</a> about unsoundness of callgraph's services computation (bug introduced in Frama-C Magnesium).</li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Fix bug when pretty printing an ACSL term <tt>"divisor / *p"</tt> (bts <a class="public" href="http://bts.frama-c.com/view.php?id=2250">#2250</a>).</li> -<li class="bugfix"><span class="kernel">[Makefile]</span>  Fix compilation of plug-ins which depends on another plug-ins when compiled outside Frama-C.</li> -</ul> -<h4>Developers Only</h4> -<ul class="entries"> -<li class="dev-break"><span class="kernel">[Kernel]</span>  Functions <tt>Integer.pgcd</tt> and <tt>Integer.ppcm</tt> are now guaranteed to return a positive result.<br/><br/></li> -<li class="dev"><span class="kernel">[Kernel]</span>  Fixes merging of contract when using <tt>Annotations.add_code_annot</tt></li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  Remove class <tt>Filecheck.check</tt> from API. Use <tt>Filecheck.check_ast</tt> that provides the correct encapsulation.</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  Suppress return_stmt field of kernel_function type. Use <tt>Kernel_function.find_return</tt> instead.</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  Rename some types of the logic AST for more coherence</li> -<li class="dev"><span class="kernel">[Makefile]</span>  Warnings and warn-error are activated only if a file .for_devel is present along side the Makefile (also for plugins)</li> -</ul> -<h2>Frama-C GUI</h2> -<ul class="entries"> -<li class="user"><span class="kernel">[Gui]</span>  Different filters for user assertions and RTEs are now available.</li> -</ul> -<h2>Plugin Eva</h2> -<h4>New Features</h4> -<ul class="entries"> -<li class="user"> Support for options <tt>-warn-signed-downcast</tt> and <tt>-warn-unsigned-downcast</tt>.</li> -<li class="user"> Improvements to option <tt>-val-subdivide-non-linear</tt> on expressions such as x*x+y*y, or t[i*i].</li> -<li class="user"> Improvements to option <tt>-val-subdivide-non-linear</tt> for high number of subdivisions </li> -<li class="user"> Various improvements to experimental Apron domain</li> -<li class="user"> More systematic backward-propagation between actual parameters and formals</li> -<li class="user"> New experimental Gauges domain, that relates integer variable to loop counters.</li> -</ul> -<h4>Bug Fixes</h4> -<ul class="entries"> -<li class="bugfix"> Setting option <tt>-val-warn-copy-indeterminate</tt> 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</li> -<li class="bugfix"> fix performance bug in the equality domain, especially visible on programs with many local variables.</li> -<li class="bugfix"> Fix bug in equality domain, after assignements lv = e where the modified locations intersect those involved in computing lv</li> -<li class="bugfix"> Prevent incorrect reductions on memory locations with volatile qualifier</li> -<li class="bugfix"> Fix bug in the bitwise domain, on some applications of the & and | operators</li> -<li class="bug-break"> Fix soundness bug on statements with RTE or programmatically-added user assertions (bts <a class="public" href="http://bts.frama-c.com/view.php?id=2258">#2258</a>). 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.</li> -</ul> -<h2>Plugin From</h2> -<ul class="entries"> -<li class="user-break"> Removed options <tt>-experimental-path-deps</tt> and <tt>-experimental-mem-deps</tt>.</li> -</ul> -<h2>Plugin Nonterm</h2> -<ul class="entries"> -<li class="user"> overall increase in precision, especially on compound statements (if, switch, loops...). Verbosity has been decreased</li> -<li class="user"> New options <tt>-nonterm-ignore</tt> f1,..,fn (to ignore calls to functions f1,..,fn) and <tt>-nonterm-dead-code</tt> (to warn about syntactically dead code)</li> -</ul> -<h2>Plugin Rte</h2> -<ul class="entries"> -<li class="user"> New option <tt>-rte-pointer-call</tt>, to generate annotations for calls through function pointers</li> -</ul> -<h2>Plugin Scope</h2> -<ul class="entries"> -<li class="user-break"> Fix bug that might lead to unsoundness and / or looping in 'Datascope' functionality (<a class="private" href="http://bts.frama-c.com/view.php?id=235">#235</a>)</li> -</ul> -<h2>Plugin Value</h2> -<h4>New Features</h4> -<ul class="entries"> -<li class="user"> 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).</li> -<li class="user"> New message key final-states, that can be used to deactivate the printing of the abstract states at the end of each function</li> -<li class="user"> New option <tt>-val-warn-on-alarms</tt>, which governs whether alarms are printed as warnings or text.</li> -<li class="user"> New message key 'garbled-mix', to track garbled mix generated during the analysis</li> -<li class="user-break"> Several warnings emitted by Value are now properly prefixed by [value] instead of [kernel]</li> -<li class="user-break"> API changes in modules Lmap and <tt>Cvalue.Model</tt>. All occurrences of `Map in returned value should be replaced by `Value</li> -<li class="user"> 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 (<tt>e.g</tt>. <tt>int/float</tt> or <tt>signed/unsigned</tt>) causes a red alarm.</li> -<li class="user"> New option <tt>-val-flamegraph</tt>, to dump information about analysis times as a Flamegraph</li> -<li class="user-break"> Option <tt>-val-show-time</tt> has been removed. Options <tt>-val-show-perf</tt> or <tt>-val-flamegraph</tt> offer more information</li> -<li class="user-break"> Do not compute the sizeof of a function when evaluating a function call through a pointer. This avoids some warnings in MSVC mode.</li> -<li class="user"> valid_string and valid_read_string predicates are now evaluated by Value</li> -<li class="user"> New builtins for string-related functions: Frama_C_strlen, Frama_C_strchr, Frama_C_strnlen, Frama_C_memchr and Frama_C_rawmemchr</li> -<li class="user"> Extended support for syntactic widening hints (@widen_hints - see the Value user manual for more details)</li> -<li class="user-break"> Option <tt>-val-warn-copy-indeterminate</tt> is now set by default. See command-line help if you want to deactivate it.</li> -<li class="user"> New (experimental) option <tt>-val-builtins-auto</tt>, to automatically replace known C functions by builtins. Will be set by default in Phosphorus.</li> -</ul> -<h4>Bug Fixes</h4> -<ul class="entries"> -<li class="bugfix"> Fix crash when extracting bits of a long double value. (Issue 92 on TIS-interpreter, reported by ch3root.).</li> -<li class="bugfix"> Option <tt>-val-show-initial-state</tt> has been removed. Instead, <tt>-value-msg-key</tt>=<tt>-initial-state</tt> can be used</li> -<li class="bugfix"> Garbled mix created when analyzing assigns / from clauses are now tagged as having <tt>"Library function"</tt> origin</li> -<li class="bugfix"> Option <tt>-val-show-perf</tt> now properly takes into account the time taken by the main function itself (without its callees)</li> -<li class="bugfix"> Frama_C_cos and Frama_C_sin builtins are now precise by default. The former Frama_C_cos / Frama_Csin_precise have been removed</li> -</ul> -</div> -<hr><div><a id="Aluminium-13.0" href="#Aluminium-13.0"></a></div><h3 class="release">Aluminium Release <span class="hversion">[13.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>  Add notation '{{ "{" }} x, y, z }' for defining sets.</li> -<li class="user"><span class="kernel">[ACSL]</span>  Add built-in operators for lists.</li> -<li class="user"><span class="kernel">[ACSL]</span>  New predicate <tt>\valid_function</tt>, requiring the compatibility between the type of the pointer and the function being pointed.</li> -<li class="user-break"><span class="kernel">[Cil]</span>  Typing within comparisons is now more strict, or made more explicit through casts.</li> -<li class="user"><span class="kernel">[Cil]</span>  Double pointer casts on the NULL pointer are now simplified.</li> -<li class="user"><span class="kernel">[Cil]</span>  Add support for parsing digraphs.</li> -<li class="user-break"><span class="kernel">[Cil]</span>  Incorrect return statements (return void on non-void functions and vice-versa) now generate errors instead of warnings.</li> -<li class="user-break"><span class="kernel">[Cil]</span>  Better handling of C99 flexible array members (FAMs). Static initialization of FAMs (a GCC extension) is no longer supported.</li> -<li class="user-break"><span class="kernel">[Cil]</span>  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 (<tt>e.g</tt>. <tt>-machdep</tt> gcc_x86_32).</li> -<li class="user"><span class="kernel">[Cil]</span>  Operator ! applied to constant expression is no longer simplified when not required.</li> -<li class="user"><span class="kernel">[Cil]</span>  Add proper support for empty aggregate initializers in GCC mode.</li> -<li class="user"><span class="kernel">[Kernel]</span>  New option <tt>-set-project-as-default</tt>.<br/><br/></li> -<li class="user"><span class="kernel">[Kernel]</span>  New option <tt>-remove-projects</tt>.</li> -<li class="user"><span class="kernel">[Kernel]</span>  New options <tt>-then-last</tt> and <tt>-then-replace</tt>.</li> -<li class="user"><span class="kernel">[Kernel]</span>  The untyped AST is no longer removed by basic program transformations such as loop unrolling.</li> -<li class="user-break"><span class="kernel">[Kernel]</span>  Option <tt>-warn-undeclared-callee</tt> changed to <tt>-implicit-function-declaration</tt>, which receives an argument (ignore, warn or error) specifying what to do when an undeclared function is called.</li> -<li class="user"><span class="kernel">[Kernel]</span>  Option <tt>-collect-messages</tt> is obsolete and will be removed in a future version; messages are now always collected.</li> -<li class="user"><span class="kernel">[Kernel]</span>  Automatic generation of assigns from GCC's extended asm.</li> -<li class="user"><span class="kernel">[Kernel]</span>  Registering twice the same machdep is now accepted.</li> -<li class="user"><span class="kernel">[Kernel]</span>  New option -<plugin><tt>-log</tt> to copy the output of plug-ins into one or several text files (described in the User Manual).</li> -<li class="user-break"><span class="kernel">[Makefile]</span>  Target 'make rebuild' has been renamed into 'make clean-rebuild'.</li> -</ul> -<h4>Bug Fixes</h4> -<ul class="entries"> -<li class="bugfix"><span class="kernel">[ACSL]</span>  Fixes example of logic label use. Fixes bug <a class="public" href="http://bts.frama-c.com/view.php?id=2203">#2203</a>.</li> -<li class="bugfix"><span class="kernel">[ACSL]</span>  Fixes implicit logic label generation on recursive definitions. Fixes bug <a class="public" href="http://bts.frama-c.com/view.php?id=2158">#2158</a>.</li> -<li class="bugfix"><span class="kernel">[ACSL]</span>  Fixes precedence uncompliance within ACSL Manual of some bitwise operators and more aggressive checks of consistent relation chains.</li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Comments are preserved even when loops are unrolled. Fixes issue <a class="private" href="http://bts.frama-c.com/view.php?id=2176">#2176</a>.</li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Avoid comment duplications on generated code.</li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  do not crash when loading statuses depending from non existing parameter. Fixes issue <a class="private" href="http://bts.frama-c.com/view.php?id=2181">#2181</a>.</li> -<li class="bugfix"><span class="kernel">[Libc]</span>  Fix specifications of memchr and strncpy.</li> -<li class="bugfix"><span class="kernel">[Logic]</span>  Meaningless assigns clauses are now rejected more aggressively. Fixes bug <a class="public" href="http://bts.frama-c.com/view.php?id=1790">#1790</a>.</li> -</ul> -<h4>Developers Only</h4> -<ul class="entries"> -<li class="dev-break"><span class="kernel">[Cil]</span>  Buggy record <tt>Cil.miscState</tt> has been removed. Customization must be done directly in <tt>Cil_printer.state</tt>.</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  API change for function <tt>Alarms.register</tt>. See .mli for details.</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  Removed function <tt>State_selection.list_state_union</tt>. Use <tt>State_selection.of_list</tt> or <tt>State_selection.list_union</tt> instead.</li> -<li class="dev"><span class="kernel">[Kernel]</span>  Several incompatible changes in module Property.</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  Do not raise Invalid_arg and Failure exn but use custom exceptions instead. Prevents warning 52 in OCaml <tt>4.03</tt>.0 Functions raising new exceptions are: - <tt>Db.From.find_deps_term_no_transitivity_state</tt> - <tt>Db.Interp</tt>.*</li> -<li class="dev-break"><span class="kernel">[Makefile]</span>  Get rid of FRAMAC_MAKE variable. Use FRAMAC_INTERNAL instead for distinguishing internal and external mode.</li> -<li class="dev"><span class="kernel">[Makefile]</span>  New option PLUGIN_EXTRA_DIRS for multi-dir plugins.</li> -<li class="dev"><span class="kernel">[Ptests]</span>  New EXEC: directive.</li> -</ul> -<h2>Frama-C GUI</h2> -<ul class="entries"> -<li class="dev-break"><span class="kernel">[Gui]</span>  Refactor GUI Helpers. (Toolbox and (partially) Gtk_helper moved to Wutil,Widget, Wform, Wtext and Wtable).</li> -<li class="user-break"><span class="kernel">[Gui]</span>  Signature change for function <tt>Design.register_source_highlighter</tt>; the first argument of the callback has now type <tt>Design.reactive_buffer</tt>, which can be coerced back to a <tt>GSourceView2.source_buffer</tt> using method buffer.</li> -</ul> -<h2>Plugin Eva</h2> -<h4>New Features</h4> -<ul class="entries"> -<li class="user"> More aggressive reductions in complex conditions such as if(a+3 < 10).</li> -<li class="user"> Improvements to backward propagation, on memory accsses and bitwise operations.</li> -<li class="user"> Experimental domain dedicated to storing and learning information from syntactic equalities (option <tt>-eva-equality-domain</tt>).</li> -<li class="user"> New experimental domain that improves precision on bitwise operations, for example on pointers. Activated by option <tt>-eva-bitwise-domain</tt>.</li> -</ul> -<h4>Bug Fix</h4> -<ul class="entries"> -<li class="bugfix"> Fixed some bugs related to 0. vs. -0. in conditions.</li> -</ul> -<h2>Plugin From</h2> -<ul class="entries"> -<li class="user"> Option <tt>-from-verify-assigns</tt> takes into account direct and indirect dependencies.</li> -</ul> -<h2>Plugin LoopAnalysis</h2> -<ul class="entries"> -<li class="user"> New plug-in 'LoopAnalysis' which estimates loop bounds and <tt>-slevel-function</tt> parameters. Invoked using option <tt>-loop</tt>.</li> -</ul> -<h2>Plugin Metrics</h2> -<ul class="entries"> -<li class="bugfix"> Fix list of undefined functions; functions that are never called were not reported.</li> -<li class="bugfix"> Fix option <tt>-metrics-value-cover</tt> when option <tt>-metrics-libc</tt> is not set.</li> -<li class="user-break"> Global variables defined in Frama-C standard library are no longer counted when option <tt>-metrics-libc</tt> is not set.</li> -</ul> -<h2>Plugin Nonterm</h2> -<ul class="entries"> -<li class="user"> New plug-in 'nonterm' for detection of definite non-termination based on Value.</li> -</ul> -<h2>Plugin RTE</h2> -<ul class="entries"> -<li class="bugfix"> Fix unsoundness for overflows on binary operations when one or two operands were constant.</li> -<li class="bugfix"> Fix unsoundness on unary minus expressions when option <tt>-rte-trivial-annotations</tt> is active.</li> -</ul> -<h2>Plugin Sparecode</h2> -<ul class="entries"> -<li class="bugfix"> Fix crash when an entire function becomes spare. (issue <a class="private" href="https://git.frama-c.com/frama-c/frama-c/issues/157">#157</a>).</li> -</ul> -<h2>Plugin Value</h2> -<h4>New Features</h4> -<ul class="entries"> -<li class="user"> Better precision for calls through function pointers when multiple functions are possible. The abstract state now contains the information of which function was called.</li> -<li class="user"> During the evaluation of ACSL 'assert', intermediate statuses (<tt>e.g</tt>. True, then Unknown, then True) are now reported in the console.</li> -<li class="user"> New option <tt>-val-warn-undefined-pointer-comparison</tt>.</li> -<li class="user-break"> 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.</li> -<li class="user-break"> 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.</li> -<li class="user"> Support for <tt>\valid_function</tt> predicate during evaluation.</li> -<li class="user"> Distinguish direct and indirect dependencies in 'from' clauses to compute the effecst of an '<tt>assigns/from</tt>' clause. See section <tt>7.2</tt> of the manual.</li> -<li class="user"> Messages on ACSL predicates with <tt>Unknown/Invalid</tt> status are now emitted with a 'warning' severity, consistently with the emission of alarms. 'True' statuses are hidden if option <tt>-val-show-progress</tt> is unset.</li> -<li class="user"> Informative messages about inactive behaviors are now emitted only at verbosity level 2.</li> -<li class="user"> Support for evaluation of predicate <tt>\valid_read_string</tt> on constant strings.</li> -</ul> -<h4>Bug Fixes</h4> -<ul class="entries"> -<li class="bugfix"> 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 <a class="private" href="http://bts.frama-c.com/view.php?id=1956">#1956</a>.</li> -<li class="bug-break"> 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 <tt>-no-eva</tt> to switch back to the legacy version. Changelog entries labelled 'Eva' refer to this new version. Entries labelled 'Value' apply to both versions.</li> -<li class="bugfix"> Take into account 'volatile' qualifiers on struct typedefs, which were previously ignored. Fixes issue <a class="private" href="https://git.frama-c.com/frama-c/frama-c/issues/102">#102</a>.</li> -<li class="bugfix"> Evaluation of ACSL ranges takes into account option <tt>-safe-arrays</tt>. In particular t[..] remains within the bounds of t. Fixes bug <a class="private" href="http://bts.frama-c.com/view.php?id=1639">#1639</a>.</li> -<li class="bugfix"> 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.</li> -<li class="bugfix"> Fix handling of functions without a body that return a pointer. The pointer was aligned on an incorrect frontier.</li> -</ul> -<h4>Developers Only</h4> -<ul class="entries"> -<li class="dev-break"> 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 <tt>Abstract_interp.Comp</tt>.</li> -<li class="dev-break"> <tt>Base.base_max_offset</tt> has been removed. Part of its functionality is still available via <tt>Base.valid_range</tt>, whose return type is now more expressive.</li> -<li class="dev-break"> API change in functor <tt>Lmap.Make</tt>.</li> -</ul> -<h2>Plugin Variadic</h2> -<ul class="entries"> -<li class="user"> New plug-in 'Variadic' which translates variadic functions, calls and macros to allow analyses to handle them more easily. Invoked using the <tt>-va</tt> option.</li> -</ul> -</div> -<hr><div><a id="Magnesium-12.0" href="#Magnesium-12.0"></a></div><h3 class="release">Magnesium Release <span class="hversion">[12.0]</span></h3> - -<div class="release"> -<h2>Frama-C General</h2> -<h4>New Features</h4> -<ul class="entries"> -<li class="user"><span class="kernel">[Cil]</span>  Function <tt>Printer.change_printer</tt> now allows composing printers, and is called <tt>Printer.update_printer</tt>.</li> -<li class="user"><span class="kernel">[Cil]</span>  Fix incorrect simplifications of '!E' to 0 when E is either an enum with value 0 (bug <a class="public" href="http://bts.frama-c.com/view.php?id=2090">#2090</a>), or an expression whose value wraps.</li> -<li class="user-break"><span class="kernel">[Cil]</span>  Parsing no longer accepts structures containing incomplete types. Fixes bug <a class="private" href="http://bts.frama-c.com/view.php?id=2091">#2091</a>.</li> -<li class="user"><span class="kernel">[Doc]</span>  Fixed typo in the manual (Thx Mihaela Sighireanu).</li> -<li class="user"><span class="kernel">[Kernel]</span>  Add new suffix '.ci' for pre-processed files containing ACSL annotations to be pre-processed.</li> -<li class="user"><span class="kernel">[Kernel]</span>  Added <tt>-no-tty</tt> option to disable terminal capabilities</li> -<li class="user"><span class="kernel">[Kernel]</span>  macro __FRAMAC__ is defined when pre-processing C files in Frama-C.</li> -<li class="user-break"><span class="kernel">[Kernel]</span>  Removed option <tt>-no-dynlink</tt>.</li> -<li class="user"><span class="kernel">[Kernel]</span>  New ACSL predicate <tt>\valid_read_string</tt> in <tt>share/libc/__fc_string_axiomatic.h</tt>.</li> -<li class="user"><span class="kernel">[Kernel]</span>  Special functions CEA_ have been removed.</li> -<li class="user"><span class="kernel">[Kernel]</span>  New API for backward dataflow propagation in file Dataflows.</li> -<li class="user"><span class="kernel">[Kernel]</span>  Reformulated help messages. Option <tt>-help</tt> is more concise. Option <tt>-version</tt> only prints version number. Options <tt>-print-xxx</tt> uniformized. New options <tt>-plugins</tt>, <tt>-print-config</tt>.</li> -<li class="user-break"><span class="kernel">[Kernel]</span>  Dynamic now rely on Findlib. Small changes in API. Option <tt>-load-module</tt> can now load any Findlib package and its dependencies as well.</li> -<li class="user"><span class="kernel">[Kernel]</span>  [2015-07-09] New option <tt>-custom-char-annot</tt> for changing the character introducing ACSL annotations (instead of '@').</li> -<li class="user-break"><span class="kernel">[Kernel]</span>  Removed support for OCaml <tt>3.12</tt>.1</li> -<li class="user-break"><span class="kernel">[Libc]</span>  Most .c and .h files under /share have been merged into /<tt>share/libc</tt>. Inclusions of <tt>builtin.h</tt> should be replaced by <tt>__fc_builtin.h</tt>.</li> -<li class="user"><span class="kernel">[Makefile]</span>  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 <tt>"MyPlugin"</tt> is register under <tt>"frama-c-myplugin"</tt> package.</li> -</ul> -<h4>Bug Fixes</h4> -<ul class="entries"> -<li class="bugfix"><span class="kernel">[Cil]</span>  Fix iterators on C99 designated initializers.</li> -<li class="bugfix"><span class="kernel">[Cil]</span>  Disallow all incomplete types for struct fields Fixes bug <a class="private" href="http://bts.frama-c.com/view.php?id=1672">#1672</a>.</li> -<li class="bugfix"><span class="kernel">[Cil]</span>  Switch statements in which some cases are not constant expressions are now completely disallowed, as per the C standard.</li> -<li class="bugfix"><span class="kernel">[Cil]</span>  Fix parsing of packing directives of the form '#pragma pack(push, N)'.</li> -<li class="bugfix"><span class="kernel">[Cil]</span>  Better typing of '?' operator. Fixes bug <a class="public" href="http://bts.frama-c.com/view.php?id=2117">#2117</a>.</li> -<li class="bugfix"><span class="kernel">[Cil]</span>  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.</li> -<li class="bugfix"><span class="kernel">[Cil]</span>  Fix bug <a class="public" href="http://bts.frama-c.com/view.php?id=1553">#1553</a>, related to nested initialisations of structures containing pointers.</li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Fix clearing of old statuses and hypotheses when a new status is emitted or an annotation is removed.</li> -<li class="bugfix"><span class="kernel">[Libc]</span>  Added ACSL specifications to some standard library functions, including read, write and realloc. Fixes bug <a class="public" href="http://bts.frama-c.com/view.php?id=1939">#1939</a>.</li> -<li class="bugfix"><span class="kernel">[Libc]</span>  Fix bug in the specifications of readir, opendir, closedir and fopen functions, that would cause incorrect analysis in <tt>-lib-entry-mode</tt>.</li> -<li class="bugfix"><span class="kernel">[Libc]</span>  Removed obsolete file <tt>machine.h</tt> (along with other similar files) from the Frama-C share folder. Fixes bug <a class="public" href="http://bts.frama-c.com/view.php?id=2171">#2171</a></li> -<li class="bugfix"><span class="kernel">[Logic]</span>  Better overloading resolution. Fixes bug <a class="public" href="http://bts.frama-c.com/view.php?id=2098">#2098</a>.</li> -<li class="bugfix"><span class="kernel">[Logic]</span>  Correct handling of string and char constant in logic pre-processing. Fixes bug <a class="public" href="http://bts.frama-c.com/view.php?id=2101">#2101</a>.</li> -<li class="bugfix"><span class="kernel">[Logic]</span>  Fix typing bug when converting into a term an expression containing a pointer subtraction.</li> -</ul> -<h4>Developers Only</h4> -<ul class="entries"> -<li class="dev-break"><span class="kernel">[Kernel]</span>  Fixed bug <a class="private" href="http://bts.frama-c.com/view.php?id=2012">#2012</a> about combining <tt>Ast.is_last_decl</tt> and <tt>Kernel_function.get_global</tt>.</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  Function <tt>Integer.two_power</tt> now raises an exception for overly big arguments.</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  AST change: split GVarDecl into GVarDecl and GFunDecl</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  Remove long-obsoleted functions <tt>Cfg.computeCFGInfo</tt> <tt>Cfg.printCfgFilename</tt>, and <tt>Cfg.printCfgChannel</tt>.</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  Remove support of plug-ins without .mli. Fixes bug <a class="private" href="http://bts.frama-c.com/view.php?id=1825">#1825</a>.</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  <tt>Ival.Float_abstract</tt> renamed to Fval. <tt>Fval.inject_r</tt> now may raise <tt>Fval.Non_finite</tt> instead of the old <tt>Float_abstract.Bottom</tt>.</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  Modules Dataflow is deprecated, and will be removed in Aluminium. Module Dataflow2 offers a very similar but simpler API.</li> -<li class="dev-break"><span class="kernel">[Logic]</span>  Functions <tt>Db.Properties.Interp.lval</tt> and <tt>Db.Properties.Interp.expr</tt> have been renamed (into term_lval and term, respectively), and have a new signature.</li> -<li class="dev"><span class="kernel">[Ptests]</span>  New LOG: directive.</li> -</ul> -<h2>Frama-C GUI</h2> -<h4>New Features</h4> -<ul class="entries"> -<li class="user"><span class="kernel">[Gui]</span>  Variables are now left- and right- clickable in the 'information' panel.</li> -<li class="user"><span class="kernel">[Gui]</span>  Internal ids (for statements, code annotations, etc.) are now hidden by default. Start the GUI in debug mode if you want to see them.</li> -<li class="user"><span class="kernel">[Gui]</span>  When a call statement is selected, the statuses of the preconditions of the called functions are displayed in the 'information' panel.</li> -</ul> -<h4>Bug Fix</h4> -<ul class="entries"> -<li class="bugfix"><span class="kernel">[Gui]</span>  Filenames in the GUI file tree (top-left panel) are now sorted correctly. Fixes bug <a class="public" href="http://bts.frama-c.com/view.php?id=2173">#2173</a>.</li> -</ul> -<h4>Developers Only</h4> -<ul class="entries"> -<li class="dev-break"><span class="kernel">[Gui]</span>  Constructor <tt>Pretty_source.PTermLval</tt> now has an additional argument, the property in which the term appears.</li> -<li class="dev-break"><span class="kernel">[Gui]</span>  Minor API changes regarding <tt>Design.reactive_buffer</tt>. Some values that used to have an option type are now guaranteed to be present.</li> -</ul> -<h2>Plugin Callgraph</h2> -<ul class="entries"> -<li class="dev-break"> Remove <tt>Cil.Callgraph</tt>, <tt>Db.Syntactic_callgraph</tt> and <tt>Db.Semantic_callgraph</tt> which are all replaced by the single plug-in Callgraph. See <tt>Changelog_detailled.md</tt> for further detail about this change.</li> -<li class="user-break"> 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 <a class="public" href="http://bts.frama-c.com/view.php?id=755">#755</a>).</li> -</ul> -<h2>Plugin Defs</h2> -<ul class="entries"> -<li class="user"> L-values for which defs are queried are now evaluated only for the callstacks that are currently active, resulting in possibly less locations.</li> -</ul> -<h2>Plugin Impact</h2> -<ul class="entries"> -<li class="user"> Removed function <tt>Db.Impact.slice</tt>, that was actually unrelated to Impact. You can use the functions contained in <tt>Db.Slicing.Select</tt>, in particular <tt>Db.Slicing.Select.select_stmt</tt>, to obtain the same result.</li> -</ul> -<h2>Plugin Inout</h2> -<ul class="entries"> -<li class="user-break"> The inputs of an instruction whose evaluation always fail include the sub-expressions for which evaluation succeeds.</li> -</ul> -<h2>Plugin Metrics</h2> -<ul class="entries"> -<li class="bugfix"> Fix computation of global cyclomatic complexity. Fixes bug <a class="private" href="http://bts.frama-c.com/view.php?id=2089">#2089</a>.</li> -<li class="user"> New category 'Extern global variables', that can be used to check whether some files are missing.</li> -<li class="user"> Functions from Frama-C standard library are now hidden by default.</li> -</ul> -<h2>Plugin Parsing</h2> -<ul class="entries"> -<li class="bugfix"> Black-list gcc's builtin macros for logic pre-processing to avoid warnings for duplication. Fixes bug <a class="public" href="http://bts.frama-c.com/view.php?id=2161">#2161</a>.</li> -</ul> -<h2>Plugin Report</h2> -<ul class="entries"> -<li class="user"> Reports in csv format now honor option <tt>-report-specialized</tt> (previously, preconditions at a callsite were always skipped).</li> -<li class="user"> New option <tt>-report-proven</tt> to control the display of proven properties.</li> -<li class="user"> New export format (.csv), through option <tt>-report-csv</tt>.</li> -</ul> -<h2>Plugin Scope</h2> -<ul class="entries"> -<li class="user"> Assertions previously removed by <tt>-remove-redundant-alarms</tt> are now marked as proven, but remain in the AST.</li> -</ul> -<h2>Plugin Value</h2> -<h4>New Features</h4> -<ul class="entries"> -<li class="user"> Support for <tt>\subset</tt> predicate.<br/><br/></li> -<li class="user"> Improvements to option <tt>-subdivide-float-var</tt>, when subdividing may avoid the emission of an alarm.</li> -<li class="user"> New option <tt>-val-initialization-padding-globals</tt> to specify how padding bits should be initialized. Option <tt>-initialized-padding-globals</tt> is deprecated.</li> -<li class="user"> Improved reduction by assertions of the form <tt>\initialized</tt>(&t[0..N]) when N is above <tt>-plevel</tt>.</li> -<li class="user-break"> Option <tt>-subdivide-float-var</tt> has been renamed into <tt>-val-subdivide-non-linear</tt>, and has now an effect on non-linear integer expressions.</li> -<li class="user"> Local variables that are in scope but not yet initialized are now present in the environment.</li> -<li class="user-break"> In synthetic results, for local variables that are not those of the current function, the approximated values encompass only the callstacks for which the variables were in scope in one of the callers.</li> -<li class="user"> Faster treatment of imprecise struct copying and left shifts in the logic.</li> -<li class="user-break"> Fix bug in <tt>-memexec-all</tt> option in presence of instructions where evaluation was guaranteed to fail.</li> -<li class="user-break"> Terms involving l-values that are bit-fields are now correctly handled.</li> -<li class="user-break"> In <tt>-lib-entry</tt> mode, functions pointers no longer force the generation of dummy functions. Instead, they are initialized to NULL. Fixes bug <a class="private" href="http://bts.frama-c.com/view.php?id=2104">#2104</a>.</li> -<li class="user"> New GUI panel 'Values', that displays nearly all the information previously available under the 'Information' panel.</li> -<li class="user"> Added built-ins for mathematical functions: atan2, fmod, pow, expf, logf, log10f, powf, sqrtf, floor, floorf, ceil, ceilf, round, roundf, trunc, truncf.</li> -<li class="user"> Improved reduction by predicate <tt>\initialized</tt> when the left argument is a range of locations.</li> -<li class="user"> 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.</li> -<li class="user"> Option <tt>-val-split-return-auto</tt> now always split between <tt>NULL/non-NULL</tt> pointers.</li> -<li class="user"> 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.</li> -<li class="user"> Do not emit pointer_comparable alarms on valid pointer comparisons involving objects of size 0.</li> -<li class="user-break"> Float operations that are guaranteed to lead to +/<tt>-infty</tt> (<tt>e.g</tt>. x = FLT_MAX*10.) now stop propagation. Previous behavior was to continue with an imprecise value for x.</li> -<li class="user"> Garbled mix origins now include at most one source location.</li> -<li class="user-break"> All plugins that depend on Value, plus Value itself are now dynamic. Custom plugins must specify in their Makefile the plugins they depend on (<tt>e.g</tt>. PLUGIN_DEPENDENCIES:=Inout Value).</li> -<li class="user-break"> WIDEN_HINTS directive are now cumulative with automatically inferred bounds. Fixes bug <a class="public" href="http://bts.frama-c.com/view.php?id=876">#876</a>.</li> -<li class="user"> The alarms raised when evaluating a global initializer that leads to an undefined behavior are now marked with an <tt>"Invalid"</tt> status.</li> -<li class="user"> Assertions containing <tt>\at</tt>(P, L), where L is a C label, can now be evaluated. Evaluation is done once Value has run; thus, it ignores option <tt>-slevel</tt>.</li> -</ul> -<h4>Bug Fixes</h4> -<ul class="entries"> -<li class="bugfix"> Fix incorrect initialization of padding bits. Option <tt>-initialized-padding</tt> was ignored in some cases.</li> -<li class="bugfix"> Fix initial state in which some volatile qualifiers for nested types were ignored.</li> -<li class="bugfix"> In <tt>-lib-entry</tt> mode, allow the generation of initial states with 0<tt>-sized</tt> bitfields.</li> -<li class="bugfix"> Pointer comparisons using relational operators (<, >=, etc) between a pointer and NULL is now flagged as undefined.</li> -<li class="bugfix"> Check the validity of the operands of the ACSL operators /, %, << and >> when evaluating a predicate.</li> -<li class="bugfix"> pointer_comparable alarms are now emitted with arguments properly cast to void* or void (*)().</li> -</ul> -<h4>Developers Only</h4> -<ul class="entries"> -<li class="dev-break"> Removed function <tt>Cvalue.V.min_and_max_float</tt>. Use <tt>Cvalue.V.project_ival</tt> and <tt>Ival.min_and_max_float</tt>.</li> -<li class="dev-break"> Remove duplicate values <tt>Ival.singleton_zero</tt> and <tt>Ival.singleton_one</tt>. Use script <tt>sodium2magnesium.sh</tt> for automatic migration.</li> -</ul> -</div> -<hr><div><a id="Sodium-11.0" href="#Sodium-11.0"></a></div><h3 class="release">Sodium Release <span class="hversion">[11.0]</span></h3> - -<div class="release"> -<h2>Frama-C General</h2> -<h4>New Features</h4> -<ul class="entries"> -<li class="user"><span class="kernel">[Cil]</span>  Values extracted from initializers of const variables are now accepted as arguments of directives pragma loop UNROLL.</li> -<li class="user-break"><span class="kernel">[Cil]</span>  Frama-C's x86 default machdeps no longer assume that the compiler is GCC. Some typing extensions and builtin are thus deactivated. If you want a GCC-centric analysis, use the gcc-prefixed machdeps.</li> -<li class="user"><span class="kernel">[Cil]</span>  Option <tt>-pp-annot</tt> should be much faster when parsing files with many ACSL annotations.</li> -<li class="user-break"><span class="kernel">[Cil]</span>  Default preprocessing command now includes Frama-C's standard library, and when possible sets option '<tt>-nostdinc</tt>'. See options <tt>-frama-c-stdlib</tt> and <tt>-cpp-gnu-like</tt>.</li> -<li class="user"><span class="kernel">[Kernel]</span>  add instructions for downloading the manuals</li> -<li class="user-break"><span class="kernel">[Kernel]</span>  require ocamlgraph version <tt>1.8</tt>.5</li> -<li class="user"><span class="kernel">[Kernel]</span>  Nicer error message in case of code incompatibility when loading a plug-in.</li> -<li class="user"><span class="kernel">[Kernel]</span>  New option <tt>-const-readonly</tt> (set by default), that asserts that 'const' variables must never be written.</li> -<li class="user-break"><span class="kernel">[Kernel]</span>  New way to handle command line options which accepts sets of values. Values may be prefixed by '+' or '-' to <tt>add/remove</tt> them and categories of values prefixed by '@' are available as well (for instance @all).</li> -<li class="user"><span class="kernel">[Kernel]</span>  New option '<tt>-then-last</tt>', which behaves like '<tt>-then-on</tt>' on the last project created by a program transformer.</li> -<li class="user"><span class="kernel">[Kernel]</span>  Improve pretty-printing of some loops.</li> -<li class="user"><span class="kernel">[Kernel]</span>  Tests are added to the distrib (make tests).</li> -<li class="user"><span class="kernel">[Logic]</span>  New builtin functions <tt>\min</tt> and <tt>\max</tt> of type Set(Integer) -> Int</li> -<li class="user"><span class="kernel">[Logic]</span>  New logic label <tt>"Init"</tt>, that refers to the state just after the initialization of globals.</li> -<li class="user"><span class="kernel">[Logic]</span>  The ACSL predicate '<tt>\specified</tt>', which has been renamed to '!<tt>\dangling_contents</tt>' is now supported.</li> -<li class="user"><span class="kernel">[Logic]</span>  The ACSL parser now ignores /*@{{ "{" }} and /*@} comments, to avoid conflicting with Doxygen.</li> -</ul> -<h4>Bug Fixes</h4> -<ul class="entries"> -<li class="bugfix"><span class="kernel">[Cil]</span>  Fix erroneous integral promotion of type 'char' on architectures where 'char' is unsigned.</li> -<li class="bug-break"><span class="kernel">[Cil]</span>  Variables __FC_MACHDEP_FOO_BAR are now automatically positioned when setting a non-standard machdep and using Frama-C's standard library.</li> -<li class="bugfix"><span class="kernel">[Configure]</span>  fix for autoconf < <tt>2.67</tt> when checking ability of default pre-processor to keep comments<br/><br/></li> -<li class="bugfix"><span class="kernel">[Configure]</span>  use the gcc from the configure for compiling c files</li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Fix bug <a class="public" href="http://bts.frama-c.com/view.php?id=1765">#1765</a> (spelling errors).</li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  allow dynamically loaded module to start with a lower-case letter. Fixes <a class="public" href="http://bts.frama-c.com/view.php?id=1276">#1276</a>.</li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  <tt>-load-module</tt> M now works fine if M uses the API of another plug-in (bts <a class="private" href="http://bts.frama-c.com/view.php?id=1824">#1824</a>).</li> -<li class="bugfix"><span class="kernel">[Logic]</span>  The ACSL parser accepts qualifiers in logic C types.</li> -<li class="bugfix"><span class="kernel">[Makefile]</span>  Do not install ZArith with Frama-C anymore.</li> -</ul> -<h4>Developers Only</h4> -<ul class="entries"> -<li class="dev-break"><span class="kernel">[Cil]</span>  The ikind for <tt>Cil.kinteger64</tt> is now optional.</li> -<li class="dev-break"><span class="kernel">[Cil]</span>  Modifications in some fields of type <tt>Cil_types.mach</tt>. Function <tt>File.new_machdep</tt> has a simpler type.</li> -<li class="dev-break"><span class="kernel">[Cil]</span>  The field 'vlogic' of type <tt>Cil_types.varinfo</tt> has been replaced by the field 'vsource', to avoid confusion with logic variables. The value of the new field is the negation of the previous one.</li> -<li class="dev"><span class="kernel">[Cil]</span>  Variables are created with a field 'vgenerated' set to 'false' by default. Only Cil should position this field to 'true'.</li> -<li class="dev-break"><span class="kernel">[Cil]</span>  Field 'vgenerated' of type <tt>Cil_types.varinfo</tt> has been replaced by the field 'vtemp' to emphasize the fact that it should only be set to true for temp variables generated during elaboration.</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  A new bunch of functors are available to define command line collections.</li> -<li class="dev"><span class="kernel">[Logic]</span>  Annotations.{{ "{" }}iter,fold}_all_code_annot are now by default sorted. Use <tt>~sorted</tt>:false in case of efficiency issues.</li> -<li class="dev"><span class="kernel">[Makefile]</span>  Fixed compilation bug for plug-ins with both a GUI and a non-empty API (bug <a class="private" href="http://bts.frama-c.com/view.php?id=1798">#1798</a>).</li> -</ul> -<h2>Frama-C GUI</h2> -<ul class="entries"> -<li class="dev"><span class="kernel">[Gui]</span>  Logic l-values inside function specifications can now be selected</li> -<li class="user"><span class="kernel">[Gui]</span>  New option <tt>-gui-project</tt> to run the GUI in a given project.</li> -<li class="user-break"><span class="kernel">[Gui]</span>  C expressions can now be selected through the source panel.</li> -</ul> -<h2>Plugin From</h2> -<ul class="entries"> -<li class="user"> New option <tt>-from-verify-assigns</tt> to give <tt>assigns/from</tt> clauses of function with bodies a validity status.</li> -<li class="user"> Major performance improvements on big analyses.</li> -</ul> -<h2>Plugin Inout</h2> -<ul class="entries"> -<li class="user"> Remove undocumented option <tt>-access-path</tt></li> -</ul> -<h2>Plugin Report</h2> -<ul class="entries"> -<li class="user"> New option <tt>-report-callsite-preconditions</tt>.</li> -<li class="user"> More consistent behavior when option <tt>-report-untried</tt> is not set.</li> -<li class="user"> Better reporting of reachability statuses; do not coalesce unproven reachability assertions with other alarms.</li> -</ul> -<h2>Plugin Rte</h2> -<ul class="entries"> -<li class="user"> Very big floating-point constants that are converted to an integer are now reported as overflowing in only one direction</li> -</ul> -<h2>Plugin Semantic</h2> -<h4>New Features</h4> -<ul class="entries"> -<li class="user"> Constant Folding Floating-point constants can now be propagated.</li> -<li class="user"> Constant Folding Generate nicer constants for integers and pointers</li> -<li class="user"> Constant Folding New option <tt>-scf-project-name</tt>.</li> -<li class="user"> Constant Folding Reducing the number of introduced casts; feature issue <a class="private" href="http://bts.frama-c.com/view.php?id=1697">#1697</a>.</li> -<li class="user"> Constant Folding Reducing the number of introduced casts; feature <a class="private" href="http://bts.frama-c.com/view.php?id=1787">#1787</a>.</li> -</ul> -<h4>Bug Fix</h4> -<ul class="entries"> -<li class="bugfix"> Constant Folding Fix crashes <tt>and/or</tt> multiple declations when a global was referenced in the constant-folded project earlier than in the original one.</li> -</ul> -<h2>Plugin Slicing</h2> -<ul class="entries"> -<li class="bugfix"> Fix issues about slicing calls to the main function and journalization (bug <a class="private" href="http://bts.frama-c.com/view.php?id=1684">#1684</a>).</li> -<li class="bugfix"> Fix crashes about multiple slicing pragma inside a function (bug <a class="public" href="http://bts.frama-c.com/view.php?id=1768">#1768</a>).</li> -</ul> -<h2>Plugin Value</h2> -<h4>New Features</h4> -<ul class="entries"> -<li class="user"> Option <tt>-val-after-results</tt> is now always active by default, and can no longer be unset<br/><br/></li> -<li class="user"> Instructions whose execution is guaranteed to fail are now displayed in the GUI</li> -<li class="user"> Alarms when converting integers to floating-point are now reported only for the range that overflows</li> -<li class="user"> Preconditions of functions that are never called are now also marked as dead at each call-site.</li> -<li class="user"> Alarms are now re-evaluated at the end of the analysis. If their truth value is 'Valid' or 'Invalid', this more precise status is used, instead of the previous 'Unknown' one.</li> -<li class="user"> Improve precision of &.</li> -<li class="user"> File-scope and formal const variables are read-only. Any possibility of writing there is treated as alarm.</li> -<li class="user-break"> Complete rewrite of the modules Int_Intervals and Offsetmap_bitwise; both are now implemented with the same datastructure as Offsetmap. Many performance improvements. Many changes in the API of module Offsetmap_bitwise. Few changes in Int_Intervals, but the englobing module Lattice_Interval_Set has been removed.</li> -<li class="user"> When option <tt>-val-callstack-results</tt> is set, the GUI now displays a callstacks-wide consolidation of the possibles values for expressions and terms. Previously, the potentially less precise summary state was used.</li> -<li class="user"> The GUI now showns the value of logic l-values inside function specifications. They are evaluated in the pre-state of the function, before the evaluation of preconditions.</li> -<li class="user"> Improved widening on variables that are used to access an array</li> -<li class="user"> Improved pretty-printing of variables containing pointers.</li> -<li class="user"> Improve conversion of float values that have been written as integers (through low-level memory accesses)</li> -<li class="user"> Option <tt>-val-split-return</tt> can now be used to split between NULL / non-NULL pointers</li> -<li class="user"> More systematic emission of message 'operation [...] incurs a loss of precision', signaling an arithmetic operation on a pointer address. This message is now emitted by Value itself.</li> -<li class="user"> The arguments of an invalid shift operation are now reduced so that they belong to the proper range.</li> -<li class="user"> Message 'extracting bits of a pointer' is no longer emitted, as it was redundant with the warnings about garbled mix.</li> -<li class="user"> Better precision when a scalar value is written through a garbled mix.</li> -<li class="user"> Reduce arguments of a function according to the possible values of the formal at the end of the call.</li> -<li class="user"> Arguments of functions that give rise to an alarm are now reduced when possible.</li> -<li class="user"> Indeterminate bits copied when option <tt>-val-warn-copy-indeterminate</tt> is active now cause a reduction in the source location.</li> -<li class="user-break"> Logic ranges are now evaluated using a dedicated lattice. Results are almost always more precise, and the analysis faster.</li> -<li class="user"> Per-callstack results are now always computed. Option <tt>-val-callstack-results</tt> is deprecated.</li> -<li class="user"> Option <tt>-slevel-merge-after-loop</tt> renamed to <tt>-val-slevel-merge-after-loop</tt>. Now takes a set of kernel functions as an argument.</li> -<li class="user"> Removed message "assigning non-deterministic value from the first time".</li> -<li class="user"> Accesses to '*(foo *)p' may now reduce p according to the validity of the access, when useful.</li> -<li class="user"> Accesses to locations that contain garbled mix now cause the garbled mix to be reduced to the set of valid locations.</li> -<li class="user"> Special functions CEA_ are deprecated. Use Frama_C_show_each or Frama_C_dump_each instead.</li> -</ul> -<h4>Bug Fixes</h4> -<ul class="entries"> -<li class="bugfix"> Dividing an integer value by a memory address requires the address to be comparable to NULL.</li> -<li class="bugfix"> Fix evaluation of '/' in the logic, that silently ignored the presence of the value 0 in the divisor.</li> -<li class="bugfix"> Text-only alarms that used the '<tt>\defined</tt>' predicate (to warn about dereferencing pointers to out-of-scope variables) are now emitted with the '<tt>\dangling_contents</tt> predicate.</li> -<li class="bugfix"> When for missing '<tt>\from</tt>' clause for '<tt>\result</tt>' when result is used in a postcondition. Fixes bug <a class="public" href="http://bts.frama-c.com/view.php?id=1908">#1908</a>.</li> -<li class="bugfix"> Fix bug when writing precise values at too many locations in packed arrays.</li> -<li class="bugfix"> Improved precision for variables that are reduced (but not written) during a call memorized by option <tt>-memexec-all</tt></li> -</ul> -<h4>Developers Only</h4> -<ul class="entries"> -<li class="dev-break"> Major API change in directories <tt>src/ai</tt> and <tt>src/memory_state</tt>. Functions no longer take <tt>~with_alarms</tt> arguments. Instead, they return booleans, that indicate an alarm occurred.</li> -<li class="dev-break"> Function <tt>Cvalue.Model.find</tt> does *not* signal its result is indeterminate anymore. Use function <tt>Cvalue.Model.find_unspecified</tt> instead.</li> -<li class="dev-break"> Multiple low-level functions have been removed from modules <tt>Cvalue.V</tt> and <tt>Cvalue.Model</tt>, and are no longer available.</li> -<li class="dev"> Argument <tt>~conflate_bottom</tt> to <tt>Cvalue.Model.find</tt> is now optional. The documentation has been updated to better explain its meaning.</li> -<li class="dev-break"> Some functions of modules Offsetmap, Lmap, <tt>Cvalue.V_Offsetmap</tt> and <tt>Cvalue.Model</tt> now require a separate <tt>Locations.Location_Bits.t</tt> and (integer) size, instead of a <tt>Locations.location</tt>. This avoids errors when the case was <tt>Int_Base.Top</tt>.</li> -<li class="dev-break"> Functions find_base and find_base_or_default in modules Lmap and <tt>Cvalue.Model</tt> now return an optional type, to account for invalid bases (that may not be present in the map).</li> -<li class="dev-break"> Improve and clarify the return conventions of modules Offsetmap, Lmap, <tt>Cvalue.V_Offsetmap</tt> and <tt>Cvalue.Model</tt>, by returning three cases: `Bottom, `Top and `Map. The latter case indicates the operation succeeded precisely'.</li> -<li class="dev-break"> API of module <tt>Cvalue.V_Or_Uninitialized</tt> is now type-safe. Replace all occurrences of 'get_flags v' by 'v'.</li> -<li class="dev-break"> Most iterators of module Lmap and <tt>Cvalue.Model</tt> now accept only the non-bottom and non-top cases.</li> -<li class="dev-break"> Value 'empty' is no longer exported in module Offsetmap. The API should prevent any accidental creation.</li> -<li class="dev-break"> Garbled mix (constructor Top in modules <tt>Location_Bits/Bytes</tt>) now explicitly mention the NULL base.</li> -<li class="dev-break"> Remove experimental support for periodic bases.</li> -</ul> -</div> -<hr><div><a id="Neon-10.0" href="#Neon-10.0"></a></div><h3 class="release">Neon Release <span class="hversion">[10.0]</span></h3> - -<div class="release"> -<h2>Frama-C General</h2> -<h4>New Features</h4> -<ul class="entries"> -<li class="user"><span class="kernel">[Configure]</span>  New option <tt>--disable-local-ocamlgraph</tt> to disable the use of the OcamlGraph version provided by Frama-C.</li> -<li class="user-break"><span class="kernel">[Journal]</span>  By default, the journal is now generated into the Frama-C session directory.</li> -<li class="user-break"><span class="kernel">[Kernel]</span>  Support parsing and printing <tt>"asm goto"</tt> from gcc <tt>4.6</tt>. Added a component to <tt>Cil_types.Asm</tt> constructor.</li> -<li class="user"><span class="kernel">[Kernel]</span>  The annotation 'loop pragma UNROLL <tt>"done"</tt>, n;' disables the unrolling of the annoted loop. Option <tt>-ulevel-force</tt> has to to used for enabling the transformation of such a loop. This pragma is introduced by the unrolling process in order to prevent unrolling on source code obtained by a previous frama-C run.</li> -<li class="user"><span class="kernel">[Kernel]</span>  Better strategy when <tt>-save</tt> is set and Frama-C crashes (bts <a class="public" href="http://bts.frama-c.com/view.php?id=1388">#1388</a>).</li> -<li class="user-break"><span class="kernel">[Kernel]</span>  Renamed argument <tt>~cache</tt> of functions cached_fold into <tt>~cache_name</tt>. The previous integer is no longer used.</li> -<li class="user"><span class="kernel">[Kernel]</span>  An 'unknown' local status is set on assigns generated from the C prototype of leaf functions</li> -<li class="user"><span class="kernel">[Kernel]</span>  Add <tt>-aggressive-merging</tt> option to merge two inline functions if they are equal modulo alpha conversion.</li> -<li class="user"><span class="kernel">[Kernel]</span>  Support for static evaluation of the __builtin_compatible_p GCC specific function.</li> -<li class="user"><span class="kernel">[Kernel]</span>  Generate more aggressive assigns clauses for unspecified library functions that arguments with type pointer to void or char</li> -<li class="user"><span class="kernel">[Kernel]</span>  Support for binary literal constants in C and in logic denoted by '0[bB][01]+' (common <tt>ISO/C</tt> extension).</li> -<li class="user"><span class="kernel">[Kernel]</span>  <tt>"-machdep help"</tt> now specifies the default machdep (bts <a class="private" href="http://bts.frama-c.com/view.php?id=1558">#1558</a>).</li> -<li class="user"><span class="kernel">[Kernel]</span>  FRAMAC_PLUGIN may now specify a list of comma-separated directories instead of a single one.</li> -<li class="user"><span class="kernel">[Kernel]</span>  Assigns clauses generated by the kernel for functions with neither a specification nor a body receive an 'Unknown' status.</li> -<li class="user"><span class="kernel">[Logic]</span>  Improve localisation of error messages during logic typing.</li> -</ul> -<h4>Bug Fixes</h4> -<ul class="entries"> -<li class="bugfix"><span class="kernel">[Cil]</span>  Do not pretty-print while(1) into while(c) when the 'break' branch is not reduced to a single break, or contains an annotation</li> -<li class="bugfix"><span class="kernel">[Cil]</span>  Fixes issue <a class="public" href="http://bts.frama-c.com/view.php?id=1589">#1589</a> (do not drop access to volatile lvals in pure expressions).</li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Fix pretty-printing of comments in ghost code (bts <a class="public" href="http://bts.frama-c.com/view.php?id=1378">#1378</a> and <a class="public" href="http://bts.frama-c.com/view.php?id=1404">#1404</a>).</li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Fix incorrect dot output of consolidation graph of property statuses.</li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Fix consolidation algorithm of property statuses which possibly occurs on cycles involving an unproved property (bts <a class="public" href="http://bts.frama-c.com/view.php?id=1443">#1443</a>).</li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  implicit annotation status is not lost through code transformations anymore. Fixes bug <a class="private" href="http://bts.frama-c.com/view.php?id=1442">#1442</a></li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  more informative error message. Fixes bug <a class="public" href="http://bts.frama-c.com/view.php?id=1352">#1352</a></li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Tmp vars created during typecheck all have a description. Fixes bug <a class="private" href="http://bts.frama-c.com/view.php?id=1387">#1387</a></li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  designated initializers are correctly pretty-printed. Fixes issue <a class="public" href="http://bts.frama-c.com/view.php?id=1457">#1457</a></li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  More clever merge of function contracts. Fixes issue <a class="public" href="http://bts.frama-c.com/view.php?id=1455">#1455</a></li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Fixes binding of formals when linking static prototypes. Fixes issue <a class="public" href="http://bts.frama-c.com/view.php?id=1475">#1475</a></li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Fixes issue <a class="public" href="http://bts.frama-c.com/view.php?id=1451">#1451</a> about <tt>-unicode</tt> which was not taken into account by <tt>-load-script</tt>.</li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Reject identifiers in the same namespace and same scope, according to C standard's rules. fixes bug <a class="public" href="http://bts.frama-c.com/view.php?id=1330">#1330</a>.</li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Statements with a label attached to them are never erased during elaboration. Fixes <a class="public" href="http://bts.frama-c.com/view.php?id=1502">#1502</a>.</li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Correctly distinguish typenames and declared identifiers in declarations. Fixes <a class="public" href="http://bts.frama-c.com/view.php?id=1500">#1500</a></li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Do not generate invalid assigns clauses when some formals are pointers to arrays</li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Do not consider array variable as read lval in unspecified sequence. It can't be written anyway. Fixes <a class="private" href="http://bts.frama-c.com/view.php?id=1519">#1519</a></li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Do not fail on nested ternary operators whose value is dropped, as in <a class="public" href="http://bts.frama-c.com/view.php?id=1503">#1503</a></li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Fixes loop unrolling having in their body 'switch' with 'continue' stmts.</li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  The parsed value could be wrong and the warning for inexact decimal floating-point constants be wrongly omitted for constants smaller than the smallest subnormal.</li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Fix bug which may occur when pretty printing range of terms.</li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Fixed parsing bug with decimal single-precision floating-point literals representing numbers above MAX_FLOAT.</li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Fix typing of variadic arguments.</li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Fix <tt>-machdep</tt> help in presence of other actions (bts <a class="public" href="http://bts.frama-c.com/view.php?id=1643">#1643</a>).</li> -<li class="bugfix"><span class="kernel">[Logic]</span>  Conversion from C array to pointers do not lose cast on pointed types. Fixes issue <a class="public" href="http://bts.frama-c.com/view.php?id=1469">#1469</a></li> -<li class="bug-break"><span class="kernel">[Logic]</span>  Disallow cyclic logic type definitions</li> -<li class="bugfix"><span class="kernel">[Logic]</span>  Accept struct with same name as typedef in specs. Fixes <a class="public" href="http://bts.frama-c.com/view.php?id=1518">#1518</a></li> -<li class="bugfix"><span class="kernel">[Logic]</span>  Do not remove labels out of scope of annotations too quickly. Fixes <a class="public" href="http://bts.frama-c.com/view.php?id=1536">#1536</a></li> -<li class="bug-break"><span class="kernel">[Logic]</span>  <tt>-check</tt> checks that C and associated logic variable agree on their type. transfer completion of type up to associated logic var and term when needed. Fixes <a class="public" href="http://bts.frama-c.com/view.php?id=1538">#1538</a></li> -<li class="bugfix"><span class="kernel">[Logic]</span>  do not cast an enum value toward its associated integral type when comparing to an enum constant. Fixes <a class="private" href="http://bts.frama-c.com/view.php?id=1546">#1546</a></li> -<li class="bugfix"><span class="kernel">[Logic]</span>  Support for _Bool in ACSL formulas</li> -<li class="bugfix"><span class="kernel">[Project]</span>  Fix messages about projects.</li> -</ul> -<h4>Developers Only</h4> -<ul class="entries"> -<li class="dev-break"><span class="kernel">[Cil]</span>  Rename function sizeOf_int into bytesSizeOf.</li> -<li class="dev"><span class="kernel">[Cil]</span>  Statements containing calls to va_start can now be printed outside of a function</li> -<li class="dev"><span class="kernel">[Cil]</span>  Terms containing ACSL keywords are now properly parsed by function <tt>Logic_lexer.lexpr</tt></li> -<li class="dev"><span class="kernel">[Doc]</span>  Fix ugly display of documentation of dynamic plug-ins API (bts <a class="private" href="http://bts.frama-c.com/view.php?id=1394">#1394</a>).</li> -<li class="dev"><span class="kernel">[Kernel]</span>  adding a category do not set debugging level to 1. Conversely debug <tt>~dkey</tt> <tt>"..."</tt> (without <tt>~level</tt>) will output <tt>"..."</tt> if dkey is requested by the user, even if debugging level is 0.</li> -<li class="dev"><span class="kernel">[Kernel]</span>  Add hook builders for hooks that can have dependencies. See <tt>src/lib/hook.mli</tt></li> -<li class="dev"><span class="kernel">[Kernel]</span>  Add hooks to register transformation to be performed on a freshly computed AST. See <tt>src/kernel/file.mli</tt></li> -<li class="dev"><span class="kernel">[Kernel]</span>  Added <tt>StringList.append_</tt>{{ "{" }}before,after} for manipulating options (both static and dynamic API)</li> -<li class="dev"><span class="kernel">[Kernel]</span>  Added hooks when <tt>registering/removing</tt> a property</li> -<li class="dev"><span class="kernel">[Kernel]</span>  <tt>Cil.mkEmptyStmt</tt> gets a valid_sid argument in order to generate valid statements.</li> -<li class="dev"><span class="kernel">[Kernel]</span>  Fixed buggy function <tt>Property.location</tt>.</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  Alpha.{{ "{" }}new,register}AlphaName: transform labelled argument 'undolist' with option type into optional argument.</li> -<li class="dev"><span class="kernel">[Kernel]</span>  Plug-ins may now have their own session directory in which they can generate project-dependent files during a Frama-C session.</li> -<li class="dev"><span class="kernel">[Kernel]</span>  Plug-ins may now have their own configuration directory in which they can generate configuration files during a Frama-C session.</li> -<li class="dev"><span class="kernel">[Kernel]</span>  parameters can be preserved across project creation through copy visitor (do_not_reset_on_copy function). fixes do_not_projectify and do_not_reset_on_copy status of Kernel's options.</li> -<li class="dev"><span class="kernel">[Kernel]</span>  Plug-ins may now have a non-empty .mli interface. It deprecates the old way to register them through module Db or Dynamic (this last one may remain useful for mutually recursive plug-ins).</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  For building a datatype, you now need to use smart constructors provided in Structural_descr.</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  Removed <tt>Db.Dominators</tt>. Use the Dominators kernel module instead.</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  Changes to the signatures in lattice_type: top and bottom are now optional, a join_and_is_included function is required, and Upper_Semi_Lattice was renamed to Join_Semi_Lattice.</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  The module Parameter_sig now contains the signatures of command line options (was in module Plugin).</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  Parameter is now called Typed_parameter.</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  The module Parameter_customize now contains the functions to customize command line options (was in module Plugin).</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  The module Parameter_state now contains the functions to select group of parameters (was in module Plugin).</li> -<li class="dev"><span class="kernel">[Lib]</span>  <tt>Filepath.normalize</tt> can replace paths by a symbolic name.</li> -<li class="dev"><span class="kernel">[Logic]</span>  Better specification and more checks on Annotations.{{ "{" }}add,remove}_* functions (fixes bug <a class="private" href="http://bts.frama-c.com/view.php?id=1635">#1635</a>).</li> -<li class="dev-break"><span class="kernel">[Makefile]</span>  Split <tt>Makefile.common</tt> in two parts in order to include generic rules (new <tt>Makefile.generic</tt> file) at the end of main Makefile, so specialized patterns will be considered first in make < <tt>v3.82</tt></li> -<li class="dev"><span class="kernel">[Ptests]</span>  add the possibility to define macros in configurations. See developer documentation.</li> -<li class="dev"><span class="kernel">[Ptests]</span>  Use <tt>ptests.opt</tt> whenever possible.</li> -</ul> -<h2>Frama-C GUI</h2> -<ul class="entries"> -<li class="user-break"><span class="kernel">[Gui]</span>  the configuration file .<tt>frama-c-gui.config</tt> is now put in the GUI config directory and named <tt>frama-c-gui.config</tt>.</li> -</ul> -<h2>Plugin From</h2> -<h4>New Features</h4> -<ul class="entries"> -<li class="user"> Slowndowns in the analyses can be mitigated using higher values for option <tt>-memory-footprint</tt></li> -<li class="user"> Better precision when querying information about a zone that has the same dependencies as its neighbors.</li> -<li class="user-break"> Separately compute data dependencies and indirect (address, control) dependencies with option <tt>-show-indirect-deps</tt></li> -<li class="user"> Fix possibly invalid dependencies for functions that return partially-written structs.</li> -</ul> -<h4>Bug Fixes</h4> -<ul class="entries"> -<li class="bugfix"> Position the 'and SELF' flag when an assigns clause z1 and z2 overlap in an assigns clause z1 <tt>\from</tt> z2 .</li> -<li class="bugfix"> Fix incorrect dependencies with code of the form 'f(); x = 1; f();' when f assigns a value with a right-hand side that depends on x.</li> -</ul> -<h4>Developers Only</h4> -<ul class="entries"> -<li class="dev-break"> Results of From cannot be intercepted by <tt>Log.add_listener</tt> anymore. Use <tt>Db.From</tt>.{{ "{" }}pretty,display} to print them.</li> -</ul> -<h2>Plugin Impact</h2> -<ul class="entries"> -<li class="user-break"> More generic dynamic function impact_statement_gui. The set of nodes impacted can now be filtered by a memory zone.</li> -</ul> -<h2>Plugin Inout</h2> -<ul class="entries"> -<li class="user-break"> Inputs of an instruction whose evaluation fails now include the sub-expressions for which evaluation succeeds</li> -</ul> -<h2>Plugin Metrics</h2> -<ul class="entries"> -<li class="user"> More precise information about coverage</li> -<li class="user"> ACSL statistics</li> -</ul> -<h2>Plugin Obfuscator</h2> -<h4>New Features</h4> -<ul class="entries"> -<li class="user"> Print the category which each symbol belongs to (bts <a class="private" href="http://bts.frama-c.com/view.php?id=1566">#1566</a>).</li> -<li class="user"> Obfuscate labels (bts <a class="public" href="http://bts.frama-c.com/view.php?id=1562">#1562</a>).</li> -<li class="user"> Obfuscate (most of) logical constructs (bts <a class="public" href="http://bts.frama-c.com/view.php?id=1563">#1563</a>).</li> -<li class="user"> Handle literal strings in a separate dictionary (bts <a class="private" href="http://bts.frama-c.com/view.php?id=1564">#1564</a>).</li> -<li class="user"> Warn about unobfuscated symbols.</li> -<li class="user"> New option <tt>-obfuscator-dictionary</tt> to generate the dictionary into a file.</li> -<li class="user"> New option <tt>-obfuscator-string-dictionary</tt> to generate the dictionary of literal strings into a separated file.</li> -</ul> -<h4>Bug Fix</h4> -<ul class="entries"> -<li class="bugfix"> Now properly handle option <tt>-ocode</tt>.</li> -</ul> -<h2>Plugin PDG</h2> -<ul class="entries"> -<li class="dev"> Function <tt>Db.Pdg.find_stmt_and_blocks_nodes</tt> returns a correct result on partially dead composite statements</li> -</ul> -<h2>Plugin Pdg</h2> -<ul class="entries"> -<li class="bugfix"> Fix possible non-termination during the computation of the control dependencies (bug <a class="public" href="http://bts.frama-c.com/view.php?id=1436">#1436</a>)</li> -<li class="user"> Shorter output when outputting results</li> -<li class="dev-break"> Results of Pdg cannot be intercepted by <tt>Log.add_listener</tt> anymore. Use <tt>Db.Pdg.get</tt> and <tt>Db.Pdg.pretty</tt> instead.</li> -</ul> -<h2>Plugin Report</h2> -<ul class="entries"> -<li class="user"> New option <tt>-report-untried</tt></li> -</ul> -<h2>Plugin RTE</h2> -<ul class="entries"> -<li class="bugfix"> Better normalization when using <tt>-rte-precond</tt>.</li> -<li class="user"> Remove limitation about alarms which do not fit into 64 bits (bts <a class="public" href="http://bts.frama-c.com/view.php?id=1391">#1391</a>).</li> -</ul> -<h2>Plugin Rte</h2> -<ul class="entries"> -<li class="bugfix"> No assertions are generated for unsigned left-shift that may overflow, regardless of whether <tt>-warn-unsigned-overflow</tt> is set. Fixes issue <a class="private" href="http://bts.frama-c.com/view.php?id=1555">#1555</a>.</li> -</ul> -<h2>Plugin Scope</h2> -<ul class="entries"> -<li class="user"> Option <tt>-inout-callwise</tt> can be used to improve the precision of computations, including the effects of option <tt>-remove-redundant-alarms</tt>. Option <tt>-calldeps</tt> is no longer necessary</li> -<li class="dev"> Functions registered in Db now return <tt>Stmt.Hptset</tt> values instead of <tt>Stmt.Set</tt></li> -</ul> -<h2>Plugin Semantic</h2> -<ul class="entries"> -<li class="bugfix"> Constant Folding Fixes error when folding fct pointer resulting in two distinct kf for the same function.</li> -</ul> -<h2>Plugin Slicing</h2> -<h4>New Features</h4> -<ul class="entries"> -<li class="user"> Better slicing of complex logical assertions (bug <a class="public" href="http://bts.frama-c.com/view.php?id=690">#690</a>).</li> -<li class="user"> <tt>-slice-calls</tt> main only selects the calls to the main function, nothing more.</li> -</ul> -<h4>Bug Fixes</h4> -<ul class="entries"> -<li class="bugfix"> Fix crash in presence of assertions involving sizeof(t), where t is an array. Fixes similar bug with option <tt>-remove-redudant-alarms</tt></li> -<li class="bugfix"> Slicing on a composite statement containing dead code now works properly</li> -<li class="bugfix"> Slicing is now compatible with option <tt>-val-use-spec</tt></li> -</ul> -<h2>Plugin Syntactic_callgraph</h2> -<ul class="entries"> -<li class="user-break"> Remove option <tt>-cg-services-only</tt> which was unused since a while.</li> -</ul> -<h2>Plugin Value</h2> -<h4>New Features</h4> -<ul class="entries"> -<li class="user"> Frama_C_show_foo functions now display struct arguments in extenso.</li> -<li class="user"> Distinguish unreachable state and invalid location when printing the value of a l-value in the GUI</li> -<li class="user"> Basic support for <tt>\inter</tt> logical predicate (treated as an union).</li> -<li class="user"> Evaluation of <tt>\base_addr</tt>, <tt>\offset</tt> and <tt>\block_length</tt> logic predicates.</li> -<li class="user"> Preliminary support on <tt>\forall</tt> and <tt>\exists</tt> quantification when the introduced variables have a C type.</li> -<li class="user"> Assertions on dead code now get a "true because unreachable" status.</li> -<li class="user"> The name of an evaluated property is now displayed in the log message. Fixes wish <a class="public" href="http://bts.frama-c.com/view.php?id=1415">#1415</a>.</li> -<li class="user"> Option <tt>-memory-footprint</tt> now accepts much bigger arguments. The size allocated to each cache is multiplied by 2 between each increment.</li> -<li class="user"> Better documentation of module Hptmap. Some incompatible API changes.</li> -<li class="user-break"> Better widening bound for signed 32 bits integers</li> -<li class="user-break"> Fewer and better widening bounds for pointer addresses: try the frontier of the block</li> -<li class="user"> Warn for missing '<tt>\from</tt>' or 'assigns <tt>\result</tt> <tt>\from</tt>' clauses. Fixes wish <a class="public" href="http://bts.frama-c.com/view.php?id=1448">#1448</a></li> -<li class="user"> More aggressive evaluation of <tt>\initialized</tt>(p) when p points to a memory zone containing both bottom and non-bottom values</li> -<li class="user"> Value analysis can now be aborted while keeping intermediate results, by sending SIGUSR1 to Frama-C</li> -<li class="user"> Degeneration points are now shown in the GUI</li> -<li class="user"> Syntactic loops (ie. 'for', 'while' and 'do ... while') are now always used to perform widening, regardless of whether they are reducible</li> -<li class="user"> Evaluation of left-values such as t[i][j] or p->arr[i] is now more precise when the total number of locations to read or write is less than the value of <tt>-plevel</tt> option</li> -<li class="user-break"> No alarms are emitted for overflowing unsigned left shift operations.</li> -<li class="user-break"> Pointer subtraction now requires that the pointers refer to the same allocated block, and returns the pointwise difference between the corresponding offsets. Use <tt>-no-val-warn-pointer-subtraction</tt> to obtain the previous behavior.</li> -<li class="user"> The option <tt>-val-left-shift-negative-alarms</tt> has been renamed into <tt>-val-warn-left-shift-negative</tt></li> -<li class="user-break"> Passing a struct containing uninitialized fields or padding bits to a function without a body no longer raises an alarm.</li> -<li class="user"> Copies of non-struct left-values that contain indeterminate bits can now be reported using option <tt>-val-warn-copy-indeterminate</tt>.</li> -<li class="user"> Improve precision of bitwise conversion from floating-point value to integers</li> -<li class="user"> Experimental option <tt>-slevel-merge-after-loop</tt></li> -<li class="user-break"> Volatile pointers are now modeled as the base addresses that are stored into the pointer, shifted by an unspecified offset.</li> -<li class="user"> Display information about temporaries when emitting an alarm</li> -<li class="user"> Ensure convergence in presence of some non-natural loops</li> -<li class="user"> Improve precision of treatment of: if ((int)floatvar == intexpr)</li> -<li class="user"> Improve precision of treatment of x = e1 & e2;</li> -<li class="user-break"> Replace mostly-inoperant option <tt>-memory-footprint</tt> by an environment variable FRAMA_C_MEMORY_FOOTPRINT</li> -<li class="user"> Fix spurious messages about integer overflow when an arithmetic operation is guaranteed to result in an undefined behavior.</li> -<li class="user"> For functions for which only the specification is available, non-invalid statuses are no longer reported when evaluating a postcondition. Invalid statuses are reported, and usually indicate a specification error.</li> -</ul> -<h4>Bug Fixes</h4> -<ul class="entries"> -<li class="bugfix"> Failure during a memory zone copy is now properly notified. Alarms were emitted, but a non-bottom result was simultaneously returned.</li> -<li class="bugfix"> Fix crash when the creation of the initial state encounters a completely invalid compound initializer.</li> -<li class="bugfix"> Fix crash when evaluating <tt>\valid</tt>(p->off) when p is NULL or a valid pointer, and p->off is itself only partially valid (bug <a class="public" href="http://bts.frama-c.com/view.php?id=1486">#1486</a>).</li> -<li class="bugfix"> Fixed bug involving the conversion to float of a double expression e <tt>s.t</tt>. 0 < fabs(e) <= <tt>0x1.0p-150</tt>.</li> -<li class="bugfix"> Prevent GUI crashes when options <tt>-no-results</tt> or <tt>-obviously-terminates</tt> are set and some functions have ACSL preconditions</li> -<li class="bugfix"> Ensures that sqrt(-0.) is -0., even with buggy MSVC runtime. Fixes bug <a class="private" href="http://bts.frama-c.com/view.php?id=1396">#1396</a></li> -<li class="bugfix"> Fix potentially invalid source line number in origin of Merge garbled mix values.</li> -<li class="bugfix"> Fix rare crash during widening operation in C union intensive code</li> -<li class="bugfix"> Fix possible unsoundness in presence of &. (unsoundness never observed in practice)</li> -<li class="bugfix"> Fix crash on analyses involving very imprecise pointers and a partially valid absolute memory range</li> -<li class="bugfix"> Fix missing <tt>read/written</tt> zones and dependencies when accessing a completely imprecise pointer (garbled mix) and using option <tt>-absolute-valid-range</tt>. Impacts the results of plugins Inout, From, Pdg, Impact and Slicing.</li> -<li class="bugfix"> Fixed spurious warning about floating-point values containing addresses.</li> -<li class="bugfix"> Remove support for ACSL <tt>\inter</tt> operator, which could lead to unsoundness with predicates involving the empty set (fixes bug <a class="private" href="http://bts.frama-c.com/view.php?id=1624">#1624</a>)</li> -<li class="bugfix"> Fix potential unsoundness in the operation testing the inclusion of two memory states (never observed in practice)</li> -<li class="bugfix"> Fix bug when writing imprecisely in a struct containing a 1<tt>-bit</tt> wide bitfield (bug <a class="private" href="http://bts.frama-c.com/view.php?id=1671">#1671</a>)</li> -</ul> -<h4>Developers Only</h4> -<ul class="entries"> -<li class="dev-break"> Remove functions <tt>Cvalue.Model.pretty_without_null</tt> and <tt>Db.Value.display_globals</tt>. Function <tt>Db.Value.display</tt> is now a reference to the real function. Removed last argument of <tt>Cvalue.Model.pretty_filter</tt>.<br/><br/></li> -<li class="dev-break"> Results of Value cannot be intercepted by <tt>Log.add_listener</tt> anymore. Use <tt>Db.Value.display</tt> to print them</li> -<li class="dev-break"> Do not crash when printing arrays or structs containing abstract structs (bug <a class="public" href="http://bts.frama-c.com/view.php?id=1416">#1416</a>).</li> -<li class="dev-break"> API change in module Base. Use script <tt>bin/fluorine2neon.sh</tt> for automatic migration.</li> -<li class="dev-break"> Function <tt>Cvalue.Model.find_unspecified</tt> now requires one additional argument <tt>~conflate_bottom</tt></li> -<li class="dev"> Fix bug in which two distinct memory states could be erroneously made equal</li> -<li class="dev"> Minor signature change for widening functions</li> -<li class="dev-break"> Function <tt>Map_Lattice.Make</tt> requires a new argument</li> -<li class="dev"> Type <tt>Base.string_id</tt> is now concrete. No more need for function <tt>Base.cstring_of_string_id</tt></li> -<li class="dev-break"> Functions previously required by some functors in directories <tt>src/ai</tt> and <tt>src/memory_state</tt> are no longer needed. Use script <tt>bin/fluorine2neon.sh</tt> for partially automatic migration.</li> -<li class="dev-break"> Harmonisation and simplifications of functions related to memory states in <tt>Cvalue.Model</tt>. Different functions are now available for updating, refining and creating a state</li> -</ul> -</div> -<hr><div><a id="Fluorine-9.2" href="#Fluorine-9.2"></a></div><h3 class="release">Fluorine Release <span class="hversion">[9.2]</span></h3> - -<div class="release"> -<h2>Plugin Value</h2> -<ul class="entries"> -<li class="bugfix"> Add missing C library files.<br/><br/></li> -</ul> -</div> -<hr><div><a id="Fluorine-9.1" href="#Fluorine-9.1"></a></div><h3 class="release">Fluorine Release <span class="hversion">[9.1]</span></h3> - -<div class="release"> -<h2>Frama-C General</h2> -<ul class="entries"> -<li class="dev"><span class="kernel">[Kernel]</span>  Fixed <tt>Type.pp_ml_name</tt> for polymorphic types with 3 and 4 type variables (bug <a class="public" href="http://bts.frama-c.com/view.php?id=1127">#1127</a>).</li> -<li class="bugfix"><span class="kernel">[Makefile]</span>  Fixed installation directory of the doc in plug-in's Makefile (bug <a class="public" href="http://bts.frama-c.com/view.php?id=1278">#1278</a>).<br/><br/></li> -</ul> -<h2>Plugin RTE</h2> -<ul class="entries"> -<li class="bugfix"> Fix off-by-one error in alarms on overflowing unsigned unary minuses.</li> -</ul> -<h2>Plugin Value</h2> -<ul class="entries"> -<li class="user"> Better precision for ^ (bitwise xor) operator when applied on intervals of positive integers</li> -<li class="bugfix"> Catch evaluation errors when selecting a logic l-value in the GUI.</li> -</ul> -</div> -<hr><div><a id="Fluorine-9.0" href="#Fluorine-9.0"></a></div><h3 class="release">Fluorine Release <span class="hversion">[9.0]</span></h3> - -<div class="release"> -<h2>Frama-C General</h2> -<h4>New Features</h4> -<ul class="entries"> -<li class="user"><span class="kernel">[Cil]</span>  The type of fields that are bit-fields now carry an informative attribute FRAMA_C_BITFIELD_SIZE.</li> -<li class="user"><span class="kernel">[Cil]</span>  Handles interpretation of linemarker ending by // and cleanup file paths.</li> -<li class="user"><span class="kernel">[Kernel]</span>  Assumptions and axioms now get consolidated status <tt>"Considered valid"</tt> instead of <tt>"Valid"</tt>.</li> -<li class="user"><span class="kernel">[Kernel]</span>  Option <tt>-enums</tt> for choosing representation of enums.</li> -<li class="user"><span class="kernel">[Kernel]</span>  When printing the AST, display the emitter name of generated annotations and also the origin of annotations corresponding to an alarm.</li> -<li class="user"><span class="kernel">[Kernel]</span>  Better <tt>frama-c.top</tt> (fixed issue <a class="public" href="http://bts.frama-c.com/view.php?id=1287">#1287</a>).</li> -<li class="user"><span class="kernel">[Kernel]</span>  Syntactic constant folding is done once by AST (fixed bug <a class="private" href="http://bts.frama-c.com/view.php?id=1306">#1306</a>).</li> -<li class="user"><span class="kernel">[Kernel]</span>  The level of verbose is at least the level of debug.</li> -<li class="user"><span class="kernel">[Kernel]</span>  Print signed downcast alarms as 'signed_downcast'</li> -<li class="user-break"><span class="kernel">[Kernel]</span>  Signed downcast alarms are no longer emitted by default. Use option <tt>-warn-signed-downcast</tt> to activate them.</li> -<li class="user-break"><span class="kernel">[Kernel]</span>  Signed overflow alarms are now emitted by default.</li> -<li class="user"><span class="kernel">[Logic]</span>  Extended syntax for naming terms and predicates (<tt>"string"</tt>:pred and <tt>"string"</tt>:term are now allowed).</li> -<li class="user"><span class="kernel">[Logic]</span>  Improved merge strategy for assigns, and report the presence of different assigns clauses between two files.</li> -</ul> -<h4>Bug Fixes</h4> -<ul class="entries"> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Fixed bug with <tt>Type.pp_ml_name</tt> for pairs, triples and quadruples which can lead to incorrect journal generation (new occurrence of bts <a class="public" href="http://bts.frama-c.com/view.php?id=1127">#1127</a>).</li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Do not attempt to merge unrelated anonymous enum that have been given the same name by Cil (fixes <a class="public" href="http://bts.frama-c.com/view.php?id=1283">#1283</a>).</li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Do not print help of negative options when the positive one is invisible (fixed <a class="public" href="http://bts.frama-c.com/view.php?id=1295">#1295</a>).</li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Fixed discrepancy between compare_type and hash_type. Added new datatype TypNoUnroll.</li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Fixed bug <a class="private" href="http://bts.frama-c.com/view.php?id=1347">#1347</a> about accessing to a consolidated status of a property which depends on removed hypotheses.</li> -<li class="bug-break"><span class="kernel">[Kernel]</span>  Add lv_kind field to trace origin of logic variables. <tt>Cil_const.make_logic_var</tt> is deprecated in favor of specialized.</li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Ghost status is appropriately propagated in statements (instead of only instructions) and pretty-printed accordingly. Fixes issue <a class="public" href="http://bts.frama-c.com/view.php?id=1328">#1328</a>.</li> -<li class="bugfix"><span class="kernel">[Logic]</span>  Fixes various type-checking issues in presence of polymorphism and implicit conversions (including <a class="public" href="http://bts.frama-c.com/view.php?id=1146">#1146</a>).</li> -<li class="bugfix"><span class="kernel">[Makefile]</span>  Compile OcamlGraph less often: fixes issue <a class="public" href="http://bts.frama-c.com/view.php?id=1343">#1343</a>.</li> -</ul> -<h4>Developers Only</h4> -<ul class="entries"> -<li class="dev-break"><span class="kernel">[Cil]</span>  Remove unused 'alignof_char_array' machdep field.</li> -<li class="dev-break"><span class="kernel">[Cil]</span>  Renamed function <tt>Cil.alignOf_int</tt> into bytesAlignOf.</li> -<li class="dev-break"><span class="kernel">[Cil]</span>  Clean up registering of new machdeps. Some machdep options have been integrated into <tt>Cil_types.mach</tt>, or removed from <tt>Cil.theMachine</tt> (as they were already in <tt>Cil_types.mach</tt>).</li> -<li class="dev-break"><span class="kernel">[Cil]</span>  Remove Cil pretty-printer. Use module Printer instead. The script <tt>bin/oxygen2fluorine.sh</tt> may be used to automatically convert your code.</li> -<li class="dev"><span class="kernel">[Kernel]</span>  Fixed consistency check of descriptor when building polymorphic datatypes (fixed bts <a class="public" href="http://bts.frama-c.com/view.php?id=1277">#1277</a>).<br/><br/></li> -<li class="dev"><span class="kernel">[Kernel]</span>  Provide <tt>Datatype.triple</tt> and <tt>Datatype.quadruple</tt> (bts wish <a class="public" href="http://bts.frama-c.com/view.php?id=1277">#1277</a>).</li> -<li class="dev"><span class="kernel">[Kernel]</span>  Optional argument 'reorder' to File.* functions creating an AST in a new project from a visitor.</li> -<li class="dev"><span class="kernel">[Kernel]</span>  Fixes incorrect visitor behavior with JustCopy (issue <a class="public" href="http://bts.frama-c.com/view.php?id=1282">#1282</a>).</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  New API for module Alarms.</li> -<li class="dev"><span class="kernel">[Kernel]</span>  New function 'get' for projectified counters.</li> -<li class="dev"><span class="kernel">[Kernel]</span>  Renamed <tt>Kernel_function.self</tt> to <tt>Kernel_function.auxiliary_kf_stmt_state</tt> to avoid confusion.</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  Get rid of useless rooted_code_annotation datatype.</li> -<li class="dev"><span class="kernel">[Kernel]</span>  New function <tt>Annotations.model_fields</tt>.</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  Signature change for constructor LReal.</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  Remove unintuitive ?prj argument from Cil visitors, and first argument of <tt>Visitor.generic_frama_c_visitor</tt>. Information is now stored inside the type <tt>Cil.visitor_behavior</tt>.</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  Added TLogic_coerce constructor to mark explicitly a conversion from a C type to a logical one (in particular floating point -> real and integral -> integer). Fixes issue <a class="public" href="http://bts.frama-c.com/view.php?id=1309">#1309</a>.</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  Various types whose names started by t_ in <tt>PDG/slicing</tt> related modules are now unprefixed.</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  Remove Cilutil's pretty printing helpers. Use Pretty_utils' ones instead.</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  Reorganize AST's pretty-printers. You must now use module Printer. Use the script <tt>oxygen2fluorine.sh</tt> to upgrade your plug-in.</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  Module Cilutil has been removed. Previously used list functions can now be found in Extlib (use script <tt>oxygen2fluorine.sh</tt> for migration). Functions related to configuration files are now Cilconfig.</li> -<li class="dev"><span class="kernel">[Kernel]</span>  Added type modules <tt>Cil_datatype.Wide_string</tt> and <tt>Datatype.List_with_collections</tt>.</li> -<li class="dev"><span class="kernel">[Kernel]</span>  Added pp_field and pp_model_field in Printer_api.</li> -<li class="dev"><span class="kernel">[Kernel]</span>  New methods videntified_term and videntified_predicate for the visitor.</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  Remove method is_annot_before from visitors (it return only 'true').</li> -<li class="dev"><span class="kernel">[Kernel]</span>  Visitor no longer crashes when a non-function global is replaced by a list containing at least one function or prototype (fixes bug <a class="private" href="http://bts.frama-c.com/view.php?id=1349">#1349</a>).</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  redesign of message categories. See detailed changelog for more information.</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  Must register keywords introducing new clauses of ACSL contracts. Fixes issue <a class="private" href="http://bts.frama-c.com/view.php?id=1358">#1358</a>.</li> -<li class="dev-break"><span class="kernel">[Logic]</span>  Change <tt>Property_status.Consolidation_graph.dump</tt> now takes a formatter instead of a file name.</li> -<li class="dev"><span class="kernel">[Makefile]</span>  Fix installation directory of API documentation (fixed bts <a class="public" href="http://bts.frama-c.com/view.php?id=1278">#1278</a>).</li> -</ul> -<h2>Frama-C GUI</h2> -<ul class="entries"> -<li class="bugfix"><span class="kernel">[Gui]</span>  In some cases, after a crash of an analyzer, the GUI was not fully restored, became inconsistent and could crash.</li> -</ul> -<h2>Plugin Aorai</h2> -<ul class="entries"> -<li class="bugfix"> Adds locations modified by Aorai to existing loop assigns (fixes issue <a class="public" href="http://bts.frama-c.com/view.php?id=1290">#1290</a>).</li> -</ul> -<h2>Plugin From</h2> -<ul class="entries"> -<li class="bugfix"> Fix rare bug in presence of involved control-flow graphs and non-terminating calls.</li> -<li class="bugfix"> Fix absence of effect of option <tt>-calldeps</tt> after a <tt>save/load</tt> cycle.</li> -</ul> -<h2>Plugin Impact</h2> -<ul class="entries"> -<li class="bugfix"> Prevent crash when a caller or callee function has been imprecisely analyzed.</li> -<li class="bugfix"> Prevent crash when considering a function with an unreachable first statement.</li> -<li class="dev-break"> Function <tt>Db.Impact.compute_pragmas</tt> now returns a list of statements.</li> -</ul> -<h2>Plugin Inout</h2> -<ul class="entries"> -<li class="bugfix"> Fix absence of effect option <tt>-inout-callwise</tt> after a <tt>save/load</tt> cycle.</li> -<li class="user"> Indirect reads (for example 'p' for '*p') are now automatically added to inputs when evaluating assigns.</li> -</ul> -<h2>Plugin Metrics</h2> -<ul class="entries"> -<li class="bugfix"> Global variables both declared and defined were counted twice.</li> -<li class="bugfix"> Option <tt>-value-metrics</tt> now report a correct location for function referenced by an initializer. Fixes <a class="private" href="http://bts.frama-c.com/view.php?id=1361">#1361</a>.</li> -</ul> -<h2>Plugin Obfuscator</h2> -<ul class="entries"> -<li class="user"> Hide variables that do not appear in the output from the dictionary.</li> -</ul> -<h2>Plugin Pdg</h2> -<ul class="entries"> -<li class="user"> Ignore inline asm statements (previous behavior was to generate Top Pdgs).</li> -<li class="user"> InCtrl nodes are no longer displayed in Dot graphs.</li> -<li class="dev"> Fix display for control dependencies in PDG graphs.</li> -</ul> -<h2>Plugin Rte</h2> -<h4>New Features</h4> -<ul class="entries"> -<li class="user-break"> Remove option <tt>-rte-print</tt>. Use <tt>-print</tt> instead.</li> -<li class="user"> Generate Value-compatible alarms and annotations.</li> -<li class="user-break"> Removed options <tt>-rte-signed</tt>, rte-unsigned-ov, <tt>-rte-downcast</tt> and <tt>-rte-unsigned-downcast</tt>. They are replaced by <tt>-warn-signed-overflow</tt>, <tt>-warn-unsigned-overflow</tt>, <tt>-warn-signed-downcast</tt> and <tt>-warn-unsigned-downcast</tt> respectively.</li> -</ul> -<h4>Bug Fix</h4> -<ul class="entries"> -<li class="bugfix"> Added missing alarm for casts from overly large floating-point numbers to integer. Fixes <a class="private" href="http://bts.frama-c.com/view.php?id=1318">#1318</a>.</li> -</ul> -<h4>Developers Only</h4> -<ul class="entries"> -<li class="dev"> Export function <tt>"exp_annotations"</tt> to get RTEs of a C expression as annotations.</li> -</ul> -<h2>Plugin Scope</h2> -<ul class="entries"> -<li class="bugfix"> Prevent crash in defs computation when a lvalue is a formal.</li> -</ul> -<h2>Plugin Slicing</h2> -<ul class="entries"> -<li class="bugfix"> Fix incorrectness in presence of assertions involving <tt>\initialized</tt> predicate. User predicates are no longer treated.</li> -<li class="bugfix"> Fix options <tt>-slice-assert</tt> and <tt>-slice-threat</tt> (<tt>-threat</tt> did nothing, <tt>-assert</tt> selected all alarms).</li> -<li class="dev-break"> Remove no longer used <tt>~ai</tt> argument.</li> -<li class="user-break"> Alarms are now removed in the generated project (regardless of option <tt>-slicing-keep-annotations</tt>).</li> -</ul> -<h2>Plugin Sparecode</h2> -<ul class="entries"> -<li class="user-break"> Alarms are now ignored during the analysis.</li> -<li class="user-break"> RTE or Value-generated alarms are now removed in the generated project.</li> -</ul> -<h2>Plugin Value</h2> -<h4>New Features</h4> -<ul class="entries"> -<li class="user"> Reduce more aggressively on accesses *p where p is imprecise but contains only one valid value.</li> -<li class="user"> New option <tt>-val-callstack-results</tt> to record and display in GUI the results split by callstacks.</li> -<li class="user"> More precise line numbers for statuses of assertions and loop invariants.</li> -<li class="user"> Improve handling of conditionals when option <tt>-val-ilevel</tt> is used.</li> -<li class="user"> Evaluation of assigns now include indirect reads (ie 'assigns *p' depends on p) automatically.</li> -<li class="user"> More agressive analysis of statements with improperly sequenced accesses when option <tt>-unspecified-access</tt> is used.</li> -<li class="user"> More aggressive reduction in presence of write through partially invalid pointers. Warn if the pointer is completely invalid.</li> -<li class="user"> Alarms emitted by Value are no longer evaluated during analysis (unlike user assertions).</li> -<li class="user"> Value more aggressive evaluation of construct '//@ for b: assert p' when b is guaranteed to be active. Harmonize behaviors-related messages.</li> -<li class="user"> Improved support for abstract structs.</li> -<li class="user"> Improve reduction by conditions that involve '&' and '|' operators.</li> -<li class="user"> Suppress superfluous warning when passing as argument a struct that contains pointers.</li> -<li class="user"> Offsets in misaligned values that repeat themselves are now always printed relatively to the beginning of the binding.</li> -<li class="user-break"> Renamed options <tt>-initialized-padding-globals</tt> and <tt>-no-no-results</tt> into <tt>-uninitialized-padding-globals</tt> and <tt>-val-store-results</tt> respectively.</li> -<li class="user"> Improved support for va_arg variadic macro.</li> -<li class="user"> Option <tt>-val-ignore-recursive-calls</tt> now uses the assigns clauses of the recursive function to treat the call.</li> -<li class="user"> Emit proper alarms for completely imprecise floating-point values, and for casts from float to int.</li> -<li class="user-break"> Removed option <tt>-val-signed-overflow-alarms</tt>. Use <tt>-warn-signed-overflow</tt> instead.</li> -<li class="user-break"> Signed overflows now cause an alarm. Option <tt>-no-warn-signed-overflow</tt> can be used to get 2's complement.</li> -<li class="user-break"> Consolidated states are now stored before 'assert' clauses are evaluatued.</li> -<li class="user"> Optionally warn against unsigned overflows according to option <tt>-warn-unsigned-overflow</tt>.</li> -<li class="user-break"> The first element of a <tt>-lib-entry</tt> allocated array, or of an array passed as an argument to main, is now valid regardless of option <tt>-valid-context-pointers</tt>.</li> -<li class="user"> Better precision for postconditions in functions with multiple return analyzed without slevel.</li> -<li class="user"> The location in which the result of a call is stored is now evaluated before the call. A warning is emitted if this location has changed after the call.</li> -<li class="user"> Highlight non-terminating calls.</li> -</ul> -<h4>Bug Fixes</h4> -<ul class="entries"> -<li class="bugfix"> Fix <tt>"Semantic level unrolling superposing up to"</tt> messages. The number displayed was sometimes lower than the actual number of superposed states.</li> -<li class="bugfix"> A bug causing the number of superposed states to be slightly underestimated has been fixed. As a result, it may be necessary to up the <tt>-slevel</tt> argument a little bit for existing proof scripts.</li> -<li class="bugfix"> Correct potentially incorrect reduction on l-values of the form *(p+off) or *(p-off).</li> -<li class="bugfix"> Fix soundness bugs for comparisons with logic constants that are not representable as 64 bits double.</li> -<li class="bugfix"> Fix evaluation of logic constant characters above 127.</li> -<li class="bugfix"> Option <tt>-absolute-valid-range</tt> can now be changed between two executions of Value.</li> -<li class="bug-break"> Various changes in the way undefined functions returning pointers are handled.</li> -<li class="bugfix"> Ignore 'const' qualifier on extern globals in lib-entry mode. Previously, those globals were initialized to 0.</li> -<li class="bugfix"> Fix erroneous casting operating when interpreting logic casts.</li> -<li class="bugfix"> Fix validities of degenerate variables, which were too big considering the size of the memory.</li> -<li class="bugfix"> Improved again support for abstract structs.</li> -<li class="bugfix"> In <tt>-lib-entry</tt> mode, void* fields or pointers now point to something potentially valid.</li> -<li class="bugfix"> Initial state of Value does not depend on <tt>-main</tt> option, but depends on <tt>-context-</tt><...>.</li> -<li class="bugfix"> Fix incorrect reduction in integers containing pointers address when option <tt>-warn-signed-overflow</tt> is set.</li> -<li class="bugfix"> Option <tt>-memexec</tt> is now correct in presence of RTE alarms.</li> -<li class="bugfix"> Fixed misleading <tt>"after statement"</tt> state on statements followed by an assertion.</li> -<li class="bugfix"> Fix incorrectness of option <tt>-remove-redundant-alarms</tt> in presence of '<tt>\initialized</tt>(...)' alarms.</li> -<li class="bugfix"> Fix incorrect interpretation of <tt>\valid</tt>{{ "{" }}L}(P) when L is not Here label.</li> -</ul> -<h4>Developers Only</h4> -<ul class="entries"> -<li class="dev-break"> Remove various instances of Top_Param, which were all equal to <tt>Base.SetLattice</tt>.</li> -<li class="dev-break"> Builtins must now warn if their results should not be cached (signature change in <tt>Db.Value.builtin_result</tt>).</li> -<li class="dev-break"> Removed <tt>Base.All</tt> validity. Use big validities with unknown flag instead. Improved signature of <tt>Base.Unknown</tt>.</li> -<li class="dev-break"> Renamed <tt>Locations.valid_enumerate_bits</tt> into <tt>Locations.enumerate_valid_bits</tt>.</li> -<li class="dev-break"> Generic types of Value are now in Value_types (previously Value_aux). Implies a signature change for <tt>Db.Value.register_builtin</tt>. <tt>Value_aux.accept_base</tt> is now in <tt>Db.Semantic_Callgraph</tt>.</li> -</ul> -</div> -<hr><div><a id="Oxygen-8.0" href="#Oxygen-8.0"></a></div><h3 class="release">Oxygen Release <span class="hversion">[8.0]</span></h3> - -<div class="release"> -<h2>Frama-C General</h2> -<h4>New Features</h4> -<ul class="entries"> -<li class="user"><span class="kernel">[Cil]</span>  In debug mode, pretty-print numerical constants instead of displaying the source file strings.</li> -<li class="user-break"><span class="kernel">[Cil]</span>  Functions returning a value cannot let control flow falling through the closing '}' Fixes <a class="public" href="http://bts.frama-c.com/view.php?id=685">#685</a>.</li> -<li class="user"><span class="kernel">[Cil]</span>  New option <tt>-warn-undeclared-callee</tt> for calls to functions that have not been previously declared.</li> -<li class="user"><span class="kernel">[Journal]</span>  Better journalisation of command line options setting a list of arguments (<tt>e.g</tt>. <tt>-slevel-function</tt>): avoid quadratic complexity in the generated code (fixed bts <a class="private" href="http://bts.frama-c.com/view.php?id=1123">#1123</a>).</li> -<li class="user-break"><span class="kernel">[Kernel]</span>  Adding supports for clause allocates and frees and their version for loops.</li> -<li class="user-break"><span class="kernel">[Kernel]</span>  Sets generated assigns clauses into the default behavior.</li> -<li class="user-break"><span class="kernel">[Kernel]</span>  Adding some more supports for built-in related to memory blocks.</li> -<li class="user"><span class="kernel">[Kernel]</span>  Support for model fields</li> -<li class="user"><span class="kernel">[Kernel]</span>  Keep all prototypes with a spec, even if not referenced.</li> -<li class="user"><span class="kernel">[Kernel]</span>  New option -<plugin><tt>-share</tt> for plug-ins to customize their specific share directories.</li> -<li class="user"><span class="kernel">[Kernel]</span>  Use Zarith whenever possible (bts <a class="private" href="http://bts.frama-c.com/view.php?id=983">#983</a>).</li> -<li class="user"><span class="kernel">[Kernel]</span>  when printing help, display the name of the opposite boolean option (bts <a class="public" href="http://bts.frama-c.com/view.php?id=1085">#1085</a>).</li> -<li class="user"><span class="kernel">[Kernel]</span>  Consolidation from call-site preconditions to original precondition now handle calls through function pointers</li> -<li class="user-break"><span class="kernel">[Kernel]</span>  improve 'reachable' properties.</li> -<li class="user"><span class="kernel">[Kernel]</span>  New option <tt>-keep-unused-specified-functions</tt>.</li> -<li class="user-break"><span class="kernel">[Kernel]</span>  A negative value given to <tt>-ulevel</tt> option hides all UNROLL_LOOP pragmas.</li> -<li class="user"><span class="kernel">[Kernel]</span>  linker checks that the ghost status of two merged declaration is the same, and raises an error otherwise.</li> -<li class="user"><span class="kernel">[Kernel]</span>  C constant expressions are now allowed as UNROLL level into loop pragmas.</li> -<li class="user"><span class="kernel">[Kernel]</span>  The annotation 'loop pragma UNROLL <tt>"completly"</tt>, n;' unroll 'n' times the annoted loop and then add it a clause 'loop invariant <tt>\false</tt>;'. The remaining loop should be death code.</li> -<li class="user"><span class="kernel">[Kernel]</span>  All globals with attribute FC_BUILTIN are preserved even if unused.</li> -<li class="user-break"><span class="kernel">[Kernel]</span>  Remove useless negative options <tt>-no-help</tt>, <tt>-no-version</tt>, <tt>-no-print-share-path</tt>, <tt>-no-print-lib-path</tt> and <tt>-no-print-plugin-path</tt>.</li> -<li class="user"><span class="kernel">[Logic]</span>  Better label inference in axiomatics (see bts <a class="public" href="http://bts.frama-c.com/view.php?id=1068">#1068</a>).</li> -<li class="user"><span class="kernel">[Logic]</span>  LoopEntry and LoopCurrent built-in labels.</li> -<li class="user"><span class="kernel">[Logic]</span>  Cleaner generated assertions in presence of multiple pointer casts.</li> -<li class="user"><span class="kernel">[Logic]</span>  Better error messages when parsing logic.</li> -<li class="user"><span class="kernel">[Project]</span>  Accept to load inconsistent project by setting to default the inconsistent states and their dependencies.</li> -</ul> -<h4>Bug Fixes</h4> -<ul class="entries"> -<li class="bugfix"><span class="kernel">[Cil]</span>  Fail when encountering a lvalue of type void (<a class="public" href="http://bts.frama-c.com/view.php?id=1013">#1013</a>).</li> -<li class="bugfix"><span class="kernel">[Cil]</span>  Go to new line more often when printing sequence of statements. Fixes issues <a class="public" href="http://bts.frama-c.com/view.php?id=1021">#1021</a>.</li> -<li class="bugfix"><span class="kernel">[Cil]</span>  Correct sharing bug on widening pragmas. Fixes <a class="private" href="http://bts.frama-c.com/view.php?id=1090">#1090</a>.</li> -<li class="bugfix"><span class="kernel">[Cil]</span>  Improve label positions in presence of loop unrolling (bug <a class="public" href="http://bts.frama-c.com/view.php?id=1100">#1100</a>).</li> -<li class="bugfix"><span class="kernel">[Cil]</span>  Preserve typedefs on global variables with an initializer</li> -<li class="bugfix"><span class="kernel">[Cil]</span>  Better propagatation of volatile, const and restrict type qualifiers through typedefs on arrays</li> -<li class="bugfix"><span class="kernel">[Journal]</span>  Fixed bug <a class="private" href="http://bts.frama-c.com/view.php?id=1080">#1080</a>: better generated journal in case of missing internal data preventing it of being runable.</li> -<li class="bugfix"><span class="kernel">[Journal]</span>  Fixed bts <a class="public" href="http://bts.frama-c.com/view.php?id=932">#932</a> about journalization of dynamic plug-ins in some corner cases.</li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Better linking behavior (fixes <a class="public" href="http://bts.frama-c.com/view.php?id=672">#672</a>).</li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Link error aborts Frama-C (fixes <a class="public" href="http://bts.frama-c.com/view.php?id=990">#990</a>).</li> -<li class="bug-break"><span class="kernel">[Kernel]</span>  empty list in <tt>complete/disjoint</tt> is expanded by logic type-checker to the list of behavior name of current contract. Fixes issue <a class="public" href="http://bts.frama-c.com/view.php?id=1006">#1006</a>. See bts comments for the differences that can appear in the treatment of specs.</li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  keep track of local variables even in presence of annotation + do not silently lose statement contract. Fixes issue <a class="public" href="http://bts.frama-c.com/view.php?id=1009">#1009</a>.</li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Fixed bug about property statuses and setting parameters after <tt>-load</tt> (statuses were not cleared when required).</li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Initialization of locals is correct for all sizes; uses bzero to 0 + contract (directly validated by Kernel)</li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Fixed bug <a class="public" href="http://bts.frama-c.com/view.php?id=1135">#1135</a> and bug <a class="public" href="http://bts.frama-c.com/view.php?id=1139">#1139</a> about loop unrolling.</li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Fixes issue in loop unrolling and annotations.</li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Strict checking of type compatibility when merging an already called prototype without arg list and a full prototype (fixes issue <a class="public" href="http://bts.frama-c.com/view.php?id=728">#728</a>, <a class="private" href="http://bts.frama-c.com/view.php?id=109">#109</a>).</li> -<li class="bug-break"><span class="kernel">[Kernel]</span>  Introduce more temporaries for a call [lv = f()] if the return type of f and the type of lv do not match. Fix issue <a class="public" href="http://bts.frama-c.com/view.php?id=1024">#1024</a>.</li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Fixed bug with <tt>Type.pp_ml_name</tt> for generic sets which can lead to incorrect journal generation (bts <a class="public" href="http://bts.frama-c.com/view.php?id=1127">#1127</a>).</li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Fix graph of consolidation statuses when several properties get the same name.</li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Fixes bug <a class="public" href="http://bts.frama-c.com/view.php?id=840">#840</a> (inaccurate position in presence of <tt>-pp-annot</tt>).</li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Fixed bug with <tt>save/load</tt>: loading a file <f>, then quitting Frama-C can no longer modify <f> (bts <a class="private" href="http://bts.frama-c.com/view.php?id=1269">#1269</a>).</li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Fixed <a class="private" href="http://bts.frama-c.com/view.php?id=1267">#1267</a> (adds explicit casts for default argument promotions).</li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Do not accept spurious '}'. Fixes bts <a class="public" href="http://bts.frama-c.com/view.php?id=1273">#1273</a>.</li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Fixed missing undefined behavior for multiple write accesses (fixes bts <a class="public" href="http://bts.frama-c.com/view.php?id=1059">#1059</a>).</li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Fine tuning AST dependencies. See developer guide.</li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Identical messages emitted in two different projects will now be visible in both projects. Fix bug <a class="public" href="http://bts.frama-c.com/view.php?id=1104">#1104</a>.</li> -<li class="bugfix"><span class="kernel">[Logic]</span>  Fixes issue <a class="public" href="http://bts.frama-c.com/view.php?id=1005">#1005</a> (earlier detection of duplicated axiom name avoids <tt>Kernel.fatal</tt>).</li> -<li class="bugfix"><span class="kernel">[Logic]</span>  Fixes sizeof(<tt>"string_literal"</tt>) in logic.</li> -<li class="bugfix"><span class="kernel">[Logic]</span>  Fixed bts <a class="private" href="http://bts.frama-c.com/view.php?id=1253">#1253</a>: IndexPI and PlusPI are equivalent.</li> -</ul> -<h4>Developers Only</h4> -<ul class="entries"> -<li class="dev-break"><span class="kernel">[Cil]</span>  Add method pFile in printers. Signature change for <tt>Cil.d_file</tt> (but you should use <tt>!Ast_printer.d_file</tt>).</li> -<li class="dev"><span class="kernel">[Cil]</span>  Fixed off-by-one error in foldLeftCompound <tt>~implicit</tt>:true.</li> -<li class="dev-break"><span class="kernel">[Cil]</span>  Ast changed: Unrool_level renamed into Unroll_specs and its argument becomes a list for next evolutions.</li> -<li class="dev"><span class="kernel">[Cil]</span>  Fixed bts <a class="public" href="http://bts.frama-c.com/view.php?id=1254">#1254</a>: incorrect documentation of <tt>Cil.d_plaininit</tt>.</li> -<li class="dev-break"><span class="kernel">[Cil]</span>  Remove type <tt>Cil_type.typeSig</tt>. Use the functions in <tt>Cil_datatype.Typ</tt> and <tt>Cil_datatype.Logic_typ</tt> to compare types.</li> -<li class="dev-break"><span class="kernel">[Cil]</span>  Split constants of logic and C (fixes bts <a class="public" href="http://bts.frama-c.com/view.php?id=745">#745</a>).</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  <tt>Logic_preprocess.file</tt> takes an additional parameter, as gcc pre-processor treats differently .c and .cxx files, and this must be reflected in annotation pre-processing.</li> -<li class="dev"><span class="kernel">[Kernel]</span>  <tt>Plugin.Register</tt> defines a new option <tt>-plugin-debug-category</tt> that allows to enable debugging for sub-categories of messages (See <tt>Log.set_debug_keys</tt> for more info).</li> -<li class="dev"><span class="kernel">[Kernel]</span>  New <tt>File.init_from_project</tt> function.</li> -<li class="dev"><span class="kernel">[Kernel]</span>  Added <tt>Property.location</tt> function.</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  <tt>Kernel.CppExtraArgs</tt> now gets type <tt>Plugin.String_list</tt> and not <tt>Plugin.String_set</tt> (fixed bts <a class="private" href="http://bts.frama-c.com/view.php?id=1132">#1132</a>).</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  <tt>Plugin.set_optional_help</tt> is now deprecated.</li> -<li class="dev"><span class="kernel">[Kernel]</span>  Fix implementation of <tt>Datatype.Triple</tt> and <tt>Datatype.Quadruple</tt> (bts <a class="private" href="http://bts.frama-c.com/view.php?id=1133">#1133</a>).</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  <tt>Kernel.Functions.get</tt> does not silently create a kernel function if it does not already exist. This behavior is kept for Cil builtins.</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  New API for Annotations which merges old Annotations, <tt>Globals.Annotations</tt> and operations of Kernel_function over function contracts.</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  Remove module Inthash. Use <tt>Datatype.Int.Hashtbl</tt> instead, or directly <tt>carbon2nitrogen.sh</tt> migration script.</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  Correct (albeit slow) hash function for terms and term lvalues.</li> -<li class="dev"><span class="kernel">[Kernel]</span>  Hook for handling for loop components in Cabs.</li> -<li class="dev"><span class="kernel">[Kernel]</span>  <tt>-check</tt> verifies if vdefined flag is coherent with status of variable in Globals tables and AST. Fixes one of the issues of <a class="private" href="http://bts.frama-c.com/view.php?id=1241">#1241</a>.</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  Add function [stmt_can_reach] to the arguments of <tt>Dataflow.Backwards</tt>, which is used to speed up the analysis. See <tt>dataflow.mli</tt> for good possible values.</li> -<li class="dev"><span class="kernel">[Kernel]</span>  Changes in interface of StringHashtbl options.</li> -<li class="dev"><span class="kernel">[Kernel]</span>  API of dynamic plug-ins is now documented as well as static plug-ins (fixed bts <a class="private" href="http://bts.frama-c.com/view.php?id=171">#171</a>).</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  Operations that silently mutate AST should now call <tt>Ast.mark_as_changed</tt> to clear states depending on it (fixes <a class="private" href="http://bts.frama-c.com/view.php?id=1244">#1244</a>).</li> -<li class="dev"><span class="kernel">[Kernel]</span>  Fixed bts <a class="private" href="http://bts.frama-c.com/view.php?id=1250">#1250</a>: setting formals of visited function is not delayed until fill_global_tables anymore.</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  Remove obsolete constructors <tt>Cabs.TRANSFORMER</tt> and <tt>Cabs.EXPRTRANSFORMER</tt> and related parsing rules.</li> -<li class="dev"><span class="kernel">[Kernel]</span>  Datatype with structural comparison for exp and lval fixes bts <a class="public" href="http://bts.frama-c.com/view.php?id=1263">#1263</a>.</li> -<li class="dev"><span class="kernel">[Kernel]</span>  Correct hash function for Sets created by <tt>Datatype.Make_with_collections</tt> or <tt>Datatype.With_collections</tt>.</li> -<li class="dev"><span class="kernel">[Kernel]</span>  Improve signature of <tt>State_builder.Set_ref</tt>.</li> -<li class="dev"><span class="kernel">[Makefile]</span>  Fixed bug <a class="public" href="http://bts.frama-c.com/view.php?id=1082">#1082</a> about wrong link in generated code documentation.</li> -<li class="dev"><span class="kernel">[Makefile]</span>  'make doc' did not work when GUI disabled (bts <a class="public" href="http://bts.frama-c.com/view.php?id=1014">#1014</a>).</li> -<li class="dev"><span class="kernel">[Makefile]</span>  Fix bug <a class="public" href="http://bts.frama-c.com/view.php?id=1145">#1145</a> about PLUGIN_LINK_GUI_OFLAGS.</li> -<li class="dev"><span class="kernel">[Makefile]</span>  Use <tt>ocamldoc.opt</tt> whenever possible.</li> -<li class="dev"><span class="kernel">[Makefile]</span>  plugin is distributed iff PLUGIN_DISTRIBUTED and PLUGIN_ENABLE are not 'no' (instead of PLUGIN_DISTRIBUTED == yes).</li> -<li class="dev"><span class="kernel">[Makefile]</span>  Added variables PTESTS_OPTS and PLUGIN_PTESTS_OPTS to pass options to ptests through make tests. See dev manual.</li> -</ul> -<h2>Frama-C GUI</h2> -<ul class="entries"> -<li class="user"><span class="kernel">[Gui]</span>  Display global annotations in the filetree.</li> -<li class="user"><span class="kernel">[Gui]</span>  Add filters for properties' consolidated statuses.</li> -<li class="user"><span class="kernel">[Gui]</span>  Removing 'add assert before' from contextual menu. Uses ACSL_Importer plugin for such a feature.</li> -<li class="user"><span class="kernel">[Gui]</span>  Display all properties in 'Properties' panel, including generated ones without location.</li> -<li class="user"><span class="kernel">[Gui]</span>  Fixed bugs when the consolidation graph cannot be displayed (fixed bts <a class="public" href="http://bts.frama-c.com/view.php?id=1122">#1122</a>).</li> -</ul> -<h2>Plugin Aorai</h2> -<ul class="entries"> -<li class="user"> Aorai gets a real Dataflow analysis for contract generation + various logic simplifications.</li> -</ul> -<h2>Plugin From</h2> -<ul class="entries"> -<li class="user"> Better precision for code of the form 'if (c) stop(); else y = x+1;', where stop does not terminate</li> -<li class="user"> More sharing between identical values when printing results.</li> -<li class="user"> Major precision improvements when evaluating library functions whose assigns contains ranges.</li> -<li class="bugfix"> The interpretation of explicit assigns clauses for library function <tt>"assigns *p \from x;"</tt> was wrong: every possible location was assumed to have been overwritten.</li> -</ul> -<h2>Plugin Impact</h2> -<ul class="entries"> -<li class="user"> Complete rewrite. Improved precision and computation time. Fixes wishes <a class="private" href="http://bts.frama-c.com/view.php?id=5">#5</a> and <a class="private" href="http://bts.frama-c.com/view.php?id=6">#6</a>.</li> -</ul> -<h2>Plugin Inout</h2> -<ul class="entries"> -<li class="user"> Major precision improvements when evaluating library functions whose assigns contains ranges.</li> -<li class="user"> Option <tt>-inout-callwise</tt> to compute callsite-wise operational inputs. Improves precision of <tt>-inout</tt>, of the <tt>"Modifies"</tt> clause in the gui, and of the slicing.</li> -<li class="user"> Operational inputs are now more precise for function with only an ACSL prototype.</li> -<li class="user"> Better precision for 'if' in which only a side is reachable.</li> -<li class="user-break"> Option <tt>-inout-callwise</tt> restarts Value when it is newly set</li> -</ul> -<h2>Plugin Metrics</h2> -<ul class="entries"> -<li class="bugfix"> Fixes count of pointer accesses.</li> -</ul> -<h2>Plugin Occurrence</h2> -<ul class="entries"> -<li class="user"> Results can be filtered to display only occurrences in read or write positions.</li> -<li class="bugfix"> Fix bug where some occurrences were silently ignored in big asts; improve performance.</li> -</ul> -<h2>Plugin Pdg</h2> -<ul class="entries"> -<li class="user"> Improve precision in presence of provably dead code branches. Fixes issue <a class="public" href="http://bts.frama-c.com/view.php?id=1194">#1194</a>.</li> -<li class="user-break"> Rename option <tt>-dot-pdg</tt> into <tt>-pdg-dot</tt></li> -<li class="user"> Improve performance, typically on arrays of structs.</li> -<li class="bugfix"> Option <tt>-pdg</tt> did nothing if <tt>-pdg-print</tt> was not set.</li> -</ul> -<h2>Plugin Report</h2> -<ul class="entries"> -<li class="user"> Display unreachable properties in a special way; identify unreachable statement more clearly.</li> -</ul> -<h2>Plugin Rte</h2> -<h4>New Features</h4> -<ul class="entries"> -<li class="user"> Emit <tt>\valid_read</tt> alarms instead of <tt>\valid</tt> for read accesses.</li> -<li class="user"> Reuse behaviors names when <tt>-rte-precond</tt> is used on fonctions with multiple behaviors.</li> -<li class="user"> Generate simpler assertions for accesses to arrays, and discard trivial ones; improve ordering of assertions. Honor option <tt>-unsafe-arrays</tt>.</li> -<li class="user-break"> Rename option <tt>-rte-const</tt> into <tt>-rte-no-trivial-annotations</tt> (set by default).</li> -</ul> -<h4>Bug Fix</h4> -<ul class="entries"> -<li class="bugfix"> Prevent generation of incorrect alarms on statements whose order of execution is not completely specified.</li> -</ul> -<h2>Plugin Scope</h2> -<ul class="entries"> -<li class="user"> Improved computation of defs. Statements are categorized between direct and indirect accesses.</li> -<li class="user"> Improve precision of Defs computation (wish <a class="public" href="http://bts.frama-c.com/view.php?id=1079">#1079</a>).</li> -</ul> -<h2>Plugin Slicing</h2> -<ul class="entries"> -<li class="user"> No more blank between <tt>-slicing-project-name</tt> and <tt>-slicing-exported-project-postfix</tt> (from <a class="private" href="http://bts.frama-c.com/view.php?id=1249">#1249</a> entry).</li> -<li class="user"> More precise slicing when <tt>-calldeps</tt> is used (fixes wish <a class="public" href="http://bts.frama-c.com/view.php?id=107">#107</a>).</li> -</ul> -<h2>Plugin Syntactic_callgraph</h2> -<ul class="entries"> -<li class="bugfix"> Fix bug <a class="public" href="http://bts.frama-c.com/view.php?id=989">#989</a> about difference of display between GUI and dot output.</li> -<li class="bugfix"> Fix tricky bug while computing services when a cycle depends on another cycle (most part of the fix is actually in OcamlGraph itself).</li> -</ul> -<h2>Plugin Value</h2> -<h4>New Features</h4> -<ul class="entries"> -<li class="user"> Improve evaluation of logic when option <tt>-val-signed-overflow-alarms</tt> is active.</li> -<li class="user"> Improve interpretation of ACSL annotations in presence of typedefs.</li> -<li class="user"> Evaluate more precisely statements of the form if (*p ==<br/><i>1</i>.  {{ "{" }}...} when *p is reused within the if block. This also improves the handling of switches.</li> -<li class="user"> New option <tt>-no-val-left-shift-negative-alarms</tt> to treat left shift of negative integers as defined.</li> -<li class="user"> Better evaluation of <tt>\initialized</tt> predicate when only some parts of the location are initialized.</li> -<li class="user"> New builtin Frama_C_assert. Take advantage of existing assertions with <tt>"#define assert Frama_C_assert"</tt>.</li> -<li class="user"> Suppressed confusing message "all target addresses were invalid. This path is assumed to be dead.".</li> -<li class="user"> After emitted an alarm <tt>\initialized</tt>(lv), the value analysis tries to remember that lv is initialized. This suppresses redundant alarms that were emitted further on.</li> -<li class="user"> Minor improvements related to single-precision floating-point handling.</li> -<li class="user"> In index out-of-bounds alarms, do not generate 'assert 0 <= i' part when 'i' is always greater than 0.</li> -<li class="user"> During evaluation, reduce indexes that are detected as out-of_bounds.</li> -<li class="user"> Reduce more aggressively invalid pointers: {{ "{" }} p->f1 = v1; p->f2 = v2 } will usually raise at most one alarm.</li> -<li class="user"> FRAMA_C_MALLOC_INDIVIDUAL modelization now properly treats allocated blocks as uninitialized.</li> -<li class="user"> Aesthetic fix: do not display {{ "{" }}{{ "{" }} &NULL }} and {{ "{" }}{{ "{" }} &<tt>"foo"</tt> + {{ "{" }}2} }} but rather {{ "{" }}{{ "{" }} NULL }} and {{ "{" }}{{ "{" }} <tt>"foo"</tt> + {{ "{" }}2} }}.</li> -<li class="user"> Improve precision for code with pointer casts (fixes bug <a class="public" href="http://bts.frama-c.com/view.php?id=1074">#1074</a>).</li> -<li class="user"> Assertions of the form <tt>\valid</tt>(p+i) and <tt>\valid</tt>(&p->f) are now used to reduce p whenever possible.</li> -<li class="user"> Evaluation of <tt>\separated</tt> predicate</li> -<li class="user"> New message for functions with only a specification. Changed old message for functions with neither code nor specification to <tt>"No code nor specification for function ..."</tt>.</li> -<li class="user"> Improved handling of *(p+i) (or equivalently p[i]) when p is a known pointer and i is unknown.</li> -<li class="user"> Improved handling of conditions involving the conversion to int of a floating-point variable.</li> -<li class="user"> Support for <tt>\valid_read</tt> predicate; evaluation of <tt>\at</tt>(p,Pre) and <tt>\initialized</tt>{{ "{" }}Pre}(...).</li> -<li class="user"> Errors during evaluation in the logic are now reported.</li> -<li class="user"> Old <tt>"Evaluate expression"</tt> menu in the GUI replaced by <tt>"Evaluate ACSL term"</tt>; value of term lval is now displayed. Evaluations that may fail are flagged.</li> -<li class="user"> Allow comparison of invalid pointers in the logic.</li> -<li class="user"> New option <tt>-val-ilevel</tt>, to change the frontier between sets of integers and intervals.</li> -<li class="user"> Add bzero builtin. A precise destination and size are required (wish <a class="public" href="http://bts.frama-c.com/view.php?id=915">#915</a>).</li> -<li class="user"> Position call-site statuses for function preconditions, instead of the previous global status.</li> -<li class="user-break"> More thorough checks for calls through a function pointer: warn when the function type and the pointer are not compatible, and stop when they cannot be reconciled.</li> -<li class="user"> Statutes 'Invalid' are now positioned on 'for behav:' assertions even when 'behav' is not the only active behavior.</li> -<li class="user"> Assertions such as <tt>\valid</tt>(p) now evaluate to Invalid when p is not initialized or an escaping address.</li> -<li class="user"> Warn when 'assigns *p' points to a completely invalid location.</li> -<li class="user"> Clarified message about completely indeterminate memory.</li> -<li class="user"> Print misaligned values in a simpler way. Fixes wish <a class="private" href="http://bts.frama-c.com/view.php?id=1271">#1271</a>.</li> -</ul> -<h4>Bug Fixes</h4> -<ul class="entries"> -<li class="bugfix"> Fixed spurious alarm <tt>\valid</tt>(p) in *p = e; when e is completely invalid. Soundness was not affected (the alarm for whatever made e invalid was present).<br/><br/></li> -<li class="bugfix"> Fixed crash when a library function is called in a state where the function's precondition cannot be true.</li> -<li class="bugfix"> Improve warnings and evaluation in presence of possibly infinite floats (fixes <a class="public" href="http://bts.frama-c.com/view.php?id=997">#997</a>).</li> -<li class="bugfix"> Generate correct assertions when using memcpy builtin. Fix <a class="public" href="http://bts.frama-c.com/view.php?id=1000">#1000</a>.</li> -<li class="bugfix"> Fixed <a class="public" href="http://bts.frama-c.com/view.php?id=1001">#1001</a>: do not warn for unsigned shifts, do not end propagation on signed left shift of an address.</li> -<li class="bugfix"> Prevent potentially incorrect assertions from being emitted when the result a call must be cast. Fixes <a class="public" href="http://bts.frama-c.com/view.php?id=997">#997</a> and <a class="public" href="http://bts.frama-c.com/view.php?id=1024">#1024</a>.</li> -<li class="bugfix"> Fixed soundness bugs involving lval = lval; assignments targeting literal strings and automatically created S_... memory zones.</li> -<li class="bugfix"> Fix wrong hash function, which could cause memory overuse and worse.</li> -<li class="bugfix"> Evaluate ACSL && and || when they appear as terms (fixes bug <a class="public" href="http://bts.frama-c.com/view.php?id=1072">#1072</a>).</li> -<li class="bugfix"> Allocate a finite space for malloc builtins; fixes some bugs when a pointer refers to a non-yet allocated space.</li> -<li class="bugfix"> Fix crashes <tt>and/or</tt> missing alarms when evaluating *p=(cast)f() with p invalid (bug <a class="private" href="http://bts.frama-c.com/view.php?id=1097">#1097</a>).</li> -<li class="bugfix"> Fix bug in evaluation of pointers to start of array.</li> -<li class="bugfix"> Fixed bug where user assertions accessing uninitialized variables got the wrong status.</li> -<li class="bugfix"> Handle 'assigns *p' where p has a typedef type</li> -<li class="bugfix"> Fix incorrect initialization of volatile fields or globals in presence of initializers (bts <a class="private" href="http://bts.frama-c.com/view.php?id=1112">#1112</a>).</li> -<li class="bugfix"> Fix possible typing bugs when evaluating logic expressions with non-integral types (bts <a class="private" href="http://bts.frama-c.com/view.php?id=1175">#1175</a>).</li> -<li class="bugfix"> Re-emit alarms when Value options are changed and an analysis is restarted.</li> -<li class="bugfix"> Better time and space complexity for initialization of big arrays in <tt>-lib-entry</tt> mode (bts <a class="public" href="http://bts.frama-c.com/view.php?id=1026">#1026</a>).</li> -<li class="bugfix"> In lib-entry mode, honor 'const' attributes that appear deep inside the type (bts <a class="public" href="http://bts.frama-c.com/view.php?id=759">#759</a>).</li> -<li class="bugfix"> Calls (*p)() where p resolves to both valid functions and invalid addresses are now properly handled.</li> -<li class="bugfix"> Fix crash when an undeclared function returned a pointer to a function that was later called.</li> -<li class="bugfix"> Fix crash when evaluating *((int*)0+x)=v when the NULL base is invalid.</li> -</ul> -<h4>Developers Only</h4> -<ul class="entries"> -<li class="dev"> shift_left and shift_right functions now take an optional signedness boolean in addition to the optional size.</li> -<li class="dev-break"> Moved contents of <tt>memory_state/Abstract_value</tt> into <tt>ai/Lattice_Interval_Set</tt>. Use <tt>bin/nitrogen2oxygen</tt> for automatic migration.</li> -<li class="dev"> <tt>Lmap.paste_offsetmap</tt> now handles imprecise destinations.</li> -<li class="dev"> Fix option <tt>-absolute-valid-range</tt> being reset by project copies.</li> -<li class="dev-break"> Made type <tt>Ival.tt</tt> private.</li> -<li class="dev-break"> Rename <tt>Db.Value.assigns_to_zone_inputs_state</tt> to <tt>Db.Value.assigns_inputs_to_zone</tt>. Add new functions <tt>Db.Value.assigns_outputs_to_zone</tt> and <tt>Db.Value.assigns_inputs_to_locations</tt>.</li> -<li class="dev-break"> Signature change for function <tt>Db.Value.register_builtin</tt>: builtins can now return multiple states.</li> -</ul> -</div> -<hr><div><a id="Nitrogen-7.0" href="#Nitrogen-7.0"></a></div><h3 class="release">Nitrogen Release <span class="hversion">[7.0]</span></h3> - -<div class="release"> -<h2>Frama-C General</h2> -<h4>New Features</h4> -<ul class="entries"> -<li class="user-break"><span class="kernel">[Cil]</span>  Enumerated constants are kept in the AST.</li> -<li class="user"><span class="kernel">[Cil]</span>  Implement precise dataflow on switch constructs. As side effect, improve precision of value analysis.</li> -<li class="user-break"><span class="kernel">[Cil]</span>  Fixed <a class="public" href="http://bts.frama-c.com/view.php?id=720">#720</a> (incorrect simplification of switch).</li> -<li class="user"><span class="kernel">[Cil]</span>  Support for &<tt>"constant_string"</tt> in parser.</li> -<li class="user"><span class="kernel">[Cil]</span>  Normalization of lval: T+1 ==> &T[1] when T is in fact an array (implies *(T+1) ==> T[1])</li> -<li class="user"><span class="kernel">[Cil]</span>  Pretty-printing lval and term_lval the same way</li> -<li class="user"><span class="kernel">[Cil]</span>  Cache results of offsets computations.</li> -<li class="user"><span class="kernel">[Cil]</span>  Add support for GCC specific cast from field of union to union</li> -<li class="user"><span class="kernel">[Kernel]</span>  Exit status on unknown error is now 125. 127 and 126 are reserved for the shell by POSIX.</li> -<li class="user"><span class="kernel">[Kernel]</span>  Better error message when plug-in crashes on loading (bts <a class="public" href="http://bts.frama-c.com/view.php?id=737">#737</a>).</li> -<li class="user"><span class="kernel">[Kernel]</span>  Big integers can now be displayed using hexadecimal notation.</li> -<li class="user"><span class="kernel">[Kernel]</span>  <tt>\at</tt>(p,Old) is pretty-printed as <tt>\old</tt>(p).</li> -<li class="user"><span class="kernel">[Kernel]</span>  Some messages may be printed several time for the same line if they refer to different columns.</li> -<li class="user-break"><span class="kernel">[Kernel]</span>  Better handling of comments with <tt>-keep-comments</tt> and new API. See <tt>Cabshelper.Comments</tt> and <tt>Globals.get_comments_</tt>*</li> -<li class="user"><span class="kernel">[Kernel]</span>  Better pretty printing of lists of any elements</li> -<li class="user"><span class="kernel">[Kernel]</span>  Current pragmas no longer give rise to code annotations (as they do not contain anything that can be proven).</li> -<li class="user"><span class="kernel">[Kernel]</span>  Improve space complexity of function stmt_can_reach.</li> -<li class="user"><span class="kernel">[Kernel]</span>  New kind of command-line parameter, for commands that do heavy output. Used for Value, Pdg and Metrics.</li> -<li class="user"><span class="kernel">[Logic]</span>  Added support for bitwise operators <tt>--</tt>> and <<tt>--</tt>> into ACSL formula.</li> -</ul> -<h4>Bug Fixes</h4> -<ul class="entries"> -<li class="bugfix"><span class="kernel">[Cil]</span>  Fixed bug <a class="public" href="http://bts.frama-c.com/view.php?id=725">#725</a> (type-checking && operator).</li> -<li class="bugfix"><span class="kernel">[Cil]</span>  Fix bugs <a class="public" href="http://bts.frama-c.com/view.php?id=780">#780</a> and <a class="public" href="http://bts.frama-c.com/view.php?id=791">#791</a>: use ids unique between projects for varinfos, statements and expressions.</li> -<li class="bugfix"><span class="kernel">[Cil]</span>  Fix bug <a class="public" href="http://bts.frama-c.com/view.php?id=785">#785</a>: promotion between long long and an unsigned same-sized type.</li> -<li class="bugfix"><span class="kernel">[Cil]</span>  Fixes wrong precedence of not in predicate when pretty-printing.</li> -<li class="bugfix"><span class="kernel">[Cil]</span>  Fixes bug <a class="public" href="http://bts.frama-c.com/view.php?id=771">#771</a> (spurious warning for <tt>read/write</tt> accesses in undefined order).</li> -<li class="bugfix"><span class="kernel">[Cil]</span>  Fixes bug <a class="public" href="http://bts.frama-c.com/view.php?id=832">#832</a> (spurious warning for <tt>read/write</tt> accesses in undefined order)</li> -<li class="bugfix"><span class="kernel">[Cil]</span>  Fixes bug <a class="public" href="http://bts.frama-c.com/view.php?id=857">#857</a> (problem with some C enum value and Ocaml 32 bits <tt>3.11</tt>.0).</li> -<li class="bugfix"><span class="kernel">[Cil]</span>  Correct obscure Cil bug linked to the removal of trivial unspecified sequences or blocks. Fixes bug <a class="public" href="http://bts.frama-c.com/view.php?id=882">#882</a>.</li> -<li class="bugfix"><span class="kernel">[Cil]</span>  Fix conversion bug for f(i++) or f(++i) when i has size less than int, and f expects an int (bug <a class="public" href="http://bts.frama-c.com/view.php?id=911">#911</a>).</li> -<li class="bugfix"><span class="kernel">[Cil]</span>  Fix merging bug (<a class="private" href="http://bts.frama-c.com/view.php?id=948">#948</a>).</li> -<li class="bugfix"><span class="kernel">[Cil]</span>  Correctly handle casts in switch. Fixes <a class="public" href="http://bts.frama-c.com/view.php?id=961">#961</a>.</li> -<li class="bugfix"><span class="kernel">[Configure]</span>  Fix bug <a class="private" href="http://bts.frama-c.com/view.php?id=262">#262</a>: <tt>--disable-plugin</tt> works for external plugins compiled from within Frama-C kernel.</li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Bug fixed in pretty printer. (incorrect precedences leading to missing parenthesis).</li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Bug fixed in <tt>File.create_project_from_visitor</tt> potentially impacted programs transformation.</li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Fixed bug <a class="public" href="http://bts.frama-c.com/view.php?id=775">#775</a>. Large octal and hexadecimal constants are now correctly typed.</li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Fixed bug <a class="public" href="http://bts.frama-c.com/view.php?id=770">#770</a> and <a class="public" href="http://bts.frama-c.com/view.php?id=769">#769</a>, part 1. Fixed typo in anonFieldName (was annonFieldName).</li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Fix bug <a class="public" href="http://bts.frama-c.com/view.php?id=769">#769</a>: merging issue for declared struct.</li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Fix 'make clean' of plug-ins.</li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Support for GCC packed and aligned attributes and for GCC pack pragmas. Fixes <a class="public" href="http://bts.frama-c.com/view.php?id=719">#719</a>.</li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Fixed typing of bitfields whose size is equal to the size of int (bugs <a class="public" href="http://bts.frama-c.com/view.php?id=823">#823</a>, <a class="public" href="http://bts.frama-c.com/view.php?id=817">#817</a>).</li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Support GCC like typing of enums.</li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Fixed macros in <tt>limit.h</tt>.</li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Correct syntactic loop unrolling in presence of switch. Fixes bug <a class="public" href="http://bts.frama-c.com/view.php?id=861">#861</a>.</li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Add parameter <tt>~declarations</tt> to <tt>Globals.FileIndex.get_functions</tt>. Prevent duplication bug in properties navigator of the GUI.</li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Fixes visitor bug + properly refresh ids of properties in code transformation (in particular loop unrolling).</li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Fixes various performance issues when parsing very large functions. Fixes <a class="private" href="http://bts.frama-c.com/view.php?id=965">#965</a>.</li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  New exception for <tt>Ast.UntypedFiles.get</tt> when no untyped AST is available. Fixes <a class="public" href="http://bts.frama-c.com/view.php?id=954">#954</a>.</li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Treat long bitfields the same way as gcc and clang. Fixes <a class="private" href="http://bts.frama-c.com/view.php?id=959">#959</a>.</li> -<li class="bug-break"><span class="kernel">[Kernel]</span>  Do not normalize Pre in Old, especially where Old is not allowed.</li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Warn when the plug-in specified by <tt>-load-module</tt> or <tt>-load-script</tt> is not found (used to remain silent)</li> -<li class="bugfix"><span class="kernel">[Logic]</span>  Fixed bug <a class="public" href="http://bts.frama-c.com/view.php?id=714">#714</a> about lexing ACSL characters and strings.</li> -<li class="bugfix"><span class="kernel">[Logic]</span>  Fixed bug <a class="public" href="http://bts.frama-c.com/view.php?id=744">#744</a> (comparison between arithmetic types is done in the smallest possible type).</li> -<li class="bugfix"><span class="kernel">[Logic]</span>  <tt>\at</tt>(t,L) when t is a C array is now a logic array whose content is the one of t at L, not the address of the first element of t (which stays the same between L and Here anyway). partial fix of bug <a class="public" href="http://bts.frama-c.com/view.php?id=761">#761</a>.</li> -<li class="bugfix"><span class="kernel">[Logic]</span>  Fix bug <a class="private" href="http://bts.frama-c.com/view.php?id=501">#501</a>: volatile clauses are handled by the kernel.</li> -<li class="bugfix"><span class="kernel">[Logic]</span>  Fix bug <a class="public" href="http://bts.frama-c.com/view.php?id=761">#761</a>: adding <tt>\old</tt> in ensures clause for parameters does not capture terms in associated offset.</li> -<li class="bugfix"><span class="kernel">[Logic]</span>  Fixed issue with <tt>-pp-annot</tt> (fix bug <a class="public" href="http://bts.frama-c.com/view.php?id=691">#691</a> and <a class="public" href="http://bts.frama-c.com/view.php?id=812">#812</a>).</li> -<li class="bugfix"><span class="kernel">[Logic]</span>  Fixed overloading resolution (fixes bug <a class="public" href="http://bts.frama-c.com/view.php?id=655">#655</a>).</li> -<li class="bugfix"><span class="kernel">[Logic]</span>  can have a local binding for a predicate (even a constant one) without spurious warnings from typechecker. (fixes <a class="private" href="http://bts.frama-c.com/view.php?id=848">#848</a>)</li> -<li class="bugfix"><span class="kernel">[Logic]</span>  Normalization of assigns clause: <tt>\result</tt> and <tt>\exit_status</tt> only appear if a <tt>\from</tt> is specified. Fixes <a class="private" href="http://bts.frama-c.com/view.php?id=557">#557</a>, <a class="private" href="http://bts.frama-c.com/view.php?id=845">#845</a></li> -<li class="bugfix"><span class="kernel">[Logic]</span>  Fixed issue <a class="private" href="http://bts.frama-c.com/view.php?id=866">#866</a> (merging specs included twice)</li> -<li class="bugfix"><span class="kernel">[Logic]</span>  Fixes bug <a class="private" href="http://bts.frama-c.com/view.php?id=887">#887</a> (merging logic constants).</li> -<li class="bugfix"><span class="kernel">[Logic]</span>  Fixes bug <a class="public" href="http://bts.frama-c.com/view.php?id=885">#885</a> (wrong insertion of cast).</li> -<li class="bugfix"><span class="kernel">[Logic]</span>  Fix bug <a class="private" href="http://bts.frama-c.com/view.php?id=501">#501</a>: volatile clauses relative to partially volatile lvalues are handled by the kernel.</li> -<li class="bugfix"><span class="kernel">[Project]</span>  Fix sharing bug when copying project.</li> -</ul> -<h4>Developers Only</h4> -<ul class="entries"> -<li class="dev"><span class="kernel">[Cil]</span> /Logic New functions <tt>Clexer.is_c_keyword</tt> and <tt>Logic_lexer.is_acsl_keyword</tt>.</li> -<li class="dev-break"><span class="kernel">[Cil]</span>  AST changed: 'a before_after type is deleted. All annotations are now attached before.</li> -<li class="dev-break"><span class="kernel">[Cil]</span>  AST changed: removing Told and Pold constructs.</li> -<li class="dev-break"><span class="kernel">[Cil]</span>  Remove incorrect <tt>Cil_const.Build_Counter</tt>; use <tt>State_builder.SharedCounter</tt> instead.</li> -<li class="dev"><span class="kernel">[Cil]</span>  Various smart constructors and ast helper functions.</li> -<li class="dev-break"><span class="kernel">[Cil]</span>  Support for large constants in programs. My_bigint is now used instead of <tt>Int64.t</tt> in the AST. Fixes <a class="private" href="http://bts.frama-c.com/view.php?id=858">#858</a>.</li> -<li class="dev-break"><span class="kernel">[Cil]</span>  Improve performances of <tt>Cil_datatype.Typ</tt>.{{ "{" }}compare, equal, hash}.</li> -<li class="dev-break"><span class="kernel">[Cil]</span>  Removing types about validity status from the AST. Use module Property_status instead.</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  module Service_graph: function entry_point in input and output of functor Make now returns an option type.</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  Bts <a class="public" href="http://bts.frama-c.com/view.php?id=729">#729</a>: calling function <tt>Plugin.is_visible</tt> (resp. <tt>Plugin.is_invisible</tt>) forces to display (resp. prevents from displaying) the corresponding parameters in an help message.</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  <tt>Extlib.temp_file_cleanup_at_exit</tt> and <tt>Extlib.temp_dir_cleanup_at_exit</tt> may now raise exception Temp_file_error. They may raise an unspecified exception before.</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  Change semantics of ChangeDoChildrenPost for vstmt_aux. See developer's manual for more precision.</li> -<li class="dev"><span class="kernel">[Kernel]</span>  Fixed bug <a class="public" href="http://bts.frama-c.com/view.php?id=727">#727</a> (visiting a GFun spec in frama-c visitor was not done in the appropriate context).</li> -<li class="dev"><span class="kernel">[Kernel]</span>  New function <tt>File.create_rebuilt_project_from_visitor</tt></li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  Remove several kernel functions: <tt>Ast_info.pretty_vname</tt>: use <tt>Cil_datatype.Varinfo.pretty_vname</tt> <tt>Cil.print_utf8</tt>: use module <tt>Parameters.UseUnicode-</tt> <tt>Clexer.keep_comment</tt>: use module <tt>Parameters.PrintComments</tt> <tt>Cabshelper.continue_annot_error_set</tt>: <tt>Cabshelper.continue_annot_error_set</tt>: use <tt>Parameters.ContinueOnAnnotError.off</tt> all Cil, Cilmsg and CilE functions for pretty printing: use Kernel ones instead.</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  Following items are now deprecated: function <tt>Kernel_function.pretty_name</tt>: use <tt>Kernel_function.pretty</tt> module UseUnicode: use module Unicode.</li> -<li class="dev"><span class="kernel">[Kernel]</span>  <tt>Makefile.plugin</tt> and .dynamic more robust wrt external plugins (can make doc clean depend more easily; fixes bug <a class="public" href="http://bts.frama-c.com/view.php?id=754">#754</a>, improves bug <a class="public" href="http://bts.frama-c.com/view.php?id=742">#742</a>).</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  get rid of <tt>bin/sed_inplace</tt> (use ISED from <tt>share/Makefile.common</tt> where needed, which was the recommended way from the beginning).</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  Alternative signature for dataflow initial state. A few IntHash replaced by <tt>Stmt.Hashtbl</tt>.</li> -<li class="dev"><span class="kernel">[Kernel]</span>  Removed type <tt>Log.source</tt>. From now on all locations have type <tt>Lexing.position</tt>.</li> -<li class="dev"><span class="kernel">[Kernel]</span>  Fix bug <a class="public" href="http://bts.frama-c.com/view.php?id=790">#790</a>: AST integrity checker issue.</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  Remove Db_types module. All types are now in Cil_types. Moved type <tt>Alarms.t</tt> to <tt>Cil_types.alarm</tt>.</li> -<li class="dev"><span class="kernel">[Kernel]</span>  Kernel now accepts declarations as main entry point.</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  <tt>Kernel_function.find_return</tt> may now raise exception <tt>Kernel_function.No_Statement</tt>.</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  Module Parameters is dead. Each module corresponding to a parameters is moved to Kernel. Module <tt>Parameters.Dynamic</tt> is now <tt>Dynamic.Parameter</tt> while <tt>Parameters.get_selection_context</tt> is now <tt>Plugin.get_selection_context</tt>. You can use the script <tt>bin/carbon2nitrogen</tt> to perform the translation (almost) automatically.</li> -<li class="dev"><span class="kernel">[Kernel]</span>  New function <tt>File.new_machdep</tt> in order to register a new machdep dynamically.</li> -<li class="dev"><span class="kernel">[Kernel]</span>  <tt>Cil_datatype.LogicLabel</tt> implemented</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  <tt>Structural_descr.pack</tt> is now a private type. Use smart constructors instead.</li> -<li class="dev"><span class="kernel">[Kernel]</span>  New function <tt>Dynamic.is_plugin_present</tt>.</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  Most types of module Property are now private. Use smart constructors instead.</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  Remove Kernel_datatype (merge with Cil_datatatype).</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  new function <tt>Kernel_function.set_spec</tt> which must be called whenever the spec of a kf is modified.</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  Remove function <tt>CilE.update_gotos</tt>.</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  New way for handling abstract type in the type library.</li> -<li class="dev"><span class="kernel">[Kernel]</span>  Fix dynamic access to function [is_default] of parameters.</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  <tt>Dynamic.load_module</tt> searches in plugin path as advertised in its documentation</li> -<li class="dev"><span class="kernel">[Kernel]</span>  Exporting <tt>Property_status.self</tt> state</li> -<li class="dev"><span class="kernel">[Kernel]</span>  Ensures that a unique kf is generated per function in each project, avoid using kf for project A in project B.</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  Modification of <tt>Log.print_on_console</tt>. No more based on <tt>Format.kfprintf</tt> to avoid deadlock when error are raised by plugin pretty printers.</li> -<li class="dev"><span class="kernel">[Kernel]</span>  Adding option <tt>~dkey</tt> to <tt>Log.debug</tt> functions. See <tt>Log.Messages</tt> for details.</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  Properties_status is now called Property_status. Fully new interface.</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  Add IPLemma, IPNotacsl and IPConjunction as new constructors of <tt>Property.t</tt>; remove IPBehavior.</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  <tt>Annotations.replace</tt> and <tt>Globals.Annotations.replace_all</tt> are removed.</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  Signature of Plugin renamed for consistency. Use carbon2nitrogen for automatic translation.</li> -<li class="dev"><span class="kernel">[Kernel]</span>  Add <tt>Kernel.Unicode.without_unicode</tt>, which applies a function without upsetting the Unicode option in the gui.</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  Getters of <tt>Dynamic.Parameter</tt> now get an extra argument of type unit. May improve efficiency a lot.</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  Export datatype <tt>Varinfo.Hptset</tt>. Signature change in functor <tt>Abstract_interp.Make_Hashconsed_Lattice_Set</tt>.</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  Add parameter <tt>~with_locals</tt> to <tt>Db.accept_base</tt> (prior this, <tt>~with_locals</tt> was implicitly false)</li> -<li class="dev"><span class="kernel">[Kernel]</span>  Quadruple datatype.</li> -<li class="dev"><span class="kernel">[Kernel]</span>  Map_common_interface to have a merge function for Ocaml < <tt>3.12</tt>.</li> -<li class="dev"><span class="kernel">[Kernel]</span>  Copy visitor creates new kf before visiting a function, allowing to use it for creating <tt>Property.t</tt> items in the new project during visit (fixes <a class="private" href="http://bts.frama-c.com/view.php?id=942">#942</a>).</li> -<li class="dev-break"><span class="kernel">[Logic]</span>  Implementation of statement contracts for function behaviors.</li> -<li class="dev-break"><span class="kernel">[Logic]</span>  Add possibility to cast integer to C integral type when type-checking (Changes parameter of <tt>Logic_typing.Make</tt>)</li> -<li class="dev"><span class="kernel">[Logic]</span>  Fixes bug <a class="public" href="http://bts.frama-c.com/view.php?id=751">#751</a> (<tt>Cil.lconstant</tt> now returns terms of type integer and not int).</li> -<li class="dev"><span class="kernel">[Makefile]</span>  Add target to launch the tests of a specific dynamic internal plugin from Frama-C's main Makefile.</li> -<li class="dev"><span class="kernel">[Ptests]</span>  Ptests adds filename of current test before the options given to frama-c (see <a class="public" href="http://bts.frama-c.com/view.php?id=736">#736</a>).</li> -</ul> -<h2>Frama-C GUI</h2> -<h4>New Features</h4> -<ul class="entries"> -<li class="user"><span class="kernel">[Gui]</span>  Hide empty plugins columns in the filetree. Add support for hiding globals entirely.</li> -<li class="user"><span class="kernel">[Gui]</span>  Automatically show the main function at launch.</li> -<li class="user"><span class="kernel">[Gui]</span>  Menu to configure what is displayed in the filetree.</li> -<li class="user"><span class="kernel">[Gui]</span>  Add history for navigating source code.</li> -<li class="user"><span class="kernel">[Gui]</span>  Support to display the state of the absolute memory.</li> -<li class="user"><span class="kernel">[Gui]</span>  Double-clicking on a warning now displays the pretty-printed source location</li> -<li class="user-break"><span class="kernel">[Gui]</span>  Improve labels under the icons of the toolbar. Smart constructors in Menu_manager now require a label and a tooltip.</li> -</ul> -<h4>Developers Only</h4> -<ul class="entries"> -<li class="dev-break"><span class="kernel">[Gui]</span>  Signature change for Filetree#append_pixbuf_column.</li> -<li class="dev-break"><span class="kernel">[Gui]</span>  Signature change for Filetree#add_select_function, Filetree#select_global and <tt>Menu_manager.entry</tt>. Deprecate <tt>Design.apply_on_selected</tt>.</li> -<li class="dev"><span class="kernel">[Gui]</span>  Menu_manager now support check menus and toggle buttons</li> -</ul> -<h2>Plugin Aorai</h2> -<h4>New Features</h4> -<ul class="entries"> -<li class="user"> Deterministic automata.</li> -<li class="user"> Automaton is handled by contract of leaf functions.</li> -</ul> -<h4>Bug Fixes</h4> -<ul class="entries"> -<li class="bugfix"> State names used as enum constant are checked to be admissible fresh C identifiers.</li> -<li class="bugfix"> Fix issue in translation of guards + better error messages.</li> -<li class="bugfix"> Existing assigns are augmented with the locations corresponding to the instrumentation of the automaton.</li> -<li class="bugfix"> Generation of loop invariant for intermediate counter + fixes various issues</li> -</ul> -<h4>Developers Only</h4> -<ul class="entries"> -<li class="dev-break"> Redefinition of internal structures before enabling Ya extensions for sequences</li> -</ul> -<h2>Plugin Dataflow</h2> -<ul class="entries"> -<li class="user"> Improve precision of backwards dataflow algorithm and of postdominators on 'if' with a missing branch</li> -</ul> -<h2>Plugin Dominators</h2> -<ul class="entries"> -<li class="user">,Postdominators No feedback by default. Use <tt>-dominators-verbose</tt> 2 or <tt>-postdominators-verbose</tt> 2 if you need it.</li> -</ul> -<h2>Plugin From</h2> -<ul class="entries"> -<li class="user"> Display results function by function, instead of as one big block (may lower memory consumption considerably).</li> -<li class="bugfix"> Fix <a class="public" href="http://bts.frama-c.com/view.php?id=781">#781</a>: handling of function calls with an implicit cast for the assignment of the result.</li> -<li class="user"> Display name of called function when displaying results of option <tt>-calldeps</tt>.</li> -<li class="dev-break"> Minor interface changes in From. Replace some meaningless kinstr by stmt, and make the callbacks lazy.</li> -</ul> -<h2>Plugin Impact</h2> -<ul class="entries"> -<li class="bugfix"> Correct a journalisation bug in gui mode.</li> -<li class="bugfix"> Bug fixed when plug-in `Security_slicing' cannot be loaded or is incompatible with Impact.</li> -<li class="bugfix"> Bug fixed with '<tt>-impact-pragma</tt> f' on an unknown function f.</li> -</ul> -<h2>Plugin Inout</h2> -<h4>New Features</h4> -<ul class="entries"> -<li class="user"> Improved precision of the computation of operational inputs in presence of function calls.</li> -<li class="user"> Improved messages in presence of recursive calls</li> -<li class="user"> Correctness in presence of recursive calls. See issue <a class="public" href="http://bts.frama-c.com/view.php?id=733">#733</a>.</li> -<li class="user"> Operational inputs and outputs are now more precise for library functions: assigns clause are evaluated at each call.</li> -</ul> -<h4>Developers Only</h4> -<ul class="entries"> -<li class="dev-break"> <tt>Db.InOutContext</tt> becomes <tt>Db.Operational_inputs</tt>.</li> -<li class="dev-break"> Interface change. Non_contextual renamed to Cumulative_analysis.</li> -</ul> -<h2>Plugin Metrics</h2> -<ul class="entries"> -<li class="user"> New command-line options to compute the functions potentially called from a given function, and the percentage of functions analyzed by the value analysis.</li> -<li class="user"> Improves efficiency of metrics computation.</li> -</ul> -<h2>Plugin Occurrence</h2> -<ul class="entries"> -<li class="user"> Better pretty-printing: do not display internal ids anymore.</li> -<li class="bugfix"> Fixed bug when journalising.</li> -</ul> -<h2>Plugin Pdg</h2> -<ul class="entries"> -<li class="user"> Pdg can now be saved on disk.</li> -<li class="user"> Improved time and space complexity on big functions.</li> -<li class="bugfix"> Better precision in the dependencies. Fix bug <a class="public" href="http://bts.frama-c.com/view.php?id=787">#787</a>, <a class="public" href="http://bts.frama-c.com/view.php?id=789">#789</a> and <a class="public" href="http://bts.frama-c.com/view.php?id=802">#802</a> : infinite loops creation in slicing.</li> -<li class="bugfix"> Fix bug <a class="public" href="http://bts.frama-c.com/view.php?id=787">#787</a> but leads to less precise dependencies.</li> -</ul> -<h2>Plugin Postdominators</h2> -<ul class="entries"> -<li class="dev"> Add <tt>Db.PostdominatorsValue</tt>: postdominators taking into account value analysis results</li> -</ul> -<h2>Plugin Rte</h2> -<ul class="entries"> -<li class="user"> No longer position 'Don't know' statuses</li> -<li class="dev-break"> Correct plug-in name for dynamically registered RTE functions.</li> -<li class="user-break"> Option <tt>-rte-precond</tt> is not entailed by <tt>-rte-all</tt> anymore (precontion annotations must now be required explicitly).</li> -</ul> -<h2>Plugin Scope</h2> -<ul class="entries"> -<li class="user"> <tt>"Show Defs"</tt> is now an interprocedural analysis.</li> -</ul> -<h2>Plugin Security_slicing</h2> -<ul class="entries"> -<li class="bugfix"> Fixed bug <a class="public" href="http://bts.frama-c.com/view.php?id=768">#768</a> about exception raised when analysing variadic functions. A warning is now emitted: the function is ignored by the analyzer, thus the result is potentially incorrect.</li> -</ul> -<h2>Plugin Semantic</h2> -<ul class="entries"> -<li class="user"> Constant Folding All options are prefixed by <tt>"scf"</tt>. Use <tt>-scf-help</tt> for the details. Fixed <a class="private" href="http://bts.frama-c.com/view.php?id=946">#946</a>. Compatibility is preserved thanks to option aliases.</li> -</ul> -<h2>Plugin Slicing</h2> -<h4>New Feature</h4> -<ul class="entries"> -<li class="user-break"> Option <tt>-slice-print</tt> is now deprecated: use instead <normal slicing command> <tt>-then-on</tt> 'Slicing export' <tt>-print</tt></li> -</ul> -<h4>Bug Fixes</h4> -<ul class="entries"> -<li class="bugfix"> Fixed bug <a class="public" href="http://bts.frama-c.com/view.php?id=709">#709</a>: missing statements in sliced program.</li> -<li class="bugfix"> Fixed bug <a class="public" href="http://bts.frama-c.com/view.php?id=774">#774</a>: journalisation works again.</li> -<li class="bugfix"> Fix bug <a class="public" href="http://bts.frama-c.com/view.php?id=786">#786</a>: missing label in sliced program.</li> -<li class="bugfix"> Fix bug <a class="public" href="http://bts.frama-c.com/view.php?id=799">#799</a>: missing label in sliced program.</li> -<li class="bugfix"> Fix incorrect simplification of single-statement block in presence of label.</li> -<li class="bugfix"> Use correct function during generation of sliced project. Fixes <a class="private" href="http://bts.frama-c.com/view.php?id=950">#950</a>.</li> -</ul> -<h2>Plugin Syntactic</h2> -<ul class="entries"> -<li class="user"> Callgraph Fixed issue <a class="public" href="http://bts.frama-c.com/view.php?id=723">#723</a>: syntactic callgraph does not require an entry point anymore. If no entry point, services are less precise yet.</li> -</ul> -<h2>Plugin Users</h2> -<ul class="entries"> -<li class="user"> Calls to this plug-in are now written in the journal.</li> -</ul> -<h2>Plugin Value</h2> -<h4>New Features</h4> -<ul class="entries"> -<li class="user"> Uniformized message displayed when no information is available for a function.</li> -<li class="user"> Take Flush-To-Zero possibility into account for single-precision floats.</li> -<li class="user"> Improved informative messages about addresses of locals escaping their scope.</li> -<li class="user"> Improved option <tt>-subdivide-float-var</tt> when used without <tt>-all-rounding-modes</tt>. Improvement marginal for double computations and significant for float ones.</li> -<li class="user"> Each precondition can get a specific validity status.</li> -<li class="user-break"> Use hash-consed sets of statements, making many analyses faster and leaner for large functions or idioms that make functions large at normalization (<tt>e.g</tt>. large initialized local arrays).</li> -<li class="user"> Improved results for operation % by zero. Removed message about binary operators raising exceptions.</li> -<li class="user"> Option <tt>-val-after-results</tt> to control the recording of post-statement states. Active by default in the GUI.</li> -<li class="user"> Alarms may pretty print the abstract value culprit for the potential violation. This is particularly informative for certain alarms.</li> -<li class="user"> New option <tt>-no-val-show-progress</tt></li> -<li class="user"> More aggressive state reduction when emitting pointer_comparable assertions. Use option <tt>-undefined-pointer-comparison-propagate-all</tt> if you liked the old behavior better.</li> -<li class="user"> Literal strings are now read-only.</li> -<li class="user"> Emit <tt>\pointer_comparable</tt> alarm for unspecified. equality test between literal strings such as <tt>"foo"</tt> == <tt>"foo"</tt>.</li> -<li class="user"> New builtin Frama_C_dump_each_file, which dumps the entire memory state into successive files.</li> -<li class="user"> Option <tt>-val-builtin</tt>: experimental support for builtins that can fail (by calling a fallback C function).</li> -<li class="user"> More precise when an alarm is emitted in a loop.</li> -<li class="user"> Postconditions containing <tt>\old</tt> are now handled.</li> -<li class="user"> Uses <tt>"complete behaviors"</tt> information.</li> -<li class="user"> Loop invariants are now used to improve analysis.</li> -<li class="user-break"> Improve behavior in presence of errors during the computation of the initial state. Allow non ISO global initializers using the value of constant globals defined earlier.</li> -<li class="user"> Improve handling of assigns in library functions.</li> -<li class="user"> Remove non-relevant variables from the 'Modifies' clauses of the GUI.</li> -<li class="user"> Wide strings more supported.</li> -<li class="user"> Better message when interpretation stops for a function argument.</li> -<li class="user"> Improved precision when using <tt>-all-rounding-modes</tt>.</li> -<li class="user"> Improved precision of &.</li> -<li class="user"> New informative message when not using. <tt>-val-signed-overflow-alarms</tt> <tt>"2's complement assumed for overflow"</tt></li> -<li class="user"> Raised cut-off limit between sets and intervals from 7 to 8 elements.</li> -<li class="user"> Improved precision of if (x!=c) when the value set of x is an interval of 9 elements.</li> -<li class="user"> New alarm, for programs that do not respect C99 <tt>6.5</tt>.<tt>16.1</tt>:3 (overlapping assignment from lvalue to lvalue). Partially supported (not emitted in some cases).</li> -<li class="user"> New option <tt>-remove-redundant-alarms</tt> for removing redundant alarms. This was previously done by default. Use this option if you are going to inspect alarms emitted by Value.</li> -<li class="user"> Do not continue evaluating successive 'requires' or 'ensures' clauses if one of them is false.</li> -<li class="user"> New alarm for left shift of negative values. Minor other changes related to shift operation alarms.</li> -</ul> -<h4>Bug Fixes</h4> -<ul class="entries"> -<li class="bugfix"> Changes related to 0., +0., -0., sort of thing. Unwarranted loss of precision fixed.<br/><br/></li> -<li class="bugfix"> Fixed representation of unknown single-precision floats in initial context (it used to be the same as for an unknown double).</li> -<li class="bugfix"> Fixed crash when passing invalid argument to function, found by John Regehr using random testing (jrrt).</li> -<li class="bugfix"> Fixed correctness bug involving nested structs (jrrt).</li> -<li class="bugfix"> Fixed forgotten warning when passing completely undefined lvalue as argument to function. (jrrt)</li> -<li class="bugfix"> Fixed bug when passing bitfield as argument to function. (jrrt)</li> -<li class="bugfix"> Fixed bug when passing struct as argument to function with a big-endian target architecture.</li> -<li class="bugfix"> Fixed bug <a class="public" href="http://bts.frama-c.com/view.php?id=732">#732</a>: Synthetic results were partial when <tt>-slevel</tt> was set not high enough to unroll loops completely.</li> -<li class="bugfix"> Fixed correctness bug when bitfield initializer exceeds range (bug <a class="public" href="http://bts.frama-c.com/view.php?id=721">#721</a>) (jrrt).</li> -<li class="bugfix"> Fixed crash with ACSL assertions involving floating-point variables (bug <a class="public" href="http://bts.frama-c.com/view.php?id=752">#752</a>).</li> -<li class="bugfix"> Some floating-point alarms could be printed several times. Fixed.</li> -<li class="bugfix"> Fixed bug <a class="public" href="http://bts.frama-c.com/view.php?id=689">#689</a>. Each postcondition can get a specific validity status.</li> -<li class="bugfix"> Correctly emit <tt>\pointer_comparable</tt>(...) alarms.</li> -<li class="bugfix"> Fix bug <a class="public" href="http://bts.frama-c.com/view.php?id=798">#798</a>: calls to functions that return a value with latent conversion.</li> -<li class="bugfix"> Fixed crash for high values of <tt>-subdivide-float-var</tt></li> -<li class="bugfix"> Fixed bug when bitfield receives the result of a function call (bug <a class="public" href="http://bts.frama-c.com/view.php?id=819">#819</a>).</li> -<li class="bugfix"> Fixed undocumented builtin is_base_aligned.</li> -<li class="bugfix"> Remove some uneeded warnings when comparing function pointers with NULL. Fixes bug <a class="private" href="http://bts.frama-c.com/view.php?id=855">#855</a>.</li> -<li class="bugfix"> Much more clever when interpreting logic terms, including those containing <tt>\old</tt> (eg. formals in postconditions)</li> -</ul> -<h4>Developers Only</h4> -<ul class="entries"> -<li class="dev-break"> Minor interface changes in Value. Replace some meaningless kinstr by stmt, and make the callbacks lazy.</li> -<li class="dev"> Defunctorized Lattice_Interval_Set.</li> -<li class="dev"> Changed representation of bases for literal strings in preparation of related checks.</li> -<li class="dev-break"> Functions valid_* now take an argument <tt>~for_writing</tt> Pass true when the lvalue being considered is used for writing in the program. Pass false when unsure.</li> -<li class="dev-break"> Add argument <tt>"exact"</tt> to <tt>Lmap.paste_offsetmap</tt> (which was preciously supposed to be always true).</li> -<li class="dev-break"> Module Cvalue_type renamed to Cvalue. Module Relations_type removed. Use Cvalue instead.</li> -<li class="dev-break"> Add some missing <tt>~with_alarms</tt> arguments, notably to offsetmaps copy and paste.</li> -<li class="dev-break"> Signature change in CilE: plugins that want to emit Value analysis alarms must define their own emitters.</li> -<li class="dev-break"> Changed the representation of <tt>Ival.t</tt>. If an external plug-in matches <tt>"Ival.Set s"</tt>, a simple fix is to add <tt>"let s = Ival.set_of_array s in"</tt> as first line of that case.</li> -</ul> -</div> -<hr><div><a id="Carbon-6.2" href="#Carbon-6.2"></a></div><h3 class="release">Carbon Release <span class="hversion">[6.2]</span></h3> - -<div class="release"> -<h2>Frama-C General</h2> -<h4>New Features</h4> -<ul class="entries"> -<li class="user-break"><span class="kernel">[Configure]</span>  Frama-C does not require Apron anymore (Why does for Jessie). Thus fix bug <a class="public" href="http://bts.frama-c.com/view.php?id=647">#647</a>.</li> -<li class="user"><span class="kernel">[Kernel]</span>  Improve performance on platform with <tt>dynami.c</tt> loading. Mainly impact value analysis (for developers: improve efficiency of <tt>Dynamic.get</tt>).</li> -<li class="user-break"><span class="kernel">[Kernel]</span>  Handle errors better when they occur when exiting Frama-C. Slight semantic changes for exit code: - old code 5 is now 127; - code 5 is now: error raised when exiting Frama-C normally; - code 6: error raised when exiting Frama-C abnormally.</li> -<li class="user"><span class="kernel">[Logic]</span>  Fix priority bug in parser.</li> -<li class="user"><span class="kernel">[Logic]</span>  Mentioning a formal on the left-hand side of an assigns clause is now an error when type-checking logic annotations.</li> -<li class="user"><span class="kernel">[Makefile]</span>  Fixed bug <a class="private" href="http://bts.frama-c.com/view.php?id=638">#638</a>. By default, warnings are no more errors when compiling a public Frama-C distribution and plug-ins. SVN versions of Frama-C are still compiled with <tt>"-warn-error A"</tt>.</li> -</ul> -<h4>Bug Fixes</h4> -<ul class="entries"> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Fixed <a class="private" href="http://bts.frama-c.com/view.php?id=313">#313</a>. Entry point with a specification is no longer wiped out.</li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Fixed bug if an empty string is given on the command line while an option name is expected. There is now a proper error message.</li> -<li class="bugfix"><span class="kernel">[Makefile]</span>  Fixed bug <a class="public" href="http://bts.frama-c.com/view.php?id=637">#637</a>: <tt>"make install -n"</tt> did wrongly create directories.</li> -<li class="bugfix"><span class="kernel">[Makefile]</span>  Fixed bug <a class="private" href="http://bts.frama-c.com/view.php?id=660">#660</a> related to a default Frama-C-compatible ocamlgraph installation under Cygwin (<tt>i.e</tt>. in a Win32 path containing the ':' character).</li> -</ul> -<h4>Developers Only</h4> -<ul class="entries"> -<li class="dev"><span class="kernel">[Cil]</span>  Fixed bug <a class="public" href="http://bts.frama-c.com/view.php?id=645">#645</a>. <tt>Ast_info.constant_expr</tt>, Cil.[zero,one,new_exp,makeZeroInit,mone,kinteger64_repr, kinteger64,kinteger,integer,constFoldBinOp,mkAddrOf, mkAddrOrStartOf,mkString,parseInt,sizeOf] no longer use an optional argument ?loc. It is now a non optional labeled argument. Previous default value of loc was <tt>~loc</tt>:<tt>Cil_datatype.Location.unknown</tt> which is most of the time not accurate.<br/><br/></li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  Remove API function <tt>Messages.enable_collect</tt>: please let the kernel do the job.</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  Remove <tt>Messages.disable_echo</tt> (can be done using Log module) and <tt>Messages.depend</tt> (can be done using <tt>Messages.self</tt>).</li> -<li class="dev"><span class="kernel">[Kernel]</span>  New function in API: <tt>Kernel_function.find_syntactic_callsites</tt>.</li> -<li class="dev"><span class="kernel">[Kernel]</span>  Fix bug <a class="public" href="http://bts.frama-c.com/view.php?id=677">#677</a>. As a side-effect, function <tt>Plugin.add_alias</tt> is now deprecated and replaced by <tt>Plugin.add_aliases</tt>.</li> -<li class="dev"><span class="kernel">[Kernel]</span>  New syntactic context for memory accesses with user-supplied validity range.</li> -<li class="dev-break"><span class="kernel">[Logic]</span>  Refactoring of assigns and from AST representation and of <tt>Property.identified_property</tt>.</li> -</ul> -<h2>Frama-C GUI</h2> -<h4>New Features</h4> -<ul class="entries"> -<li class="user-break"><span class="kernel">[Gui]</span>  Gui options start by <tt>-gui</tt> and not <tt>-GUI</tt></li> -<li class="user"><span class="kernel">[Gui]</span>  Implement feature <a class="public" href="http://bts.frama-c.com/view.php?id=635">#635</a>: display messages in the messages panel while loading a batch session in the GUI. The batch session must have been previously executed with the new option <tt>-collect-messages</tt>.</li> -<li class="user"><span class="kernel">[Gui]</span>  Display more precise state after statement (http://<tt>blog.frama-c</tt>.<tt>com/index.php</tt>?<tt>post/2011/01/11/Seven-errors-game</tt>).</li> -</ul> -<h4>Bug Fixes</h4> -<ul class="entries"> -<li class="bugfix"><span class="kernel">[Gui]</span>  Fixed 100% cpu load while external command are launched.</li> -<li class="bugfix"><span class="kernel">[Gui]</span>  Fixed bug <a class="public" href="http://bts.frama-c.com/view.php?id=666">#666</a>. Do not display misleading <tt>"After statement"</tt>.</li> -</ul> -<h4>Developers Only</h4> -<ul class="entries"> -<li class="dev"><span class="kernel">[Gui]</span>  Added support for icons in <tt>Gtk_helper.Icon</tt>.</li> -</ul> -<h2>Plugin Inout</h2> -<ul class="entries"> -<li class="bugfix"> Return statement dependencies were forgotten in operational input computations. Fixed.</li> -</ul> -<h2>Plugin Report</h2> -<ul class="entries"> -<li class="dev"> Option <tt>-report</tt> no longer survive after <tt>-then</tt>.</li> -</ul> -<h2>Plugin Slicing</h2> -<ul class="entries"> -<li class="bugfix"> Fixed bug <a class="public" href="http://bts.frama-c.com/view.php?id=673">#673</a>.</li> -<li class="user"> New options added for fixing bug <a class="public" href="http://bts.frama-c.com/view.php?id=668">#668</a>.</li> -</ul> -<h2>Plugin Sparecode</h2> -<ul class="entries"> -<li class="dev"> API modified for fixing <a class="public" href="http://bts.frama-c.com/view.php?id=668">#668</a>.</li> -</ul> -<h2>Plugin Value</h2> -<h4>New Features</h4> -<ul class="entries"> -<li class="user"> Improved precision of | operator.</li> -<li class="user"> New alarm for float -> int cast overflows.</li> -<li class="user"> Added check that denormals work correctly on host computer (correction would be affected otherwise).</li> -<li class="user"> Improved precision of & operator.</li> -<li class="user"> Interpretation of ==> in ACSL annotations.</li> -<li class="user"> Disabled incorrect interpretation of ACSL statement contracts.</li> -<li class="user"> Improve performance of callbacks.</li> -<li class="user"> Various minor speed improvements.</li> -<li class="user"> More aggressive handling of if(x>e) where x has type double.</li> -<li class="user"> Change in initial states generated by <tt>-lib-entry</tt> Much smaller. Perhaps more representative.</li> -<li class="user"> Generate independent assertions for signed overflow and signed underflow. In many cases only one is generated (win!).</li> -<li class="user"> Is is now possible to call Frama_C_show_each without ..._x.</li> -<li class="user"> Changes in Frama_C_memcpy built-in. Still not perfect.</li> -</ul> -<h4>Bug Fixes</h4> -<ul class="entries"> -<li class="bugfix"> Fixed obscure crash that could happen during very imprecise analyses.</li> -<li class="bugfix"> Fixed correctness bug involving pointers to signed integer pointing to memory locations containing unsigned integers or vice versa.</li> -</ul> -<h4>Developers Only</h4> -<ul class="entries"> -<li class="dev"> New callback for recording the state after a statement.</li> -<li class="dev-break"> Renamed copy to copy_offsmap in Offsetmaps. The name <tt>"copy"</tt> clashed with Datatypes.</li> -</ul> -<h2>Plugin WP</h2> -<ul class="entries"> -<li class="user"> Plug-in WP removed from kernel-releases (now an independent plug-in).</li> -</ul> -</div> -<hr><div><a id="Carbon-6.1" href="#Carbon-6.1"></a></div><h3 class="release">Carbon Release <span class="hversion">[6.1]</span></h3> - -<div class="release"> -<h2>Plugin WP</h2> -<ul class="entries"> -<li class="bugfix"> Fixed bug <a class="public" href="http://bts.frama-c.com/view.php?id=639">#639</a>: no more Coq compilation to shared directory.</li> -<li class="user"> Accessibility of all provers from gui.<br/><br/></li> -</ul> -</div> -<hr><div><a id="Carbon-6.0" href="#Carbon-6.0"></a></div><h3 class="release">Carbon Release <span class="hversion">[6.0]</span></h3> - -<div class="release"> -<h2>Frama-C General</h2> -<h4>New Features</h4> -<ul class="entries"> -<li class="user"><span class="kernel">[Cil]</span>  Be less aggressive during inline function merge. Alpha equivalent function are now kept separate.</li> -<li class="user-break"><span class="kernel">[Cil]</span>  Clean up local variables handling and pretty-printing modified pBlock method interface (unified pBlock and pInnerBlock)</li> -<li class="user-break"><span class="kernel">[Cil]</span>  Cil normalization takes care of abrupt clauses</li> -<li class="user"><span class="kernel">[Configure]</span>  Better detection of native dynlink support.</li> -<li class="user"><span class="kernel">[Kernel]</span>  Feature <a class="public" href="http://bts.frama-c.com/view.php?id=484">#484</a> about requires into named behaviors</li> -<li class="user-break"><span class="kernel">[Kernel]</span>  Fixed bug <a class="public" href="http://bts.frama-c.com/view.php?id=548">#548</a>: <tt>limit.h</tt> now syntactically correct. Architectures other than x86_32 still unsupported.</li> -</ul> -<h4>Bug Fixes</h4> -<ul class="entries"> -<li class="bugfix"><span class="kernel">[Cil]</span>  Extended grammar of pragma lines.</li> -<li class="bugfix"><span class="kernel">[Cil]</span>  Fixed bugs <a class="public" href="http://bts.frama-c.com/view.php?id=451">#451</a> (break outside of <tt>loop/switch</tt>) and <a class="public" href="http://bts.frama-c.com/view.php?id=452">#452</a> (spurious 'body of f call falls through' warnings)</li> -<li class="bugfix"><span class="kernel">[Cil]</span>  Fixed bug <a class="public" href="http://bts.frama-c.com/view.php?id=440">#440</a> (remove spurious block generation at parsing time that clashed with label scoping rule in ACSL)</li> -<li class="bugfix"><span class="kernel">[Cil]</span>  Fixed <a class="public" href="http://bts.frama-c.com/view.php?id=542">#542</a> (now raises parse error when C function call dot not provide correct number of arguments)</li> -<li class="bugfix"><span class="kernel">[Configure]</span>  Fixed bug in configuration of external plug-ins</li> -<li class="bugfix"><span class="kernel">[Configure]</span>  get rid of <tt>known_plugins.ac</tt> (fix <a class="public" href="http://bts.frama-c.com/view.php?id=462">#462</a>)</li> -<li class="bugfix"><span class="kernel">[Configure]</span>  Always configure OcamlGraph local version (if used) when configuring Frama-C.</li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Fixed bug in handling of <tt>-cpp-command</tt></li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Tried to fix all permissions on *.{{ "{" }}c,h} files</li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  CL options for cabs2cil flags (fix <a class="public" href="http://bts.frama-c.com/view.php?id=506">#506</a>)</li> -<li class="bug-break"><span class="kernel">[Kernel]</span>  Fixed <a class="public" href="http://bts.frama-c.com/view.php?id=620">#620</a> (default assigns generation).</li> -<li class="bugfix"><span class="kernel">[Logic]</span>  fix bug <a class="private" href="http://bts.frama-c.com/view.php?id=454">#454</a> (multiple labels in same statement)</li> -<li class="bugfix"><span class="kernel">[Logic]</span>  Fixed wrong precedence of <==></li> -<li class="bugfix"><span class="kernel">[Logic]</span>  Checking for loop variant position</li> -<li class="bugfix"><span class="kernel">[Logic]</span>  Fix bug <a class="private" href="http://bts.frama-c.com/view.php?id=498">#498</a> (behaviors within same scope must now have unique names)</li> -<li class="bugfix"><span class="kernel">[Logic]</span>  ACSL identifiers starting with a \ are not replaced by pre-processing when a macro of the same name exists (fix <a class="public" href="http://bts.frama-c.com/view.php?id=541">#541</a>)</li> -<li class="bugfix"><span class="kernel">[Logic]</span>  Better error messages for logic parser and other fix (fix <a class="public" href="http://bts.frama-c.com/view.php?id=512">#512</a>, <a class="public" href="http://bts.frama-c.com/view.php?id=538">#538</a>, <a class="private" href="http://bts.frama-c.com/view.php?id=553">#553</a>, <a class="private" href="http://bts.frama-c.com/view.php?id=560">#560</a>)</li> -<li class="bugfix"><span class="kernel">[Logic]</span>  Fixed <a class="public" href="http://bts.frama-c.com/view.php?id=549">#549</a> (Arrays in the logic)</li> -<li class="bugfix"><span class="kernel">[Logic]</span>  Fixed <a class="public" href="http://bts.frama-c.com/view.php?id=570">#570</a> (implicit conversion to void*) and fixes issue in overloading resolution</li> -<li class="bugfix"><span class="kernel">[Logic]</span>  Priority is used for pretty printing predicates.</li> -<li class="bugfix"><span class="kernel">[Makefile]</span>  Fixed potential generation of corrupted .o</li> -<li class="bugfix"><span class="kernel">[Makefile]</span>  Fix bug <a class="public" href="http://bts.frama-c.com/view.php?id=460">#460</a> when using a non-local ocamlgraph</li> -<li class="bugfix"><span class="kernel">[Makefile]</span>  Fix bug <a class="public" href="http://bts.frama-c.com/view.php?id=461">#461</a> when installing the GUI on a bytecode-only architecture</li> -<li class="bugfix"><span class="kernel">[Makefile]</span>  Fix bug <a class="public" href="http://bts.frama-c.com/view.php?id=528">#528</a> when building a dynamic plug-in in a sandbox.</li> -</ul> -<h4>Developers Only</h4> -<ul class="entries"> -<li class="dev-break"><span class="kernel">[Cil]</span>  Remove deprecated annotation_status of AAssert in the AST</li> -<li class="dev"><span class="kernel">[Cil]</span>  Fix bug <a class="public" href="http://bts.frama-c.com/view.php?id=489">#489</a>: constant literal present in original source are preserved in the AST. NB: this implies that they might be explicitly cast when an integer conversion occur.</li> -<li class="dev"><span class="kernel">[Cil]</span>  Support for custom extension in grammar of behaviors. See <tt>Logic_typing.register_behavior_extension</tt>.</li> -<li class="dev-break"><span class="kernel">[Cil]</span>  Preliminary support for function calls in UnspecifiedSequence</li> -<li class="dev"><span class="kernel">[Cil]</span>  <tt>Cil.makeLocalVar</tt> now inserts the variable into one of the function's local blocks.</li> -<li class="dev-break"><span class="kernel">[Cil]</span>  global_annotation has location information</li> -<li class="dev-break"><span class="kernel">[Cil]</span>  Removed function varinfo_from_vid. You can use maps or hashtables indexed by varinfos directly instead.</li> -<li class="dev-break"><span class="kernel">[Cil]</span>  Cil and Cabs expression have now a location.</li> -<li class="dev-break"><span class="kernel">[Cil]</span>  Changed ignored pure exp hook + hook for conditional evaluation of side-effects</li> -<li class="dev-break"><span class="kernel">[Cil]</span>  Extending logic label for plugin purpose.</li> -<li class="dev-break"><span class="kernel">[Cil]</span>  Changed type of doGuard in forward dataflow</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  Ptmap (resp. Ptset) is renamed into Hptmap (Hptset)</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  Fix bug <a class="private" href="http://bts.frama-c.com/view.php?id=441">#441</a> (keep track of original names in AST)</li> -<li class="dev"><span class="kernel">[Kernel]</span>  Deprecate <tt>Globals.Functions.find_englobing_kf</tt>. Use <tt>Kernel_function.find_englobing_kf</tt> which has a much better complexity instead.</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  Added field b_extended in behaviors to support grammar extensions</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  New implementation of module Properties_status</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  Major changes in the kernel. Mainly merge the old modules Datatype and Type into a single most powerful library called Type. The API of these libraries changes.<br/><br/> Consequently, some other API changes. By side effect, a lot of functions of module Cilutil has been removed and replaced by their counterpart in module Cil_datatype.<br/><br/> The script <tt>bin/boron2carbon.sh</tt> fixes most changes automatically. Feel free to use it to upgrade your plug-in.<br/><br/> In the process, some minor bugs found and fixed in the Frama-C kernel.</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  <tt>File.check_file</tt> takes a new argument, allowing to describe which AST fails integrity check in case of trouble.</li> -<li class="dev"><span class="kernel">[Kernel]</span>  New Task module: a monadic library for calling asynchronous commands from the toplevel and the gui.</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  Remove function <tt>Globals.has_entry_point</tt>. Use <tt>Globals.entry_point</tt> instead.</li> -<li class="dev-break"><span class="kernel">[Logic]</span>  Parameterize search of field in logic typing functor in a similar way to search of other C symbols</li> -<li class="dev"><span class="kernel">[Logic]</span>  Fix bug <a class="public" href="http://bts.frama-c.com/view.php?id=505">#505</a> (Associate default label for predicates with a single label parameter and no argument)</li> -<li class="dev-break"><span class="kernel">[Project]</span>  Reimplementation of the project library (the contents of directory <tt>src/project</tt>). New API.</li> -<li class="dev"><span class="kernel">[Ptests]</span>  Slightly changed semantics of CMD and STDOPT. See developer manual for more info</li> -</ul> -<h2>Frama-C GUI</h2> -<h4>New Features</h4> -<ul class="entries"> -<li class="user"><span class="kernel">[Gui]</span>  Better graph display. Require ocamlgraph > <tt>1.4</tt></li> -<li class="user"><span class="kernel">[Gui]</span>  First support for persistent GUI configuration. GtkPaned ratios, main and launcher window dimensions are saved to file <tt>frama-c-gui.config</tt> in the user's home directory.</li> -<li class="user"><span class="kernel">[Gui]</span>  In expressions 't[v]', allow to select 't' (when it is a variable). To select the entire expression 't[v]', click on the ']' on the right.</li> -<li class="user"><span class="kernel">[Gui]</span>  One tooltip by parameter in the launcher</li> -<li class="user-break"><span class="kernel">[Gui]</span>  New graph viewer, requires ocamlgraph > <tt>1.5</tt></li> -</ul> -<h4>Bug Fixes</h4> -<ul class="entries"> -<li class="bugfix"><span class="kernel">[Gui]</span>  Fix bug with toolbar button 'duplicate project'</li> -<li class="bugfix"><span class="kernel">[Gui]</span>  Fixed parsing of floats in <tt>frama-c-gui.config</tt></li> -</ul> -<h2>Plugin From</h2> -<ul class="entries"> -<li class="user"> Improved interpretation of assigns clauses</li> -</ul> -<h2>Plugin Inout</h2> -<h4>New Features</h4> -<ul class="entries"> -<li class="user"> Improved precision of <tt>-inout</tt> with possibly invalid pointers.</li> -<li class="user"> New option <tt>-inout-with-formals</tt> similar to <tt>-inout</tt> but without locals and with formals</li> -<li class="user"> Improve option <tt>-inout-with-formals</tt>: cleanup local variables that come from out of call tree functions.</li> -<li class="user"> Improved precision for option <tt>-inout-with-formals</tt></li> -<li class="user"> Clean local variables passed by address to callees from results of <tt>-input</tt>, <tt>-out</tt>, <tt>-deps</tt></li> -<li class="user"> Improve printing of <tt>-out</tt> <tt>-input</tt> <tt>-deps</tt></li> -</ul> -<h4>Bug Fix</h4> -<ul class="entries"> -<li class="bugfix"> Fixed bug in <tt>-inout</tt> where operational inputs of called library function were improperly inferred from assigns</li> -</ul> -<h2>Plugin Obfuscator</h2> -<ul class="entries"> -<li class="user-break"> Option <tt>-obfuscate</tt> is now part of a new dynamic plug-in `Obfuscator' (fixed issue <a class="private" href="http://bts.frama-c.com/view.php?id=265">#265</a>). The behaviour of this option is now journalized and may be run by other plug-ins.</li> -</ul> -<h2>Plugin Occurrence</h2> -<ul class="entries"> -<li class="bugfix"> Fix bug <a class="public" href="http://bts.frama-c.com/view.php?id=550">#550</a>: crash when selecting an occurrence if the entry point set by <tt>"-main"</tt> is incorrect.</li> -</ul> -<h2>Plugin Security_slicing</h2> -<ul class="entries"> -<li class="user"> Only use the GUI; does not require it anymore</li> -</ul> -<h2>Plugin Slicing</h2> -<ul class="entries"> -<li class="bugfix"> Fixed bug <a class="private" href="http://bts.frama-c.com/view.php?id=448">#448</a> about <tt>-keep-annotations</tt> option</li> -</ul> -<h2>Plugin Syntactic</h2> -<ul class="entries"> -<li class="bugfix"> callgraph Fixed bug <a class="private" href="http://bts.frama-c.com/view.php?id=587">#587</a>: proper error message when the entry point is invalid.</li> -</ul> -<h2>Plugin Value</h2> -<h4>New Features</h4> -<ul class="entries"> -<li class="user"> Optimization in the handling of library functions</li> -<li class="user"> More optimization of library functions</li> -<li class="user"> Yet more small improvements in value analysis of large programs.</li> -<li class="user"> Variables now uninitialized by default. Improves <tt>-deps</tt>, <tt>-input</tt>, <tt>-output</tt> when addresses of local variables are passed as arguments of called functions.</li> -<li class="user"> Tweak in <tt>-slevel</tt>* options. A little slower for some programs, much faster for others.</li> -<li class="user"> More consistent naming scheme for generating shorter names when using <tt>-lib-entry</tt>. <tt>"star_"</tt> becomes <tt>"S_"</tt>.</li> -<li class="user"> Improved Frama_C_memcpy built-in.</li> -<li class="user"> Improved precision of analysis for program short s[]= {{ "{" }}0,1,0,1,0,1,0,1,0,1,0,1,0,1,0,1};main(){{ "{" }}return((int*)s)[u()];}</li> -<li class="user-break"> Structures passed as function arguments now precisely handled.</li> -<li class="user-break"> Abort analysis when recursion is encountered.</li> -<li class="user"> Clean local variables passed by address to callees from results of <tt>-val</tt>.</li> -<li class="user"> Lowered memory consumption slightly.</li> -<li class="user"> <tt>"assert(TODO)"</tt>, used when a property to check in the analyzed code cannot be expressed as ACSL and the user should read the English explanation (<tt>e.g</tt>. "accessing uninitialized left-value") instead, could look unprofessional to the superficial onlooker. <tt>"assert(Ook)"</tt> will now be used instead.</li> -<li class="user"> Do not emit alarm for uninitialized arguments to non-library functions. Necessary for structs. Relevant messages changed a little.</li> -<li class="user"> Improved speed of options <tt>-slevel</tt>* for arguments in the thousands. Synthetizing results remains slow, so consider options <tt>-no-results</tt>* if you take advantage of them.</li> -<li class="user"> Emit alarm for uninitialized arguments to library functions.</li> -<li class="user"> Preliminary support for interpreting C type float as IEEE 754 single-precision.</li> -<li class="user"> New option named <tt>-undefined-pointer-comparison-propagate-all</tt></li> -<li class="user"> Removed undocumented option <tt>-float-digits</tt></li> -<li class="user"> New option <tt>-float-normal</tt> (undocumented)</li> -</ul> -<h4>Bug Fixes</h4> -<ul class="entries"> -<li class="bugfix"> Fixed bug with extern variables of incomplete type</li> -<li class="bugfix"> Fixed correctness bug involving the comparison of a variable of type float or double.</li> -<li class="bugfix"> Do not emit an alarm for the comparison of function addresses to NULL.</li> -<li class="bugfix"> Some <tt>"Misaligned"</tt> imprecision origins were wrongly classified as <tt>"Arithmetic"</tt>. Fixed.</li> -<li class="bugfix"> Fixed bug involving typedefs when using option <tt>-val-signed-overflow-alarms</tt>.</li> -<li class="bugfix"> Fixed performance bug that could lead to "stack overflow" error during large analyses.</li> -<li class="bugfix"> Fixed memory leak.</li> -<li class="bugfix"> Disappearance of non termination messages from the log. The messages were inconsistent.</li> -<li class="bugfix"> Emit alarm for overflowing floating-point constants instead of crashing.</li> -<li class="bugfix"> Emit proper ACSL alarm for overflowing floating-point binary and unary operators. Fixed <a class="public" href="http://bts.frama-c.com/view.php?id=259">#259</a>.</li> -<li class="bugfix"> Do not evaluate annotations right after propagation is stopped.</li> -<li class="bugfix"> Fixed bug that could happen in programs casting address of floating-point type to address of integer type</li> -</ul> -<h4>Developers Only</h4> -<ul class="entries"> -<li class="dev-break"> There was one too many function called <tt>"find_ival"</tt>. One was renamed to <tt>"project_ival"</tt>.</li> -<li class="dev-break"> Function <tt>Cvalue_type.V.is_top</tt> rebaptized is_imprecise</li> -<li class="dev-break"> Renamed <tt>Int.eq</tt> into <tt>Int.equal</tt>. Removed <tt>Int.neq</tt></li> -</ul> -</div> -<hr><div><a id="Boron-5.0" href="#Boron-5.0"></a></div><h3 class="release">Boron Release <span class="hversion">[5.0]</span></h3> - -<div class="release"> -<h2>Frama-C General</h2> -<h4>New Features</h4> -<ul class="entries"> -<li class="user"><span class="kernel">[Cil]</span>  Extend logic pretty printer to handle all specific clauses</li> -<li class="user"><span class="kernel">[Configure]</span>  Dynamic plug-ins are now statically linked by default whenever native dynlink is not usable (bts <a class="private" href="http://bts.frama-c.com/view.php?id=301">#301</a>).</li> -<li class="user-break"><span class="kernel">[Configure]</span>  Compiling the GUI now requires LablGnomeCanvas.</li> -<li class="user"><span class="kernel">[Kernel]</span>  Add status for all clauses</li> -<li class="user"><span class="kernel">[Kernel]</span>  Clarification of the multiple accesses warning. Becomes <tt>"undefined multiple accesses in expression"</tt>.</li> -<li class="user"><span class="kernel">[Kernel]</span>  Better error messages when a dynamic plug-in cannot be loaded.</li> -<li class="user"><span class="kernel">[Kernel]</span>  Better -*<tt>-help</tt>.</li> -<li class="user"><span class="kernel">[Kernel]</span>  New option <tt>-no-dynlink</tt> in order to prevent loading of dynamic plug-ins.</li> -<li class="user-break"><span class="kernel">[Kernel]</span>  The journal is generated only if the GUI is crashing, or if the option <tt>-journal-enable</tt> is explicitly set (fixed issue <a class="private" href="http://bts.frama-c.com/view.php?id=330">#330</a>).</li> -<li class="user"><span class="kernel">[Kernel]</span>  Backtrace when Frama-C is crashing (only if Frama-C is compiled with caml >= <tt>3.11</tt>.0)</li> -<li class="user"><span class="kernel">[Kernel]</span>  New option <tt>"-plugin-h"</tt> as an alias for option <tt>"-plugin-help"</tt></li> -<li class="user"><span class="kernel">[Kernel]</span>  Preliminary standard C library in $<tt>FRAMAC_SHARE/libc</tt></li> -<li class="user"><span class="kernel">[Logic]</span>  Better error message when using = in annotations</li> -<li class="user"><span class="kernel">[Logic]</span>  ordering of clauses in contracts</li> -<li class="user"><span class="kernel">[Logic]</span>  If a C typedef integer, real or boolean exists, it takes precedence over corresponding logic type. The logic type remains accessible through its utf-8 denomination.</li> -<li class="user-break"><span class="kernel">[Logic]</span>  Support for type abbreviation in logic</li> -<li class="user-break"><span class="kernel">[Logic]</span>  Support for <tt>"reads \nothing"</tt></li> -<li class="user"><span class="kernel">[Logic]</span>  Adding <tt>"\pi"</tt> as built-in symbol</li> -</ul> -<h4>Bug Fixes</h4> -<ul class="entries"> -<li class="bugfix"><span class="kernel">[Cil]</span>  Bug fixed with incompatible declarations of C functions</li> -<li class="bugfix"><span class="kernel">[Cil]</span>  Fix crash in parser when double definition of variable in two different files, in some order (fixed bug <a class="public" href="http://bts.frama-c.com/view.php?id=213">#213</a>)</li> -<li class="bugfix"><span class="kernel">[Configure]</span>  Fixed bug with <tt>-help</tt>.</li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  <tt>-kernel-debug</tt> and <tt>-kernel-verbose</tt> did not work as expected (bts <a class="private" href="http://bts.frama-c.com/view.php?id=343">#343</a>).</li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  <tt>-load-script</tt> did not clean up compiled files after exiting (fixed bug <a class="private" href="http://bts.frama-c.com/view.php?id=371">#371</a>)</li> -<li class="bug-break"><span class="kernel">[Logic]</span>  Support for abrupt clauses; Modifies AST</li> -<li class="bugfix"><span class="kernel">[Logic]</span>  Fixed bug <a class="public" href="http://bts.frama-c.com/view.php?id=272">#272</a> (complete behaviors wo name)</li> -<li class="bugfix"><span class="kernel">[Logic]</span>  Fixed bug <a class="public" href="http://bts.frama-c.com/view.php?id=228">#228</a>, <a class="public" href="http://bts.frama-c.com/view.php?id=327">#327</a> (syntax garbage at end of contracts)</li> -<li class="bugfix"><span class="kernel">[Logic]</span>  More utf-8 identifier accepted (fixes bug <a class="public" href="http://bts.frama-c.com/view.php?id=366">#366</a>)</li> -<li class="bugfix"><span class="kernel">[Logic]</span>  Default label is <tt>"Old"</tt> inside <tt>\old</tt>(...)</li> -<li class="bugfix"><span class="kernel">[Logic]</span>  <tt>complete/disjoint</tt> behaviors do not accept undefined behaviors anymore (fixed bug <a class="public" href="http://bts.frama-c.com/view.php?id=364">#364</a>)</li> -<li class="bug-break"><span class="kernel">[Logic]</span>  Full support for <tt>\let</tt> (fixed bug <a class="private" href="http://bts.frama-c.com/view.php?id=344">#344</a>)</li> -<li class="bug-break"><span class="kernel">[Logic]</span>  Arrays and pointers are distinct in the logic, as per ACSL reference. Fixes bug <a class="public" href="http://bts.frama-c.com/view.php?id=396">#396</a></li> -<li class="bugfix"><span class="kernel">[Makefile]</span>  Fixed bug <a class="public" href="http://bts.frama-c.com/view.php?id=305">#305</a>: make did not terminate when all plug-ins were disabled.</li> -<li class="bugfix"><span class="kernel">[Makefile]</span>  Fixed bug <a class="public" href="http://bts.frama-c.com/view.php?id=310">#310</a>: improve robustness against new ocaml warnings.</li> -<li class="bugfix"><span class="kernel">[Makefile]</span>  Some GUI library files was not installed</li> -<li class="bugfix"><span class="kernel">[Makefile]</span>  Fixed 'make clean' in plug-in directory (bug <a class="private" href="http://bts.frama-c.com/view.php?id=407">#407</a>)</li> -<li class="bugfix"><span class="kernel">[Makefile]</span>  Fix bug for generating .o files through recursive calls to Make in quiet mode (VERBOSEMAKE unset)</li> -</ul> -<h4>Developers Only</h4> -<ul class="entries"> -<li class="dev-break"><span class="kernel">[Cil]</span>  pAssigns now prints directly a whole list of assigns</li> -<li class="dev"><span class="kernel">[Cil]</span>  New hook after Cabs elaboration (fix bug <a class="private" href="http://bts.frama-c.com/view.php?id=446">#446</a>)</li> -<li class="dev"><span class="kernel">[Configure]</span>  Improved dependencies handling (fix <a class="private" href="http://bts.frama-c.com/view.php?id=54">#54</a>)</li> -<li class="dev"><span class="kernel">[Kernel]</span>  Add unique id for elements in <tt>Db.Properties.Status</tt> tables.</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  Function <tt>Db.Properties.predicate_on_stmt</tt> and <tt>Db.Properties.get_user_assert</tt> does not exist anymore.</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  Module <tt>Db.Properties.Status</tt> replaced by module Properties_status.</li> -<li class="dev"><span class="kernel">[Kernel]</span>  Extlib now contains various functions to replace <tt>Sys.command</tt> but with portability and efficiency in mind.</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  Use of global logic constants is now a TLval (TVar _,TNoOffset) instead of TApp(_,[])</li> -<li class="dev"><span class="kernel">[Kernel]</span>  Support for dynamic uses of StringSet parameters</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  New implementation of <tt>save/load</tt> with small changes in the project API. Loading is now rid of its previous allocation peak and faster.</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  <tt>Type.register</tt> is more robust but gets a modified interface (fixed issue <a class="private" href="http://bts.frama-c.com/view.php?id=276">#276</a>)</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  Major changes in API of module Annotations: add possible dependencies <tt>from/to</tt> a single annotation of a statement</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  <tt>Log.protect</tt> is replaced by <tt>Cmdline.protect</tt></li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  <tt>Kernel_function.Set</tt> now implemented with Patricia.</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  Type changes in <tt>Db.Properties.Interp</tt>. Use <tt>~result</tt>:None to get your plug-in to compile again.</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  <tt>Dynamic.register</tt> and <tt>Dynamic.get</tt> are more robust, but take an extra parameter</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  Slight modification of Hook API</li> -<li class="dev-break"><span class="kernel">[Project]</span>  <tt>Project.register_todo_on_clear</tt> is deprecated and replaced by <tt>Project.register_todo_before_clear</tt></li> -</ul> -<h2>Frama-C GUI</h2> -<h4>New Features</h4> -<ul class="entries"> -<li class="user"><span class="kernel">[Gui]</span>  Assigns clauses are now localizable in GUI</li> -<li class="user-break"><span class="kernel">[Gui]</span>  Extend type <tt>Pretty_source.localizable</tt></li> -<li class="user"><span class="kernel">[Gui]</span>  Options *<tt>-verbose</tt>, *<tt>-debug</tt> and <tt>-quiet</tt> are now settable via the launcher dialog box (bts <a class="private" href="http://bts.frama-c.com/view.php?id=317">#317</a>).</li> -<li class="user"><span class="kernel">[Gui]</span>  New shortcut buttons.</li> -<li class="user"><span class="kernel">[Gui]</span>  Now possible to delete the current project.</li> -<li class="user-break"><span class="kernel">[Gui]</span>  Drop gtksourceview <tt>1.x</tt> dependency and replace it with gtksourceview <tt>2.x</tt>.</li> -<li class="user"><span class="kernel">[Gui]</span>  View property status in GUI. Fixed a bug on reset with strange reactive zones in default buffer.</li> -<li class="user"><span class="kernel">[Gui]</span>  Now possible to <tt>save/load</tt> a single project (fixed issue <a class="private" href="http://bts.frama-c.com/view.php?id=9">#9</a>)</li> -<li class="user"><span class="kernel">[Gui]</span>  Plug-in panels can be detached with drag and drop.</li> -<li class="user"><span class="kernel">[Gui]</span>  New menu entries for loading ocaml scripts and ocaml object files (fixed issue <a class="private" href="http://bts.frama-c.com/view.php?id=318">#318</a>)</li> -<li class="user"><span class="kernel">[Gui]</span>  Add a menu entry for setting C source files of the current project</li> -</ul> -<h4>Bug Fixes</h4> -<ul class="entries"> -<li class="bugfix"><span class="kernel">[Gui]</span>  Instantaneous actions are no longer cancelable but are as fast as possible now.</li> -<li class="bugfix"><span class="kernel">[Gui]</span>  Fixed bug while choosing 'New project' if <tt>-cpp-command</tt> is set (fixed bug <a class="public" href="http://bts.frama-c.com/view.php?id=374">#374</a>)</li> -</ul> -<h4>Developers Only</h4> -<ul class="entries"> -<li class="dev-break"><span class="kernel">[Gui]</span>  Methods protect and full_protect of main_window_extension_points now have an additional arguments.</li> -<li class="dev-break"><span class="kernel">[Gui]</span>  New implementation for the menubar and the toolbar. API fully changed for adding an item in these bars.</li> -</ul> -<h2>Plugin Impact</h2> -<ul class="entries"> -<li class="user"> In the GUI filetree, for each function, a bullet shows if some statements are highlighted</li> -</ul> -<h2>Plugin Inout</h2> -<ul class="entries"> -<li class="user-break"> <tt>-out</tt> and <tt>-out-external</tt> now obey <tt>-inout-verbose</tt> option Generated logs re-ordered a little.</li> -</ul> -<h2>Plugin Security</h2> -<ul class="entries"> -<li class="user-break"> No more distributed.</li> -</ul> -<h2>Plugin Security_slicing</h2> -<ul class="entries"> -<li class="user"> New experimental and quite undocumented plug-in. Sub-part of the old plug-in security. Only usable through the GUI.</li> -</ul> -<h2>Plugin Slicing</h2> -<ul class="entries"> -<li class="user"> Assigns clauses was missing from the sliced program (fixed bug <a class="public" href="http://bts.frama-c.com/view.php?id=393">#393</a>)</li> -</ul> -<h2>Plugin Syntactic_callgraph</h2> -<ul class="entries"> -<li class="user"> Big speedup for showing the callgraph in the GUI. Require ocamlgraph >= <tt>1.4</tt>.</li> -<li class="bugfix"> Fixed bug in services computation.</li> -</ul> -<h2>Plugin Value</h2> -<h4>New Features</h4> -<ul class="entries"> -<li class="user"> Improved treatment of <tt>"assigns p[..]"</tt> clauses in <tt>-input</tt><br/><br/></li> -<li class="user"> Handling of behavior-specific assertions now correct (albeit imprecise).</li> -<li class="user"> New option <tt>-all-rounding-modes</tt> (floating-point) New dependency on C99 functions to control the FPU.</li> -<li class="user"> Improved precision of floating-point operations</li> -<li class="user"> Take into account all known flush-to-zero floating-point variants. No option seems necessary for now.</li> -<li class="user"> Preliminary support of post-conditions for library functions.</li> -<li class="user"> New display option <tt>-float-relative</tt></li> -<li class="user-break"> Clarified progress messages</li> -<li class="user"> Improved precision when loop index has type char or short. Fixes bug <a class="public" href="http://bts.frama-c.com/view.php?id=325">#325</a></li> -<li class="user"> Interpreting post-conditions about <tt>\result</tt> in contracts for functions that have implementations.</li> -<li class="user"> New option <tt>-slevel-function</tt> f:n for fine-tuning semantic unrolling.</li> -<li class="user"> Suppressed undocumented option <tt>-klr</tt></li> -<li class="user"> New options <tt>-no-results</tt> and <tt>-no-results-function</tt>, improved replacements for undocumented option <tt>-klr</tt></li> -<li class="user"> Experimental new option <tt>-subdivide-float-var</tt></li> -<li class="user"> Experimental new option <tt>-val-signed-overflow-alarms</tt></li> -</ul> -<h4>Bug Fixes</h4> -<ul class="entries"> -<li class="bugfix"> Synthetic validity status for assertions.</li> -<li class="bugfix"> Some <tt>"loss of precision"</tt> messages were duplicated and failed to be localized. Fixed.</li> -<li class="bugfix"> Fixed bug <a class="public" href="http://bts.frama-c.com/view.php?id=372">#372</a></li> -<li class="bugfix"> Fixed uncaught exception that could happen in analysis of programs with floating-point operations.</li> -</ul> -<h4>Developers Only</h4> -<ul class="entries"> -<li class="dev-break"> Changed type of functions <tt>Db.Value</tt>.*_to_kernel_function. These functions now return a <tt>Kernel_function.Set.t</tt>. Use <tt>Kernel_function.Set.elements</tt> to transform this set into a list.</li> -</ul> -</div> -<hr><div><a id="Beryllium-4.2" href="#Beryllium-4.2"></a></div><h3 class="release">Beryllium Release <span class="hversion">[4.2]</span></h3> - -<div class="release"> -<h2>Frama-C General</h2> -<h4>New Features</h4> -<ul class="entries"> -<li class="user"><span class="kernel">[Configure]</span>  Detection of dot if required.</li> -<li class="user"><span class="kernel">[Journal]</span>  Better handling of exceptions.</li> -<li class="user"><span class="kernel">[Kernel]</span>  Slightly less false alarms with <tt>-warn-unspecified-order</tt></li> -<li class="user"><span class="kernel">[Makefile]</span>  Why is no longer a compilation dependency. It is required only at runtime for the experimental WP plugin.</li> -<li class="user"><span class="kernel">[Makefile]</span>  Now possible to build custom binaries for plug-ins. Roughly these binaries are frama-c[.byte] + the plug-in statically-linked. The goal is called <tt>"static"</tt> in the plug-in's makefile.</li> -</ul> -<h4>Bug Fixes</h4> -<ul class="entries"> -<li class="bugfix"><span class="kernel">[Makefile]</span>  Fixed compilation error occurring on a platform which does not support native dynlink and with ocaml >= <tt>3.11</tt> (bts <a class="public" href="http://bts.frama-c.com/view.php?id=224">#224</a>).<br/><br/></li> -<li class="bugfix"><span class="kernel">[Makefile]</span>  Frama-C compiles even if ocamlopt is not available.</li> -<li class="bug-break"><span class="kernel">[Makefile]</span>  Fixed bug <a class="public" href="http://bts.frama-c.com/view.php?id=236">#236</a>. Require ocamlgraph version > <tt>1.2</tt>.</li> -<li class="bugfix"><span class="kernel">[Project]</span>  Fixed bug involving loading and options previously set while saving.</li> -</ul> -<h4>Developers Only</h4> -<ul class="entries"> -<li class="dev"><span class="kernel">[Cil]</span>  Deprecated <tt>Cil.get_status</tt>. Use <tt>Db.Properties.Status</tt>.* instead.</li> -<li class="dev"><span class="kernel">[Cil]</span>  New pIdentifiedPredicate method in pretty-printer</li> -<li class="dev"><span class="kernel">[Makefile]</span>  Fixed bugs with the use of PLUGIN_EXTRA_BYTE and PLUGIN_EXTRA_OPT by plug-ins.</li> -</ul> -<h2>Frama-C GUI</h2> -<ul class="entries"> -<li class="bugfix"><span class="kernel">[Gui]</span>  Elimination of repeated messages (bts <a class="public" href="http://bts.frama-c.com/view.php?id=237">#237</a>).</li> -<li class="bugfix"><span class="kernel">[Gui]</span>  Release the terminal when the splash window is deleted.</li> -</ul> -<h2>Plugin Jessie</h2> -<ul class="entries"> -<li class="user"> Is no longer built within Frama-C. It becomes part of Why.</li> -</ul> -<h2>Plugin Obfuscator</h2> -<ul class="entries"> -<li class="bugfix"> obfuscator does not lose links between logic and C variables anymore (bts <a class="public" href="http://bts.frama-c.com/view.php?id=250">#250</a>). Obfuscator now gives a specific name to formal parameters.</li> -</ul> -<h2>Plugin Syntactic</h2> -<ul class="entries"> -<li class="user-break"> callgraph Improvement of the GUI of syntactic callgraph. Require ocamlgraph > <tt>1.2</tt>.</li> -</ul> -<h2>Plugin Syntactic_callgraph</h2> -<ul class="entries"> -<li class="user"> Better implementation for computing the service graph: faster + correctly handle cycles.</li> -<li class="user-break"> <tt>-cg-services-only</tt> is not relevant anymore.</li> -</ul> -<h2>Plugin Value</h2> -<ul class="entries"> -<li class="user-break"> Computed values not displayed on <tt>-load</tt>. Use <tt>-val-load</tt> to force display of computed values. Use <tt>-val</tt> <tt>-quiet</tt> to compute without printing results.</li> -<li class="user"> Stopped displaying temporary variables introduced by normalization of source code, and block-local variables.</li> -<li class="bugfix"> Fixed display bug when logging the call stack introduced in Beryllium.</li> -<li class="user"> Improved treatment of <tt>"assigns p[..]"</tt> clauses in value analysis. Other plug-ins (outputs,...) have not had the same improvement yet.</li> -</ul> -</div> -<hr><div><a id="Beryllium-4.1" href="#Beryllium-4.1"></a></div><h3 class="release">Beryllium Release <span class="hversion">[4.1]</span></h3> - -<div class="release"> -<h2>Frama-C General</h2> -<h4>New Features</h4> -<ul class="entries"> -<li class="user"><span class="kernel">[Kernel]</span>  New options <tt>-kernel-help</tt>, <tt>-kernel-verbose</tt> and <tt>-kernel-debug</tt> (bts <a class="private" href="http://bts.frama-c.com/view.php?id=205">#205</a>).</li> -<li class="user"><span class="kernel">[Logic]</span>  <tt>"reads"</tt> clauses on logic functions and predicates, which disappeared with the introduction of axiomatic blocks, have been resurected. Beware that the semantics is slightly different from before: see ACSL document for details. It is used to automatically generate footprint axioms.</li> -</ul> -<h4>Bug Fixes</h4> -<ul class="entries"> -<li class="bugfix"><span class="kernel">[Configure]</span>  Fixed bug with <tt>--disable-gui</tt> in <tt>configure.in</tt><br/><br/></li> -<li class="bugfix"><span class="kernel">[Journal]</span>  Fix generation of invalid variable name in journal</li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Restore compatibility with ocaml <tt>3.10</tt>.2</li> -<li class="bugfix"><span class="kernel">[Makefile]</span>  Fixed bug with static linking of plug-ins using external libraries (bts <a class="public" href="http://bts.frama-c.com/view.php?id=200">#200</a>)</li> -<li class="bugfix"><span class="kernel">[Project]</span>  Fixed bug with <tt>save/load</tt> in multi-project contexts (bts <a class="private" href="http://bts.frama-c.com/view.php?id=161">#161</a>)</li> -<li class="bugfix"><span class="kernel">[Project]</span>  Fixed bug causing delays with <tt>-load</tt> (bts <a class="public" href="http://bts.frama-c.com/view.php?id=180">#180</a>)</li> -</ul> -<h4>Developers Only</h4> -<ul class="entries"> -<li class="dev-break"><span class="kernel">[Cil]</span>  Added 2 components to <tt>Cil_types.typ</tt> to optimize bitsSizeOf. The proper way to get a default value is <tt>Cil.empty_size_cache</tt>. The added value must not be shared by types. No one should need to read this value directly.</li> -<li class="dev-break"><span class="kernel">[Project]</span>  Preliminary support for direct unmarshalling. Datatypes must define value descr. Using <tt>Unmarshal.Direct</tt> is okay for now.</li> -</ul> -<h2>Frama-C GUI</h2> -<ul class="entries"> -<li class="user"><span class="kernel">[Gui]</span>  Graphical customization now uses Gtk rc files. A default file is loaded from <tt>FRAMAC_SHARE/frama-c.rc</tt>. The end user can provide its custom <tt>FRAMAC_SHARE/frama-c-user.rc</tt> to override defaults.</li> -<li class="user"><span class="kernel">[Gui]</span>  Redesign the dialog box for running analysis</li> -<li class="user"><span class="kernel">[Gui]</span>  New message panel</li> -<li class="user"><span class="kernel">[Gui]</span>  Possible to stop the GUI while computing analysis</li> -<li class="user"><span class="kernel">[Gui]</span>  Improved display of summary information when selecting a file.</li> -</ul> -<h2>Plugin Semantic</h2> -<ul class="entries"> -<li class="bugfix"> Constant Folding Fix bad journalisation</li> -</ul> -<h2>Plugin Syntactic_callgraph</h2> -<ul class="entries"> -<li class="user-break"> New design of the callgraph in the GUI. Frama-C now requires ocamlgraph <tt>1.2</tt>.</li> -<li class="user"> New option <tt>-cg-services-only</tt> to only computes the graph of services</li> -</ul> -<h2>Plugin Value</h2> -<ul class="entries"> -<li class="user"> Improved treatment of conditions involving char or short variables.</li> -<li class="user"> Improved integer division. Now returns best effort results when 0 is among the possible values for the divisor.</li> -</ul> -</div> -<hr><div><a id="Beryllium-4.0" href="#Beryllium-4.0"></a></div><h3 class="release">Beryllium Release <span class="hversion">[4.0]</span></h3> - -<div class="release"> -<h2>Frama-C General</h2> -<h4>New Features</h4> -<ul class="entries"> -<li class="user"><span class="kernel">[Configure]</span>  For each dynamic plug-in P, a new option <tt>--with-P-static</tt> is added to <tt>configure.in</tt> for linking P statically with Frama-C.</li> -<li class="user"><span class="kernel">[Configure]</span>  New option <tt>-with-all-static</tt> in order to statically link all plug-ins, except those explicitly specified as dynamic (bts <tt>'430'</tt>).</li> -<li class="user"><span class="kernel">[Configure]</span>  better message when a plug-in isn't enable by default.</li> -<li class="user"><span class="kernel">[Configure]</span>  Auto-detection of lablgtk2's custom tree model.</li> -<li class="user"><span class="kernel">[Journal]</span>  Journalisation of plug-ins slicing, sparecode, impact and security done.</li> -<li class="user"><span class="kernel">[Journal]</span>  Journalisation of functions with labels is now possible (bts <tt>'427'</tt>).</li> -<li class="user"><span class="kernel">[Journal]</span>  Operations on projects (bts <tt>'436'</tt>) and code outputs are journalised.</li> -<li class="user-break"><span class="kernel">[Journal]</span>  Option <tt>-journal-loader-run</tt> does not exist anymore. Use <tt>-load-module</tt> instead.</li> -<li class="user"><span class="kernel">[Journal]</span>  Journal disabled by default in batch mode</li> -<li class="user-break"><span class="kernel">[Kernel]</span>  New implementation of command line parsing</li> -<li class="user"><span class="kernel">[Kernel]</span>  Syntax <tt>"-option-name=value"</tt> is now valid on the command line. In such a case, [value] may begin by '-', which is forbidden for the usual syntax <tt>"-option-name value"</tt>.</li> -<li class="user"><span class="kernel">[Kernel]</span>  Better message for errors on the command line.</li> -<li class="user"><span class="kernel">[Kernel]</span>  New alias <tt>"-h"</tt> and <tt>"--help"</tt> for <tt>"-help"</tt> (bug <a class="public" href="http://bts.frama-c.com/view.php?id=61">#61</a>).</li> -<li class="user"><span class="kernel">[Kernel]</span>  Each boolean option now has an opposite.</li> -<li class="user"><span class="kernel">[Kernel]</span>  New option <tt>-load-script</tt> to dynamically compile and load an ocaml script.</li> -<li class="user"><span class="kernel">[Kernel]</span>  When loading a module via <tt>-load-module</tt>, the dynamically registered options are now recognized on the command line.</li> -<li class="user"><span class="kernel">[Kernel]</span>  New environment variable FRAMAC_LIB</li> -<li class="user"><span class="kernel">[Kernel]</span>  New options <tt>-no-type</tt> and <tt>-no-obj</tt></li> -<li class="user"><span class="kernel">[Kernel]</span>  By default, Frama-C stops on annotation errors. Option <tt>-continue-annotation-error</tt></li> -<li class="user-break"><span class="kernel">[Kernel]</span>  FRAMAC_DYN_PATH is now called FRAMAC_PLUGIN</li> -<li class="user"><span class="kernel">[Logic]</span>  Support for concrete type definition.</li> -<li class="user"><span class="kernel">[Logic]</span>  Overloaded logic symbols.</li> -</ul> -<h4>Bug Fixes</h4> -<ul class="entries"> -<li class="bugfix"><span class="kernel">[Cil]</span>  Fixed parsing of global initializers like <tt>"(3>0)?0:1"</tt> when <tt>Cil.lowerConstants</tt> is false.</li> -<li class="bugfix"><span class="kernel">[Cil]</span>  Fixed some localization problems with frontc visitor.</li> -<li class="bugfix"><span class="kernel">[Cil]</span>  Keep track of variables that have block scope (bts <tt>'218'</tt>) uninitialize them at the exit of corresponding block.</li> -<li class="bugfix"><span class="kernel">[Configure]</span>  Fixed bug with <tt>--disable-</tt>* options (except when '*' was a plug-in name).</li> -<li class="bugfix"><span class="kernel">[Configure]</span>  Fixed issues in configure and makefile if lablgtk2 is not enabled.</li> -<li class="bugfix"><span class="kernel">[Journal]</span>  Fixed bug in journalisation of non-functional values.</li> -<li class="bugfix"><span class="kernel">[Journal]</span>  Fixed bug with <tt>-disable-journal</tt> and type with no pretty-printer.</li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Frama-C has now a very early initialisation step. That's fixed minor issues with <tt>-journal-disable</tt> (bts <a class="private" href="http://bts.frama-c.com/view.php?id=14">#14</a> and <a class="private" href="http://bts.frama-c.com/view.php?id=16">#16</a>).</li> -<li class="bugfix"><span class="kernel">[Logic]</span>  Fixed bug in type-checking of polymorphic functions.</li> -<li class="bugfix"><span class="kernel">[Logic]</span>  Allow \ as first letter of identifier.</li> -<li class="bugfix"><span class="kernel">[Logic]</span>  Changed <tt>\result_finite_float</tt> into <tt>\is_finite_float</tt>. Alarm generation is still untyped.</li> -<li class="bugfix"><span class="kernel">[Logic]</span>  Fixed predicate typing of <tt>\pointer_comparable</tt>.</li> -<li class="bugfix"><span class="kernel">[Logic]</span>  Fixed bugs in type unification.</li> -<li class="bugfix"><span class="kernel">[Makefile]</span>  Fixed bug in compilation of dynamic plug-ins with a GUI.</li> -<li class="bugfix"><span class="kernel">[Makefile]</span>  Fixed bug whenever all plug-ins should be static.</li> -<li class="bugfix"><span class="kernel">[Project]</span>  Fixed bug <a class="private" href="http://bts.frama-c.com/view.php?id=113">#113</a>: loading a session containing a project p referring to another project generated a new incorrect project p.</li> -</ul> -<h4>Developers Only</h4> -<ul class="entries"> -<li class="dev-break"><span class="kernel">[Cil]</span>  C expressions now have a unique ID. See frama-c-commits for details.</li> -<li class="dev"><span class="kernel">[Configure]</span>  No longer require to modify the end of <tt>configure.in</tt> when you add a new plug-in.</li> -<li class="dev"><span class="kernel">[Configure]</span>  Explicitly require >= OCaml <tt>3.10</tt>.0</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  Some changes in API of module Type (bts <tt>'410'</tt>). In particular:<br/><i>1</i>.  module FunTbl no longer exist. Replaced by <tt>Type.Tbl</tt><br/><i>2</i>.  Merge of pretty printer registration with type registration. No more in module Journal. Only in module Type.</li> -<li class="dev"><span class="kernel">[Kernel]</span>  Dynamic plug-ins can now register their own types (abstract from the outside) and operations on such types (bts <tt>'413'</tt>).</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  <tt>File.pretty</tt> does not take anymore a formatter as argument. The default output is the one specified by option <tt>-ocode</tt>.</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  Type of <tt>Db.register</tt> changed in order to be able to say that a function call must never be written in the journal.</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  Dynamic plug-ins have to take care about journalisation.</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  Cil_state is now called Ast and <tt>Cil_state.file</tt> is now called <tt>Ast.get</tt>.</li> -<li class="dev"><span class="kernel">[Kernel]</span>  Possibility to define alias for options.</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  Moved lightweight annotation support from Jessie to Kernel. They are now available for all plugins. Support for lightweight global invariants on globals has been dropped.</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  <tt>Db.Main.extend</tt> is now of type unit -> unit</li> -<li class="dev-break"><span class="kernel">[Logic]</span>  Merge terms and tsets in the AST.</li> -<li class="dev-break"><span class="kernel">[Logic]</span>  Tresult has a type attached to it</li> -<li class="dev"><span class="kernel">[Makefile]</span>  New implementation of (un)verbose mode (bts <tt>'442'</tt>).</li> -<li class="dev"><span class="kernel">[Makefile]</span>  Fixed <tt>"dist"</tt> and <tt>"bdist"</tt> targets that had been broken on <tt>02/27</tt>.</li> -<li class="dev"><span class="kernel">[Makefile]</span>  Independent Makefile for dynamic plug-ins.</li> -<li class="dev-break"><span class="kernel">[Project]</span>  Remove functions <tt>Project.save</tt> and <tt>Project.load</tt>: cannot ensure their correctness.</li> -</ul> -<h2>Frama-C GUI</h2> -<h4>New Features</h4> -<ul class="entries"> -<li class="user"><span class="kernel">[Gui]</span>  Add 2 separate pages for stdout and stderr redirections .</li> -<li class="user-break"><span class="kernel">[Gui]</span>  Code annotation and all globals are now reactive to selections (bts <tt>'359'</tt> and <tt>'387'</tt>).</li> -<li class="user"><span class="kernel">[Gui]</span>  Environment variables FRAMAC_MONOSPACEFONT and FRAMAC_GENERALFONT.</li> -<li class="user"><span class="kernel">[Gui]</span>  Change the warning to panel to preserve decent performance. This imposes lablgtk <tt>2.12</tt> at least.</li> -</ul> -<h4>Bug Fixes</h4> -<ul class="entries"> -<li class="bugfix"><span class="kernel">[Gui]</span>  Fix a bug with broken UTF-8 output on stdout (bts <tt>'420'</tt>).</li> -<li class="bugfix"><span class="kernel">[Gui]</span>  Reentrancy fix with left panels.</li> -<li class="bugfix"><span class="kernel">[Gui]</span>  Fixed bug with some utf8 strings.</li> -<li class="bugfix"><span class="kernel">[Gui]</span>  Changes having to do with dependencies between computations. Hopefully less problems exist now than before.</li> -</ul> -<h4>Developers Only</h4> -<ul class="entries"> -<li class="dev"><span class="kernel">[Gui]</span>  Add function <tt>Design.main_window_extension_points</tt>#help_message.</li> -<li class="dev"><span class="kernel">[Gui]</span>  The plug-in GUI is now packed with the core plug-in</li> -</ul> -<h2>Plugin Aorai</h2> -<ul class="entries"> -<li class="user"> Aorai is now a dynamic plug-in.</li> -</ul> -<h2>Plugin From</h2> -<ul class="entries"> -<li class="bugfix"> Improved dependencies + bug fixes</li> -</ul> -<h2>Plugin Impact</h2> -<h4>New Features</h4> -<ul class="entries"> -<li class="user"> Slicing after impact is now possible (bts <tt>'301'</tt>).</li> -<li class="user-break"> Do not select anymore the selected statements except if they are effectively impacted themselves (bts <tt>'411'</tt>).</li> -<li class="user"> In the GUI, highlight the selected statement in cyan.</li> -</ul> -<h4>Bug Fixes</h4> -<ul class="entries"> -<li class="bugfix"> Bug fixed in the GUI (on project switching).</li> -<li class="bugfix"> In the GUI, fixed bug while the analysis raised an exception. It is now properly caught and displayed on stderr.</li> -</ul> -<h2>Plugin InOut</h2> -<ul class="entries"> -<li class="user"> Add <tt>-out-external</tt> option.</li> -</ul> -<h2>Plugin Inout</h2> -<ul class="entries"> -<li class="user-break"> <tt>-input_with_formals</tt> is now called <tt>-input-with-formals</tt></li> -</ul> -<h2>Plugin Jessie</h2> -<h4>New Features</h4> -<ul class="entries"> -<li class="user"> Jessie is now a dynamic plug-in (bts <tt>'419'</tt>).</li> -<li class="user-break"> GUI mode is now the default, options <tt>-jessie-gui</tt> and <tt>-jessie-goals</tt> do not exists anymore</li> -<li class="user-break"> Option for launching jessie is now <tt>-jessie</tt>, not <tt>-jessie-analysis</tt></li> -</ul> -<h4>Bug Fixes</h4> -<ul class="entries"> -<li class="bugfix"> Support constant sizeof and alignof in logic terms (bts <tt>'396'</tt>).</li> -<li class="bugfix"> proper message when <tt>\lambda</tt> is encountered (bts <tt>'7528'</tt>).</li> -<li class="bugfix"> fixed bugs <a class="private" href="http://bts.frama-c.com/view.php?id=63">#63</a> and <a class="public" href="http://bts.frama-c.com/view.php?id=71">#71</a> (labels and <tt>\at</tt>)</li> -<li class="bugfix"> Fix bug <a class="private" href="http://bts.frama-c.com/view.php?id=8">#8</a>, compilation of jessie with Apron</li> -<li class="bugfix"> Support for loop assigns, partially fixes bug <a class="public" href="http://bts.frama-c.com/view.php?id=41">#41</a> see <tt>tests/jessie/bts0041-bis.c</tt> for details</li> -<li class="bugfix"> Full support for loop assigns, including those implicitly generated from function's assigns, fixes bug <a class="public" href="http://bts.frama-c.com/view.php?id=41">#41</a></li> -<li class="bugfix"> Support for label Post in assigns clauses. Fixes bug <a class="public" href="http://bts.frama-c.com/view.php?id=160">#160</a></li> -<li class="bugfix"> Fixed contract for strchr() and strrchr() in <tt>string.h</tt></li> -</ul> -<h2>Plugin Pdg</h2> -<ul class="entries"> -<li class="dev"> The functions that return nodes from an annotations now also return a list of the variables declarations nodes.</li> -</ul> -<h2>Plugin Semantic_callgraph</h2> -<ul class="entries"> -<li class="user"> small change in the computation of services: the roots are now the same as the syntactic callgraph (while there is no function pointer).</li> -<li class="user-break"> new options <tt>-scg-dump</tt> and <tt>-scg-init-func</tt> consistent with the options <tt>-cg-dump</tt> and <tt>-cg-init-func</tt> of the syntactic callgraph.</li> -</ul> -<h2>Plugin Slicing</h2> -<ul class="entries"> -<li class="user"> New option <tt>"-slicing-keep-annotations"</tt></li> -</ul> -<h2>Plugin Sparecode</h2> -<ul class="entries"> -<li class="bugfix"> Selected an annotation attached to a function call made a wrong propagation in the visibility of the call (bts <a class="private" href="http://bts.frama-c.com/view.php?id=3">#3</a>).</li> -<li class="bugfix"> The generated project lost some useful parameters like the entry point (bts <a class="private" href="http://bts.frama-c.com/view.php?id=10">#10</a>).</li> -</ul> -<h2>Plugin Syntactic_callgraph</h2> -<ul class="entries"> -<li class="bugfix"> Fixed bug when the callgraph is computed twice</li> -<li class="user"> Separate services are now created for callees of the entry point.</li> -</ul> -<h2>Plugin Users</h2> -<ul class="entries"> -<li class="dev"> Users are now computed on need while calling <tt>!Db.Users.get</tt></li> -</ul> -<h2>Plugin Value</h2> -<h4>New Features</h4> -<ul class="entries"> -<li class="user"> Improved support for state reduction on a memory read.<br/><br/></li> -<li class="user"> Minor changes in floating-point handling.</li> -<li class="user"> Adjustments in the appearance of some alarms</li> -<li class="user"> Improved results for char ones[] = <tt>"11111111"</tt>; col_ones = 1 + * (int*) ones;</li> -<li class="user"> Trivially redundant alarms are now automatically discharged.</li> -<li class="user"> Improved reduction for (ptr-ptr) expressions.</li> -</ul> -<h4>Bug Fixes</h4> -<ul class="entries"> -<li class="bugfix"> Miscellaneous fixes and tuning.</li> -<li class="bugfix"> Fixed correctness bug that had a tiny chance to manifest itself when analyzing code that dereferences casted pointers.</li> -<li class="bugfix"> Fixed performance bug.</li> -<li class="bugfix"> Fixed bug that could appear with assignments like t[5] = t[4]; where t[4] is not a singleton.</li> -<li class="bugfix"> Fixed bug with the interpretation of <tt>"==>"</tt>.</li> -</ul> -<h4>Developers Only</h4> -<ul class="entries"> -<li class="dev"> New constructor Signed_overflow_alarm for type <tt>Alarms.t</tt></li> -</ul> -</div> -<hr><div><a id="Lithium-3.1" href="#Lithium-3.1"></a></div><h3 class="release">Lithium Release <span class="hversion">[3.1]</span></h3> - -<div class="release"> -<h2>Frama-C General</h2> -<h4>New Features</h4> -<ul class="entries"> -<li class="user-break"><span class="kernel">[Kernel]</span>  Changed the definition of non-determinist functions in <tt>builtin.c</tt>. These functions no longer rely on a volatile variable. Analysis logs may change slightly as a result.</li> -<li class="user"><span class="kernel">[Logic]</span>  Added support for (wide) string constants in ACSL formula.</li> -</ul> -<h4>Developers Only</h4> -<ul class="entries"> -<li class="dev"><span class="kernel">[Cil]</span>  New methods for visiting compinfo, enuminfo, fieldinfo and enumitem (prevents potential misuse of copy visitor for these types).</li> -<li class="dev-break"><span class="kernel">[Cil]</span>  enum items now have their own type and are shared between declaration and use.</li> -<li class="dev"><span class="kernel">[Cil]</span>  New methods current_function and current_kf methods (bts <tt>'406'</tt>).</li> -<li class="dev-break"><span class="kernel">[Cil]</span>  Modified typeForInsertedCast hook to take as arguments the expression and its original type in addition to the destination type.</li> -<li class="dev"><span class="kernel">[Makefile]</span>  Support for native compilation in <tt>Makefile.template</tt> (require ocaml >= <tt>3.11</tt>).<br/><br/></li> -<li class="dev"><span class="kernel">[Makefile]</span>  Fixed various bugs in <tt>Makefile.template</tt>.</li> -</ul> -<h2>Frama-C GUI</h2> -<ul class="entries"> -<li class="user-break"><span class="kernel">[Gui]</span>  Improved consistency of some information messages.</li> -</ul> -<h2>Plugin Impact</h2> -<ul class="entries"> -<li class="user"> In the GUI, new panel to manage impact analysis actions.</li> -</ul> -<h2>Plugin Jessie</h2> -<ul class="entries"> -<li class="bugfix"> Fixed bug with multiple labels in axiomatic definitions.</li> -<li class="user"> Added example <tt>tests/jessie/minimum_sort.c</tt> in Jessie tutorial.</li> -<li class="bugfix"> Fixed problem with array in logical annotations.</li> -<li class="bugfix"> Fixed problem with memory model preventing the proof of some pointer programs. The solution is to require pointers that are compared to belong to the same allocated memory block, which can be expressed in logical annotations using equality of <tt>\base_addr</tt> constructs.</li> -</ul> -<h2>Plugin Slicing</h2> -<ul class="entries"> -<li class="user-break"> Unused global variables and types are now removed in sparecode analysis and slicing results.</li> -</ul> -<h2>Plugin Sparecode</h2> -<ul class="entries"> -<li class="user"> New option <tt>-rm-unused-globals</tt> to remove unused global variables and types.</li> -</ul> -<h2>Plugin Value</h2> -<ul class="entries"> -<li class="user"> Abstract structs are now supported in conjunction with option <tt>-lib-entry</tt>, and invalid to access.</li> -<li class="user-break"> Removed outdated warning about uninitialized const variables.</li> -<li class="user"> Introduced preliminary support for state reductions on a memory read access. This should eliminate some redundant alarms.</li> -</ul> -</div> -<hr><div><a id="Lithium-3.0" href="#Lithium-3.0"></a></div><h3 class="release">Lithium Release <span class="hversion">[3.0]</span></h3> - -<div class="release"> -<h2>Frama-C General</h2> -<h4>New Features</h4> -<ul class="entries"> -<li class="user"><span class="kernel">[Journal]</span>  Journalization available (only Cmdline and Occurrence are done yet).</li> -<li class="user"><span class="kernel">[Journal]</span>  New options available <tt>-load-journal</tt>, <tt>-journal-name</tt>, <tt>-journal-disable</tt> for user management of journals.</li> -<li class="user"><span class="kernel">[Kernel]</span>  Dynamic linking of plugin available (experimental).</li> -<li class="user"><span class="kernel">[Kernel]</span>  Added option <tt>-warn-unspecified-order</tt> to display a warning for each unspecified sequence containing writes.</li> -<li class="user"><span class="kernel">[Logic]</span>  Support for <tt>\separated</tt>.</li> -<li class="user"><span class="kernel">[Logic]</span>  Basic support for sets as first-class value.</li> -<li class="user"><span class="kernel">[Logic]</span>  Support for address-of operator (&) in tsets.</li> -<li class="user"><span class="kernel">[Project]</span>  Projectification of machdep (bts <tt>'101'</tt>).</li> -</ul> -<h4>Bug Fixes</h4> -<ul class="entries"> -<li class="bugfix"><span class="kernel">[Logic]</span>  Fixed bug "0 can be seen as pointer to any type" (bts <tt>'338'</tt>).</li> -<li class="bugfix"><span class="kernel">[Logic]</span>  Fixed typing error of pointer lval hidden by typdefs.</li> -</ul> -<h4>Developers Only</h4> -<ul class="entries"> -<li class="dev-break"><span class="kernel">[Cil]</span>  AST changes for unspecified sequences (experimental).</li> -<li class="dev-break"><span class="kernel">[Kernel]</span>  Refined UnspecifiedSequence information.</li> -<li class="dev"><span class="kernel">[Ptests]</span>  Added config option STDOPT (see developer's manual for details).</li> -</ul> -<h2>Frama-C GUI</h2> -<ul class="entries"> -<li class="user"><span class="kernel">[Gui]</span>  Lower the bound on maximum number of displayed globals to 20 (bts <tt>'342'</tt>).</li> -</ul> -<h2>Plugin Deps</h2> -<ul class="entries"> -<li class="user"> In the GUI, the <tt>"Dependencies"</tt> contextual menu provides the old <tt>"Scope"</tt> and <tt>"Show Def"</tt> features in addition to the new <tt>"Zones"</tt> feature. These three actions can be launch together with the <tt>"All"</tt> button.</li> -</ul> -<h2>Plugin Inout</h2> -<ul class="entries"> -<li class="user"> New option <tt>-input_with_formals</tt>.</li> -</ul> -<h2>Plugin Jessie</h2> -<ul class="entries"> -<li class="bugfix"> Fixed path problems with binary distributions.<br/><br/></li> -</ul> -<h2>Plugin Pdg</h2> -<ul class="entries"> -<li class="bugfix"> Fixed bugs for <tt>CAT/AF</tt> evaluation.</li> -</ul> -<h2>Plugin Semantic_callgraph</h2> -<ul class="entries"> -<li class="user"> New option <tt>-scg-dump</tt> to dump a semantic callgraph to stdout.</li> -</ul> -<h2>Plugin Slicing</h2> -<h4>New Features</h4> -<ul class="entries"> -<li class="user"> In the GUI, request related to <tt>read/write</tt> accesses to lvalues is available from the contextual submenu.</li> -<li class="user"> In the GUI, implemented feature request related to highlighting when the source function is called, for <tt>CAT/AF</tt> evaluation.</li> -<li class="user"> In the GUI, new panel to manage slicing actions.</li> -<li class="user"> In the GUI, slicing request related to values returned by functions is available from the contextual submenu.</li> -</ul> -<h4>Bug Fix</h4> -<ul class="entries"> -<li class="bugfix"> In the GUI, fixed bugs related to <tt>enabling/disabling</tt> conditions of the slicing submenu.</li> -</ul> -<h2>Plugin Value</h2> -<h4>New Features</h4> -<ul class="entries"> -<li class="user"> Added option <tt>-no-unspecified-access</tt> to disable alarm above.</li> -<li class="user-break"> Raise alarm for undefined behavior caused by side-effects in UnspecifiedSequence (except for function calls).</li> -<li class="user-break"> Changed behavior of option <tt>-context-valid-pointers</tt> to make it more like the documentation says it is.</li> -</ul> -<h4>Bug Fixes</h4> -<ul class="entries"> -<li class="bugfix"> Fixed huge bug in the computation of the dependencies of an expression. Differences are most visible in the results of options <tt>-input</tt> and <tt>-deps</tt>, and of course all she slicing options that make use of these.</li> -<li class="bugfix"> Fixed a bug introduced with the "value concatenation" feature where an imprecise value obtained by reading misaligned data would have the origin <tt>"Arithmetic"</tt> instead of <tt>"Misaligned"</tt>.</li> -</ul> -<h4>Developers Only</h4> -<ul class="entries"> -<li class="dev-break"> Removed argument <tt>~skip_base_deps</tt> from all functions in <tt>Db.Value</tt> that had one. This argument did not make sense.</li> -</ul> -</div> -<hr><div><a id="Helium-2.0" href="#Helium-2.0"></a></div><h3 class="release">Helium Release <span class="hversion">[2.0]</span></h3> - -<div class="release"> -<h2>Frama-C General</h2> -<h4>New Features</h4> -<ul class="entries"> -<li class="user"><span class="kernel">[Configure]</span>  <tt>./configure</tt> will not emit so many warning when gui is not available (bts <tt>'296'</tt>).</li> -<li class="user-break"><span class="kernel">[Kernel]</span>  Do not remove unused static functions.</li> -<li class="user-break"><span class="kernel">[Kernel]</span>  Change <tt>-lib-entry</tt> option into a boolean. <tt>"-lib-entry foo"</tt> becomes <tt>"-lib-entry -main foo"</tt></li> -<li class="user-break"><span class="kernel">[Logic]</span>  Support for constant predicates and functions (breaks 0<tt>-argument</tt> old syntax).</li> -<li class="user"><span class="kernel">[Logic]</span>  Better error messages for logic typing errors.</li> -<li class="user"><span class="kernel">[Logic]</span>  Typing of terms: implement ACSL semantics for <tt>integral/real</tt> promotions.</li> -<li class="user"><span class="kernel">[Logic]</span>  Pretty printing of pointer accesses in terms and tsets are now much nicer. For example *(T+(0+i..j)) becomes T[0+i..j].</li> -<li class="user-break"><span class="kernel">[Logic]</span>  Quantification over arrays are interpreted as quantification over pointers to be consistent with predicates and C function calls.</li> -<li class="user-break"><span class="kernel">[Logic]</span>  <tt>\valid</tt>* predicates rejects void pointers.</li> -<li class="user-break"><span class="kernel">[Logic]</span>  Merge predicates and logic functions when linking multiple c files.</li> -<li class="user"><span class="kernel">[Logic]</span>  Enforce correct return type of logic functions.</li> -<li class="user"><span class="kernel">[Logic]</span>  Typing of recursive logic functions.</li> -<li class="user"><span class="kernel">[Makefile]</span>  Prefix install directories by the value of DESTDIR (patch contributed by Igor Galic).</li> -<li class="user"><span class="kernel">[Project]</span>  Loading works even if the configuration while saving is not exactly equal to the one while loading.</li> -</ul> -<h4>Bug Fixes</h4> -<ul class="entries"> -<li class="bugfix"><span class="kernel">[Kernel]</span>  <tt>-machdep</tt> was ignored (bts <tt>'309'</tt>).<br/><br/></li> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Correct promotion rules from bitfields to integers.</li> -<li class="bugfix"><span class="kernel">[Logic]</span>  Correct typing for predicates: no more dangerous promotions.</li> -<li class="bugfix"><span class="kernel">[Makefile]</span>  Fixed bug in <tt>"make distclean"</tt> (bts <tt>'308'</tt>).</li> -</ul> -<h4>Developers Only</h4> -<ul class="entries"> -<li class="dev-break"><span class="kernel">[Logic]</span>  AST changes for invariants.</li> -</ul> -<h2>Frama-C GUI</h2> -<ul class="entries"> -<li class="user-break"><span class="kernel">[Gui]</span>  Enforce lablgtksourceview dependency and suppressed camlp4 need.</li> -<li class="user"><span class="kernel">[Gui]</span>  First rehighlight support.</li> -<li class="user"><span class="kernel">[Gui]</span>  Invalidate display cache on project switching.</li> -<li class="user"><span class="kernel">[Gui]</span>  Improve speed of configuration menu.</li> -</ul> -<h2>Plugin Constfold</h2> -<ul class="entries"> -<li class="user-break"> Semantic constant folding does not introduce casts by default.</li> -<li class="user"> New option <tt>-cast-from-constant</tt> has been added to allows cast introductions.</li> -</ul> -<h2>Plugin Impact</h2> -<ul class="entries"> -<li class="bugfix"> Fixed bug when a function is undefined (bts <tt>'322'</tt>).</li> -</ul> -<h2>Plugin Metrics</h2> -<ul class="entries"> -<li class="user"> Number of syntactic calls by functions and potential entry points.</li> -<li class="user"> New option <tt>-metrics-dump</tt>.</li> -</ul> -<h2>Plugin Occurrence</h2> -<ul class="entries"> -<li class="user"> Occurrences of a variable can be computed from any occurrence of the program (not only from its declaration).</li> -</ul> -<h2>Plugin Pdg</h2> -<ul class="entries"> -<li class="user"> Improvement of the precision of interprocedural analysis (bts <tt>'179'</tt>).</li> -<li class="bugfix"> Fixed bug in interprocedural analysis (bts <tt>'324'</tt>).</li> -</ul> -<h2>Plugin Slicing</h2> -<ul class="entries"> -<li class="user"> In the GUI, slicing contextual submenu available.</li> -<li class="user"> Some slicing requests are available from the GUI.</li> -</ul> -<h2>Plugin Sparecode</h2> -<ul class="entries"> -<li class="user"> New option <tt>-sparecode-no-annot</tt> (bts <tt>'331'</tt> and <tt>'334'</tt>).</li> -</ul> -<h2>Plugin Value</h2> -<ul class="entries"> -<li class="user-break"> Separate warnings for uninitialized and addresses escaping their scopes (these used to be grouped together as <tt>"unspecified"</tt> alarms)</li> -<li class="user-break"> Remove remaining TOP in value analysis: WELL at amx-valid-depth and for leaf functions.</li> -<li class="user"> New implicit context generation with a fixed width of 6 (an option will be available later).</li> -<li class="user"> Some partial builtin_va_start support</li> -<li class="user-break"> Removed last top from merging leaf functions returns.</li> -<li class="user"> New option <tt>-context-width</tt> for auto-allocated context pointer width. Defaults to 2.</li> -<li class="user-break"> Do not emit imprecision tracing warning when a lval=lval is optimized.</li> -</ul> -</div> -<hr><div><a id="Hydrogen-1.3" href="#Hydrogen-1.3"></a></div><h3 class="release">Hydrogen Release <span class="hversion">[1.3]</span></h3> - -<div class="release"> -<h2>Frama-C General</h2> -<ul class="entries"> -<li class="dev"><span class="kernel">[Makefile]</span>  Fixed bug in <tt>"make clean-doc"</tt> (and <tt>"make distclean"</tt>).</li> -</ul> -<h2>Frama-C GUI</h2> -<ul class="entries"> -<li class="user"><span class="kernel">[Gui]</span>  All internal options are available in the GUI preferences pannel.<br/><br/></li> -</ul> -</div> -<hr><div><a id="Hydrogen-1.2" href="#Hydrogen-1.2"></a></div><h3 class="release">Hydrogen Release <span class="hversion">[1.2]</span></h3> - -<div class="release"> -<h2>Frama-C General</h2> -<h4>New Feature</h4> -<ul class="entries"> -<li class="user"><span class="kernel">[Kernel]</span>  Option <tt>-no-unicode</tt> : do not print Unicode chars.<br/><br/></li> -</ul> -<h4>Bug Fixes</h4> -<ul class="entries"> -<li class="bugfix"><span class="kernel">[Kernel]</span>  Various Win32 path fixes.</li> -<li class="bugfix"><span class="kernel">[Project]</span>  Inconsistent data with multiple projects and while removing projects.</li> -<li class="bugfix"><span class="kernel">[Project]</span>  Fixed bug in <tt>save/load</tt> with duplicated computations.</li> -</ul> -<h4>Developers Only</h4> -<ul class="entries"> -<li class="dev"><span class="kernel">[Project]</span>  Warnings are project compliant.</li> -</ul> -<h2>Frama-C GUI</h2> -<h4>New Features</h4> -<ul class="entries"> -<li class="user"><span class="kernel">[Gui]</span>  Large improvements in reactivity</li> -<li class="user"><span class="kernel">[Gui]</span>  No file selection on startup.</li> -<li class="user"><span class="kernel">[Gui]</span>  Persistent position.</li> -<li class="user"><span class="kernel">[Gui]</span>  Buffer memoization for speedup.</li> -<li class="user"><span class="kernel">[Gui]</span>  Progress added in existing plugins.</li> -<li class="user"><span class="kernel">[Gui]</span>  Project names are pairwise different in the GUI.</li> -</ul> -<h4>Bug Fixes</h4> -<ul class="entries"> -<li class="bugfix"><span class="kernel">[Gui]</span>  <tt>Prefs/Execute</tt> bugs fixed.</li> -<li class="bugfix"><span class="kernel">[Gui]</span>  Win32 default fonts fixed.</li> -</ul> -<h4>Developers Only</h4> -<ul class="entries"> -<li class="dev"><span class="kernel">[Gui]</span>  Project management redesigned for older Gtk and for the best.</li> -</ul> -<h2>Plugin Impact</h2> -<ul class="entries"> -<li class="user"> Available from toplevel through <tt>-impact-pragma</tt> and <tt>-impact-print</tt>.</li> -</ul> -<h2>Plugin Scope</h2> -<ul class="entries"> -<li class="user"> First release of the plug-in (bts <tt>'191'</tt>).</li> -</ul> -<h2>Plugin Value</h2> -<ul class="entries"> -<li class="user-break"> Display a warning whenever an uninitialized value causes the death of a branch.</li> -<li class="user"> In the GUI, function level information displayed in Information panel.</li> -</ul> -</div> -<hr><div><a id="Hydrogen-1.1" href="#Hydrogen-1.1"></a></div><h3 class="release">Hydrogen Release <span class="hversion">[1.1]</span></h3> - -<div class="release"> -<h2>Frama-C General</h2> -<ul class="entries"> -<li class="bugfix"><span class="kernel">[Makefile]</span>  Fixed bug with GUI compilation.</li> -<li class="bugfix"><span class="kernel">[Project]</span>  Fixed bug with checksum computation during <tt>save/load</tt>.</li> -</ul> -<h2>Frama-C GUI</h2> -<ul class="entries"> -<li class="bugfix"><span class="kernel">[Gui]</span>  GUI no longer frozen during computations.</li> -<li class="user"><span class="kernel">[Gui]</span>  'New' menu entry.</li> -</ul> -<h2>Plugin Occurrence</h2> -<ul class="entries"> -<li class="user"> New option <tt>-occurrence</tt>.</li> -<li class="user"> First release of the plug-in.</li> -</ul> -<h2>Plugin Slicing</h2> -<ul class="entries"> -<li class="bugfix"> Fixed bug in interprocedural slicing (bts <tt>'201'</tt>).<br/><br/></li> -</ul> -</div> -<hr><div><a id="Hydrogen-1.0" href="#Hydrogen-1.0"></a></div><h3 class="release">Hydrogen Release <span class="hversion">[1.0]</span></h3> - -<div class="release"> -<h2>Plugin First</h2> -<ul class="entries"> -<li class="user"> release<br/><br/></li> -</ul> -</div> diff --git a/generator/generate b/generator/generate index de9376c5fb9be18aeb0b491cf53c181f47e89022..92bf486bf1051dc124ecd7c9d0cb14ea7a83dee2 100755 Binary files a/generator/generate and b/generator/generate differ diff --git a/generator/lexer.mll b/generator/lexer.mll index 2fa0b613ef211255b7342c099e4ffa0812feef7f..59def45fdec00faf025aef85a319519700271c4e 100755 --- a/generator/lexer.mll +++ b/generator/lexer.mll @@ -116,7 +116,7 @@ let space = [' ' '\t'] let newline = ['\n' '\r']+ let upper = ['A'-'Z'] -let letter = ['a'-'z' 'A'-'Z' '_'] +let letter = ['a'-'z' 'A'-'Z' '_' '-'] let ident = ['a'-'z' 'A'-'Z' '_' '0'-'9'] let file = ['a'-'z' 'A'-'Z' '_' '-' '0'-'9'] let digit = ['0'-'9'] @@ -162,6 +162,7 @@ rule main ce = parse (* e is just created *) and entry e = parse | space { entry e lexbuf } + | (letter+ space+ letter+) as a { set_name e a ; text e lexbuf } | (letter+) as a { set_name e a ; text e lexbuf } | _ { error "Missing plugin or service name (at %S)" (Lexing.lexeme lexbuf) } @@ -173,7 +174,7 @@ and text e = parse | space { add_word e Space ; text e lexbuf } | eof { } - | space+ (digit as k) ')' { add_word e (Item k) ; text e lexbuf } + (* | space+ (digit as k) ')' { add_word e (Item k) ; text e lexbuf } *) | '#' ((digit+) as bug) { add_word e (PublicBts(int_of_string bug)) ; text e lexbuf } @@ -253,13 +254,20 @@ and text e = parse { major; minor; patch } (* compares both old-style (YYYYMMDD) and new-style numbering (MAJOR.MINOR) - note: codenames are only used in case of equality + note: codenames are only used for old versions or in case of equality *) let compare_version v1 v2 cn1 cn2 = - let re_old_numbering = Str.regexp "[0-9][0-9][0-9][0-9][0-9][0-9][0-9][0-9].*" in + let re_old_numbering = Str.regexp ".*\\([0-9][0-9][0-9][0-9][0-9][0-9][0-9][0-9]\\)" in let is_old_numbering v = Str.string_match re_old_numbering v 0 in - match is_old_numbering v1, is_old_numbering v2 with - | true, true -> String.compare v2 v1 + let get_old_version v = + let v = String.map (fun c -> if c = '_' then '-' else c) v in + assert(Str.string_match re_old_numbering v 0) ; + Str.matched_group 1 v + in + match is_old_numbering cn1, is_old_numbering cn2 with + | true, true -> + let r = String.compare (get_old_version cn2) (get_old_version cn1) in + if r = 0 then String.compare v2 v1 else r | false, true -> (* new numbering is always newer *) -1 | true, false -> (* old numbering is always older *) 1 | false, false -> (* compare new-style versions *)