Changes in coq 8.11.0:

Changes in frama-c 20.0:

  • Eva [2019/11/25] In the summary, fixes the number of alarms by category when the RTE plugin is used, and do not count logical properties in dead code as proven.
  • Kernel [2019/10/31] More stringent verifications on the use of ghost variable in non ghost-code. Fixes #2421
  • MdR [2019/10/31] New plug-in Markdown-Report (MdR) for markdown and SARIF outputs
  • Eva [2019/10/23] In the summary, fixes the total number of functions (and thus the computed analysis coverage).
  • Eva [2019/10/23] New option -eva-auto-loop-unroll N to unroll all loops whose number of iterations can be easily bounded by <N>.
  • Eva [2019/10/21] New octagon domain inferring relations of the form l ≤ ±X±Y ≤ e between pairs of integer variables X and Y. Enabled with option -eva-octagon-domain. Only infers relations between pairs of scalar variables occuring in a same instruction. Intra-procedural by default; octagons can be propagated through function calls with option -eva-octagon-through-calls.
  • ACSL [2019/10/04] Support for ghost parameters
  • Eva [2019/10/04] Evaluates ACSL predicates \is_plus_infinity and \is_minus_infinity.
  • Kernel [2019/10/04] Supports macro INFINITY and NAN.
  • Config [2019/09/27] ocp-indent 1.7.0 is now used for indentation
  • Eva [2019/09/16] Dynamic registration of abstract values and domains: developers of new domains no longer need to modify Eva's engine.
  • Kernel [2019/09/13] Fixes Hptmap on keys with id greater than 2^28.
  • Makefile [2019/09/12] Fixes #2378 - bytecode only compilation (patch contributed by madroach) and use -thread where needed.
  • Eva [2019/08/21] Fixes the reduction by the negation of \initialized and \dangling predicates on imprecise lvalues.
  • Kernel [2019/08/20] Fixes a rare but critical bug which occured when Frama-C internally switched the current project in presence of >2 projects and destroyed the old current project at about the same time: the Frama-C internal state became inconsistent and lead to unsound computations and crashes. It may be revealed to the end-user when using a long sequence of -then-replace (at least 3 of them).
  • Kernel [2019/08/20] Fixed sequence of -removed-projects and -then options.
  • Ptests [2019/08/05] Add new MODULE directive for compiling and loading an auxiliary OCaml module for a test
  • Kernel [2019/08/05] Add -keep-unused-types normalization option
  • Libc [2019/08/05] Remove obsolete (and forcing cpp error) builtins.h
  • Kernel [2019/08/02] Functions over visitor's behaviors have been moved from Cil into a new module Visitor_behavior. Apply the migration script potassium2calcium.sh to update your plug-ins automatically.
  • Sparecode [2019/07/26] Removed from Db. Use proper Sparecode API instead.
  • Kernel [2019/07/24] OCaml version greater than or equal to 4.05.0 required.
  • Kernel [2019/07/24] Improve placeholders handling in -cpp-command
  • Kernel [2019/07/23] Types in Properties are now records and not tuples
  • Eva [2019/07/09] Supports ACSL floating-point comparison operators eq_float, le_float, eq_double, le_double, etc.
  • Kernel [2019/06/28] removes AST constructors TCoerce, TCoerceE, PLCoercion, PLCoercionE, Psubtype and PLsubtype
  • Kernel [2019/06/20] fixes dangling ref when removing unused static local

Changes in ocaml-menhir 20200211:

Changes in why3 1.3.1:

These packages were simply rebuilt due to the other changes:

  • alt-ergo
  • coccinelle
  • flocq
  • zenon

Package pre-release version which supports OCaml 4.10 (#1817182).

How to install

sudo dnf upgrade --advisory=FEDORA-2020-bc649d3429

This update has been submitted for testing by jjames.

4 months ago

This update's test gating status has been changed to 'waiting'.

4 months ago

This update has obsoleted coccinelle-1.0.9-0.1.111d328fee1303f14a5b9def835301d849e41331.fc32, and has inherited its bugs and notes.

4 months ago

This update's test gating status has been changed to 'ignored'.

4 months ago

This update has been pushed to testing.

4 months ago
User Icon nixuser commented & provided feedback 4 months ago

I am still experiencing BZ#1795083 with this version.

BZ#1795083 The frama-c and frama-c-gui programs abort on startup in Rawhide (f32)

This update's test gating status has been changed to 'greenwave_failed'.

3 months ago

This update's test gating status has been changed to 'ignored'.

3 months ago

This update can be pushed to stable now if the maintainer wishes

3 months ago

This update has been submitted for stable by bodhi.

3 months ago

This update has been pushed to stable.

3 months ago

Please login to add feedback.

Metadata
Type
enhancement
Karma
0
Signed
Content Type
RPM
Test Gating
Settings
Unstable by Karma
-3
Stable by Karma
3
Stable by Time
7 days
Dates
submitted
4 months ago
in testing
4 months ago
in stable
3 months ago
BZ#1795083 The frama-c and frama-c-gui programs abort on startup in Rawhide (f32)
-1
0
BZ#1808111 coq fails to build with Python 3.9: 'caml_young_ptr' undeclared
0
0
BZ#1817182 coccinelle is not installable in F32
0
0

Automated Test Results