_data/nav.yml

+- name: Using Frama-C
+  link: /html/using-frama-c.html
+- name: Features
+  link: /html/kernel-plugin.html
+- name: Documentation
+  link: /dokuwiki/start.html
+- name: Blog
+  link: /blog/index.html
+- name: Careers
+  link: /html/careers.html
+- name: Contact
+  link: /html/contact.html

_data/tabs.yml

+- name: Plugins
+  link: /html/kernel-plugin.html
+- name: Kernel
+  link: /html/kernel.html
+- name: ACSL
+  link: /html/acsl.html
+- name: GUI
+  link: /html/gui.html

_events/clang-0.1.md

+---
+layout: default
+date: 04-07-2016
+event: Frama-Clang 0.0.1
+title: Release of Frama-Clang 0.0.1
+---
+
+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

_events/clang-0.2.md

+---
+layout: default
+date: 05-05-2017
+event: Frama-Clang 0.0.2
+title: Release of Frama-Clang 0.0.2
+---
+
+Version 0.0.2 of the Frama-Clang plugin is available for download.
\ No newline at end of file

_events/clang-0.3.md

+---
+layout: default
+date: 02-08-2017
+event: Frama-Clang 0.0.3
+title: Release of Frama-Clang 0.0.3
+---
+
+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

_events/clang-0.4.md

+---
+layout: default
+date: 21-12-2017
+event: Frama-Clang 0.0.4
+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

_events/clang-0.5.md

+---
+layout: default
+date: 19-02-2018
+event: Frama-Clang 0.0.5
+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

_events/clang-0.6.md

+---
+layout: default
+date: 23-07-2018
+event: Frama-Clang 0.0.6
+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

_events/clang-0.7.md

 ---
 layout: default
 date: 13-09-2019
-title: Release of Frama-C Clang 0.0.7
-image: /assets/img/events/frama-clang.png
+event: Frama-Clang 0.0.7
+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

_events/clang-0.8.md

+---
+layout: default
+date: 10-03-2020
+event: Frama-Clang 0.0.8
+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

_events/eacsl-0.8.md

+---
+layout: default
+date: 17-01-2017
+event: 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

_events/fc-day-2019.md

 ---
 layout: default
 date: 18-05-2019
+event: Frama-C & SPARK Day 2019
 title: Frama-C & SPARK Day 2019
-image: /assets/img/events/fc-day-2019.png
 ---
 
 Frama-C & SPARK Day 2019 will take place on June 3, 2019 in Paris.

_events/framac-10.md

+---
+layout: default
+date: 07-03-2014
+event: Frama-C 10.0 (Neon)
+title: Release of Frama-C 10.0 (Neon)
+---
+
+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.

_events/framac-11.md

+---
+layout: default
+date: 06-03-2015
+event: Frama-C 11.0 (Sodium)
+title: Release of Frama-C 11.0 (Sodium)
+---
+
+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

_events/framac-12.md

+---
+layout: default
+date: 15-01-2016
+event: Frama-C 12.0 (Magnesium)
+title: Release of Frama-C 12.0 (Magnesium)
+---
+
+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

_events/framac-13.md

+---
+layout: default
+date: 31-05-2016
+event: Frama-C 13.0 (Aluminium)
+title: Release of Frama-C 13.0 (Aluminium)
+---
+
+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

_events/framac-14.md

+---
+layout: default
+date: 01-12-2016
+event: Frama-C 14.0 (Silicon)
+title: Release of Frama-C 14.0 (Silicon)
+---
+
+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

_events/framac-15.0.md

+---
+layout: default
+date: 31-05-2017
+event: Frama-C 15.0 (Phosphorus)
+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

_events/framac-16.0.md

+---
+layout: default
+date: 29-11-2017
+event: Frama-C 16.0 (Sulfur)
+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

_events/framac-17.0.md

 ---
 layout: default
 date: 31-05-2018
+event: Frama-C 17.0 (Chlorine)
 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