Skip to content
Snippets Groups Projects
Commit 99275fee authored by David Bühler's avatar David Bühler
Browse files

Timeline: adds events, and removes the images.

parent e59f8d70
No related branches found
No related tags found
1 merge request!32Better timeline
Showing
with 252 additions and 22 deletions
---
layout: default
date: 21-12-2017
title: Release of Frama-Clang 0.0.4
---
Frama-Clang 0.0.4, compatible with Frama-C 16, is out.
Download it [here](/fc-plugins/frama-clang.html).
\ No newline at end of file
---
layout: default
date: 19-02-2018
title: Release of Frama-Clang 0.0.5
---
Frama-Clang 0.0.5, fixing compatibility issue with Debian/Ubuntu, is out.
Download it [here](/fc-plugins/frama-clang.html).
\ No newline at end of file
---
layout: default
date: 23-07-2018
title: Release of Frama-Clang 0.0.6
---
Frama-Clang 0.0.6, compatible with Frama-C 17 Chlorine, is out.
Download it [here](/fc-plugins/frama-clang.html).
\ No newline at end of file
---
layout: default
date: 13-09-2019
title: Release of Frama-C Clang 0.0.7
image: /assets/img/events/frama-clang.png
title: Release of Frama-Clang 0.0.7
---
Frama-C Clang 0.0.7 is out. Download it [here](/fc-plugins/frama-clang.html).
\ No newline at end of file
Frama-Clang 0.0.7 is out. Download it [here](/fc-plugins/frama-clang.html).
\ No newline at end of file
---
layout: default
date: 10-03-2020
title: Release of Frama-Clang 0.0.8
---
Frama-Clang 0.0.8 is out. Download it [here](/fc-plugins/frama-clang.html).
\ No newline at end of file
---
layout: default
date: 31-05-2017
title: Release of Frama-C 15.0 (Phosphorus)
---
Frama-C 15.0 (Phosphorus) is out. Download it [here](/fc-versions/phosphorus.html).
Main changes with respect to Frama-C 14 - Silicon include:
#### Kernel
- E-ACSL is now included in the standard distribution
- Better handling of Variable-Length Arrays (VLA)
- ZArith is now a required dependency. Support of Big_int has been dropped
- Bash and Zsh completion for Frama-C options
- new AST nodes to explicitly mark local variable initialization
#### EVA
- better set of default options
- dropped support for legacy version of Value Analysis
#### WP
- Interactive Proof Editor in the GUI
- Extensible Proof Engine via Tactics and Strategies
- More powerful simplifications of goals
- Dynamic API is deprecated in favor of static API
- Fatally flawed support of generalized invariants (`-wp-invariants`)
has been dropped
#### E-ACSL
- included in the standard Frama-C distribution
- use of a (much more efficient) shadow memory model by default
- much better support of unstructured control flow (complex goto, ...)
#### Variadic
- translation of variadic calls is now enabled by default
- option names have changed to avoid confusion with EVA
A complete changelog can be found [here](/html/changelog.html#Phosphorus-15.0).
\ No newline at end of file
---
layout: default
date: 29-11-2017
title: Release of Frama-C 16.0 (Sulfur)
---
Frama-C 16.0 (Sulfur) is out. Download it [here](/fc-versions/sulfur.html).
Main changes with respect to Frama-C 15 - Phosphorus include:
#### Kernel
- Extra type checking verifications
(e.g. const on local variables, qualifiers in function calls)
#### EVA
- Precision and efficiency improvements
- Better feedback for abstract domains
- Scripts to help analyze large programs
(in $FRAMAC_SHARE/analysis-scripts)
#### WP
- New tacticals for TIP
(for dealing with modulus, bit operations, equality rewriting, etc)
- Several new simplifications
#### RTE
- Emission of more alarms (\initialized)
#### Studia
- New plug-in for case studies with EVA, integrated in the GUI
#### GUI
- Display of local callgraphs (useful for large programs)
A complete changelog can be found [here](/html/changelog.html#Sulfur-16.0).
\ No newline at end of file
......@@ -2,7 +2,34 @@
layout: default
date: 31-05-2018
title: Release of Frama-C 17.0 (Chlorine)
image: /assets/img/events/Chlorine.jpg
---
Frama-C 17.0 (Chlorine) is out. Download it [here](/fc-versions/chlorine.html).
\ No newline at end of file
Frama-C 17.0 (Chlorine) is out. Download it [here](/fc-versions/chlorine.html).
Main changes with respect to Frama-C 16 - Sulfur include:
#### Kernel
* Added option -inline-calls for syntactic inlining
* Introduced warning categories: possibility of disabling some warnings, converting warnings into errors and vice-versa, and more detailed warning messages
* Added support for CERT EXP46-C
* Extra-type checking verifications (e.g. in function pointer compatibility and lvalues assignments)
* Added support for JSON compilation databases, a.k.a. compile_commands.json (optional: requires package 'yojson')
#### EVA
* Added support for infinite floats and NaN (via option -warn-special-float)
* Added a new panel "Red alarms" in the GUI that shows all properties for which a red status has been emitted for some states during the analysis. They may not be completely invalid, but should often be investigated first
* Evaluate the preconditions of the functions for which a builtin is used; builtins do not emit alarms anymore
* The subdivision of evaluations (through the option -val-subdivide-non-linear) can subdivide the values of several lvalues simultaneously (on expressions such as x*x - 2*x*y + y*y)
* Various improvements in the equality domain which is now inter-procedural (equalities can be propagated through function calls)
#### WP
* Support for ACSL math builtins (\sqrt, \exp, \log, etc.) and _Bool type
* Improved Qed simplifications in many domains
* Upgrade reference versions for provers (Alt-Ergo 2.0.0, Coq 8.7.1 and Why-3 0.88.3)
* New and/or enhanced tactics available from the graphical user-interface
* Searching for strategies from the command line
#### E-ACSL
* New option -e-acsl-validate-format-strings to detect format string vulnerabilities in printf-like functions
A complete changelog can be found [here](/html/changelog.html#Chlorine-17.0).
\ No newline at end of file
......@@ -2,7 +2,42 @@
layout: default
date: 29-10-2018
title: Release of Frama-C 18.0 (Argon)
image: /assets/img/events/Argon.jpg
---
Frama-C 18.0 (Argon) is out. Download it [here](/fc-versions/argon.html).
\ No newline at end of file
Frama-C 18.0 (Argon) is out. Download it [here](/fc-versions/argon.html).
Main changes with respect to Frama-C 17 (Chlorine) include:
#### Kernel:
- Improved command-line options for treatment of warning categories:
-plugin-warn-key category:status will set the status of category,
instead of using 7 options -plugin-warn-abort, -plugin-warn-feedback, …
with awkward ± categories
- All errors emitted during a run will now lead to a non-zero exit status
of frama-c command line
- options for emitting an alarm on [left|right] shift of a negative
value are now at kernel level (and removed from Eva)
- const globals are now unconditionally constants (option -const-writable is
removed)
- several improvements to the frama-c libc specifications
- new binary frama-c-script to help with case studies
#### Eva:
- Eva is now consistently named "Eva", and all its options start with -eva
(compatibility with previous option names has been preserved).
- New "//@ loop unroll N;" annotations to unroll exactly the N first iterations
of a loop, as an improvement over slevel options.
- The memexec cache is compatible with all domains, and is enabled by default.
This cache greatly improves the analysis time.
- Builtins for memset and memcpy are now included in the open-source release.
- Alternative domains use the frama-c libc specification when a builtin is used,
to minimize the loss of precision.
- Emits alarms when reading trap representations of type _Bool.
- New experimental domain numerors inferring absolute and relative errors of
floating-point computations. Does not handle loops for now.
#### E-ACSL:
- support of ranges in memory built-ins, e.g. \valid(t+(0..9))
- support of \at on logic variables, e.g. \forall integer i; 0 <= i < 10 ==> t[i] == \old(t[i])
A complete Changelog can be found [here](/html/changelog.html#Argon-18.0).
\ No newline at end of file
......@@ -2,7 +2,39 @@
layout: default
date: 21-06-2019
title: Release of Frama-C 19.0 (Potassium)
image: /assets/img/events/Potassium.jpg
---
Frama-C 19.0 (Potassium) is out. Download it [here](/fc-versions/potassium.html).
\ No newline at end of file
Frama-C 19.0 (Potassium) is out. Download it [here](/fc-versions/potassium.html).
Main changes with respect to Frama-C 18 (Argon) include:
#### Kernel:
- new check annotation, similar to assert except that it does not introduce
additional hypotheses on the program state
- new options added to frama-c-script
#### GUI:
- compatibility with lablgtk3
#### Eva:
- New annotation "//@ split exp" to separate the analysis states for each
possible value of an expression until a "//@ merge exp" annotation.
- New option -eva-partition-history to delay the join of the analysis states at
merging points; useful when a reasoning depends on the path taken to reach a
control point.
- By default, prints a summary at the end of the analysis.
- New meta option -eva-precision to globally configure the analysis.
- Improved precision on nested loops.
#### WP:
- new auto-search mode to automatically apply strategies and tactics (see -wp-auto)
- extended simplifications on range, bitwise and C-boolean values (_Bool is now
handled by default)
- refactored float model (although it still requires further axiomatisation)
#### E-ACSL:
- support for user-defined logic functions and predicates without labels
- new option -e-acsl-functions that allows the user to specify a white/black list
of functions in which annotations are monitored, or not.
A complete changelog can be found [here](/html/changelog.html#Potassium-19.0).
\ No newline at end of file
......@@ -2,7 +2,9 @@
layout: default
date: 17-09-2019
title: Release of Frama-C 19.1 (Potassium)
image: /assets/img/events/Potassium.jpg
---
Frama-C 19.1 (Potassium) is out. Download it [here](/fc-versions/potassium.html).
\ No newline at end of file
Frama-C 19.1 (Potassium) is out. Download it [here](/fc-versions/potassium.html).
This release merely restores compatibility with OCaml 4.08.1 (and the new
4.09.0), and fixes a few issues with lablgtk3.
\ No newline at end of file
---
layout: default
date: 04-12-2019
title: Release of Frama-C 20.0 (Calcium)
---
Frama-C 20.0 (Calcium) is out. Download it [here](/fc-versions/calcium.html).
Main changes with respect to Frama-C 19 (Potassium) include:
##### Kernel:
- the minimum required OCaml version is now 4.05.0
- more strict checks related to ghost variables in non-ghost code, and support for ghost parameters
- visitor behavior functions were moved from Cil to a new module Visitor_behavior
##### Eva:
- New octagon domain inferring relations of the form
a ≤ ±X±Y ≤ b between pairs of integer variables X and Y.
- New option "-eva-auto-loop-unroll N", to unroll all
loops whose number of iterations can be easily bounded by <N>.
- Dynamic registration of abstract values and domains:
developers of new domains no longer need to modify Eva's engine.
##### WP:
- Use native Why3 API (now requires why3 at compile time); deprecated native alt-ergo & coq output
- New cache mechanism for why3 provers, see -wp-cache option
##### E-ACSL:
- Support of rational numbers and operations.
And a new plug-in, Markdown-report (MdR), to generate reports in both Markdown and SARIF formats.
A complete changelog can be found [here](/html/changelog.html#Calcium-20.0).
\ No newline at end of file
......@@ -1469,12 +1469,8 @@ a.goDown .icon {
.calendarScreen {
/*background: #f6f6f6;*/
overflow: hidden;
}
@media (max-width: 767px) {
.calendarScreen {
height: auto;
padding-bottom: 120px;
}
height: auto;
padding-bottom: 120px;
}
.calendarScreen .sectionContent {
padding: 28px 0 20px;
......@@ -1579,13 +1575,13 @@ a.goDown .icon {
}
@media (min-width: 768px) {
.eventDetailsBlock .eventDetail {
width: 640px;
width: 100%;
margin: 0 auto;
padding-bottom: 30px;
}
.eventDetailsBlock .eventDetail .contentBlk {
display: inline-flex;
width: 330px;
width: auto;
vertical-align: middle;
padding: 10px 0 0 15px;
}
......@@ -1596,7 +1592,7 @@ a.goDown .icon {
padding-bottom: 40px;
}
.eventDetailsBlock .eventDetail .contentBlk {
width: 400px;
width: auto;
padding: 12px 0 0 22px;
font-size: 14px;
}
......@@ -1610,7 +1606,7 @@ a.goDown .icon {
width: 1080px;
}
.eventDetailsBlock .eventDetail .contentBlk {
width: 500px;
width: auto;
font-size: 15px;
}
.eventDetailsBlock .eventDetail .contentBlk > div {
......@@ -1627,7 +1623,7 @@ a.goDown .icon {
padding-bottom: 50px;
}
.eventDetailsBlock .eventDetail .contentBlk {
width: 520px;
width: auto;
padding: 15px 0 0 27px;
font-size: 16px;
}
......
assets/img/events/Argon.jpg

7.25 KiB

assets/img/events/Chlorine.jpg

11.7 KiB

assets/img/events/Phosphorus.png

135 KiB

assets/img/events/Potassium.jpg

7.7 KiB

assets/img/events/Sulfur.jpg

17 KiB

assets/img/events/fc-day-2019.png

195 KiB

assets/img/events/frama-clang.png

7.37 KiB

0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment