Commit 348b4eb4 authored by François Bobot's avatar François Bobot
Browse files

Start conversion of Frama-C website

      half of the index done
parent 73d7084b
Pipeline #36707 passed with stage
in 1 minute and 27 seconds
---
layout: default
date: 20-08-2021
short_title: Colibri2 0.1
title: First public release of Colibri2
link:
---
The solver supports:
* Boolean
* Linear arithmetic (using Fourier-Mostkin)
* Uninterpreted symbols
* Quantifiers
* Polymorphism
In a limited way:
* Floating Point numbers
* Function ceil and floor
---
layout: default
date: 01-01-2014
short_title: SOPRANO
title: Start of the SOPRANO project
link: https://soprano-project.fr
---
The [ANR](https://anr.fr/Project-ANR-14-CE28-0020) [SOPRANO
project](http://soprano-project.fr) allowed to gather researchers working on SMT
(OcamlPro, Université Paris-Saclay) and CP (CEA, INRIA) and industrials partner
(Adacore) in the domain of software verification. The goal was to merge the
powerful learning of SMT and the powerful propagations of CP.
---
layout: default
date: 04-07-2016
short_title: Frama-Clang 0.0.1
title: Release of Frama-Clang 0.0.1
link: /fc-plugins/frama-clang.html
---
The first version of the [Frama-Clang](/fc-plugins/frama-clang.html) plugin,
an experimental C++ front-end for Frama-C, is available.
\ No newline at end of file
---
layout: default
date: 08-03-2021
short_title: Frama-Clang 0.0.10
title: Release of Frama-Clang 0.0.10
link: /fc-plugins/frama-clang.html
---
Frama-Clang 0.0.10 is out. Download it [here](/fc-plugins/frama-clang.html).
---
layout: default
date: 13-07-2021
short_title: Frama-Clang 0.0.11
title: Release of Frama-Clang 0.0.11
link: /fc-plugins/frama-clang.html
---
Frama-Clang 0.0.11 is out. Download it [here](/fc-plugins/frama-clang.html).
---
layout: default
date: 05-05-2017
short_title: Frama-Clang 0.0.2
title: Release of Frama-Clang 0.0.2
link: /fc-plugins/frama-clang.html
---
Version 0.0.2 of the Frama-Clang plugin is available for download.
\ No newline at end of file
---
layout: default
date: 02-08-2017
short_title: Frama-Clang 0.0.3
title: Release of Frama-Clang 0.0.3
link: /fc-plugins/frama-clang.html
---
Frama-Clang 0.0.3, compatible with Frama-C 15, is out.
Download it [here](/fc-plugins/frama-clang.html).
\ No newline at end of file
---
layout: default
date: 21-12-2017
short_title: Frama-Clang 0.0.4
title: Release of Frama-Clang 0.0.4
link: /fc-plugins/frama-clang.html
---
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
short_title: Frama-Clang 0.0.5
title: Release of Frama-Clang 0.0.5
link: /fc-plugins/frama-clang.html
---
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
short_title: Frama-Clang 0.0.6
title: Release of Frama-Clang 0.0.6
link: /fc-plugins/frama-clang.html
---
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
short_title: Frama-Clang 0.0.7
title: Release of Frama-Clang 0.0.7
link: /fc-plugins/frama-clang.html
---
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
short_title: Frama-Clang 0.0.8
title: Release of Frama-Clang 0.0.8
link: /fc-plugins/frama-clang.html
---
Frama-Clang 0.0.8 is out. Download it [here](/fc-plugins/frama-clang.html).
\ No newline at end of file
---
layout: default
date: 15-07-2020
short_title: Frama-Clang 0.0.9
title: Release of Frama-Clang 0.0.9
link: /fc-plugins/frama-clang.html
---
Frama-Clang 0.0.9 is out. Download it [here](/fc-plugins/frama-clang.html).
\ No newline at end of file
---
layout: default
date: 17-01-2017
short_title: E-ACSL 0.0.8
title: Release of E-ACSL 0.0.8
---
Version 0.8 of the E-ACSL plugin is available.
\ No newline at end of file
---
layout: default
date: 18-05-2019
short_title: Frama-C and SPARK Day 2019
title: Frama-C and SPARK Day 2019
---
Frama-C & SPARK Day 2019 will take place on June 3, 2019 in Paris.
Registration and program [here](http://frama-c.com/FCSD19.html).
\ No newline at end of file
---
layout: default
date: 07-03-2014
short_title: Frama-C 10.0 (Neon)
title: Release of Frama-C 10.0 (Neon)
link: /fc-versions/neon.html
---
Frama-C 10.0 (Neon) is available.
This new major version includes too many bug fixes and improvements to
list here: details are available at http://frama-c.com/Changelog.html.
The main highlights are:
- The Value plugin is more efficient (computation and cache have been
optimized). The experimental option -val-show-perf helps estimating
which part of the C code takes time to analyze. One can send SIGUSR1
signal to a Frama-C process for stopping and saving the
partial results of the Value plugin.
- The From plugin computes separately data dependencies and indirect
(address, control) dependencies with option -show-indirect-deps
- The axiomatizations used by the WP plugin are now shared between the
different prover outputs and mainly realized in Coq thanks to a better
integration with Why3.
For plug-in developers:
- The api for Dataflow have been greatly simplified.
- This major release changes several Frama-C APIs
in an incompatible way. Some of the plugin-side changes can
be automatically applied by using the script bin/fluorine2neon.sh of
the source distribution. Complex plug-ins should be reviewed for
compatibility.
---
layout: default
date: 06-03-2015
short_title: Frama-C 11.0 (Sodium)
title: Release of Frama-C 11.0 (Sodium)
link: /fc-versions/sodium.html
---
Frama-C 11.0 (Sodium) is available.
This new major version includes too many bug fixes and improvements to
list here: details are available at http://frama-c.com/Changelog.html.
The main highlights are:
- **kernel**: Frama-C standard library is included by default (-no-frama-c-stdlib
for the previous behavior)
- **kernel**: When preprocessor supports it, expansions of macros in
annotations (-pp-annot) is now done by default. Efficiency of
-pp-annot has been greatly improved.
- **kernel**: the default machdep no longer assumes the compiler is gcc. See
'frama-c -machdep help'
- Homogenization of collections options (eg: -cpp-extra-args, -slevel-function)
- **value**: much-improved pretty-printing of pointer abstract values
- **value**: logic ranges are now evaluated using a dedicated domain,
resulting in faster analysis and more precise results
- **value**: the parameters of a function call may be reduced if they are
constrained by the callee
- **kernel, value**: support for \dangling predicate
- **kernel, value, WP**: support for const variables
- **rte, value**: alarms are now emitted for casts from floating-point to integer
that overflow
- **from**: assigns/from acsl clauses of functions with a body can now be verified
through option -from-verify-assigns
- **from**: major performance improvements on large input programs.
- **semantic constant folding**: better propagation on pointer variables
For plug-in developers:
- New API for collections options
- New AST nodes Throw and TryCatch for dealing with exception. The C
front-end does not generate any such node. A code transformation can
compile such nodes away if needed (see src/kernel/exn_flow.mli for
more information).
\ No newline at end of file
---
layout: default
date: 15-01-2016
short_title: Frama-C 12.0 (Magnesium)
title: Release of Frama-C 12.0 (Magnesium)
link: /fc-versions/magnesium.html
---
Frama-C 12.0 (Magnesium) is available.
This new major version includes too many bug fixes and improvements to
list here: details are available at http://frama-c.com/Changelog.html.
The main highlights are:
- **value**: brand new GUI, found in the "Values" tab
- **value**: new builtins for floating-point functions of the standard library
- **value**: more fine-grained control on the value of padding after initialisation
- **value**: multiple improvements to option -subdivide-float-var
- **wp**: many improvements for user experience (see Changelog)
- **wp**: many new or improved simplifications in Qed (see Changelog)
- **wp**: support for global const (see -wp-init-const option)
- **wp**: refined memory access and compound encoding
- **wp**: new memory model 'Caveat' for unit-proofs
- **wp**: new (less precise) integer model 'rg' to simplify integral ranges
- **wp**: more ACSL builtins (\subset, \is_NaN, \is_finite, \is_infinite, \is_plus_infinity,
\is_minus_infinity)
- **report**: new report in .csv format
---
layout: default
date: 31-05-2016
short_title: Frama-C 13.0 (Aluminium)
title: Release of Frama-C 13.0 (Aluminium)
link: /fc-versions/aluminium.html
---
Frama-C 13.0 (Aluminium) is available.
This major version fixes many bugs and includes improvements
and three new plug-ins.
The main highlights are:
- **variadic**: new plug-in which translates variadic functions, calls and
macros to allow analyses to handle them more easily.
- **loop**: new plug-in which estimates loop bounds and -slevel-function
parameters.
- **nonterm**: new plug-in for detection of definite non-termination based on
Value.
- **value**: major reimplementation of large parts of the plugin. New analysis
domains are available (see options -eva-equality-domain and
-eva-bitwise-domain), and the analysis of conditionals has been
improved. 'direct' and 'indirect' annotations are now used to evaluate
assigns clauses. Better propagation strategy for nested loops and changes
in the widening strategy for frontiers of integer types.
- **cil**: various improvements to the handling of empty structs, zero-length
arrays, and flexible array members.
- **kernel**: automatic generation of assigns from GCC's extended asm.
- **ACSL**: new predicate \valid_function, requiring the compatibility
between the type of the pointer and the function being pointed (currently
supported by Value), notation { x, y, z } for defining sets and built-in
operators for lists (currently supported by WP).
\ No newline at end of file
---
layout: default
date: 01-12-2016
short_title: Frama-C 14.0 (Silicon)
title: Release of Frama-C 14.0 (Silicon)
link: /fc-versions/silicon.html
---
Frama-C 14.0 (Silicon) is available.
Main changes are:
Kernel:
- refactoring of ACSL extensions + allow extensions in loop annotations
- rename multiple types of the logic AST for more coherence
Libc:
- The implementations of some functions of the standard library are now available in share/libc/*.c. The .c and .h files in share/libc are deprecated.
Eva/Value plugin:
- two now (experimental) analysis domains are available. Gauges infer affine relations between variables in loops. Symbolic locations keep track of the contents of l-values such as *p or t[i].
- new builtins are available for dynamic allocation, and some functions of string.h and. Default builtins can be activated through option -val-builtins-auto.
WP plugin:
- unified variable usage for all models
- WP now honors the kernel option -warn-(signed|unsigned)-(overflow|downcast). The cint and cfloat are used by default
Rte plugin:
- new option -rte-pointer-call, to generate annotations for calls through function pointers.
Nonterm plugin:
- overall increase in precision, especially on compound statements (if, switch, loops...).
Changes in the compilation process:
- OCamlGraph is no longer packaged within Frama-C, and must be installed to build Frama-C from source.
- OCaml version greater or equal than 4.02.3 required..
A complete changelog can be found [here](/html/changelog.html#Silicon-14.0).
\ No newline at end of file
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment