diff --git a/Changelog b/Changelog index 964aeb6a2422dc827645797a4363c81bae53b312..e619fceeedb77c384c4a7f965b2de3e7359104ff 100644 --- a/Changelog +++ b/Changelog @@ -22,6 +22,9 @@ Open Source Release <next-release> Open Source Release 27.0 (Cobalt) ############################################################################### +-! Kernel [2023-05-15] New machdep mechanism, based on YAML files. A new + make_machdep.py script allows automatic machdep creation from a + C11-compatible (cross-)compiler. - Eva [2023-05-04] The octagon domain can now infer relations between any lvalues of integer or pointer types. -* Ivette [2023-05-02] Ends properly frama-c process when Ivette is closed. diff --git a/reference-configuration.md b/reference-configuration.md index fdd8a9c5f041ac331816d4ac864d63acdeaa9db1..f88987b805c1fec8e12bb34f6c733d9cd5d32924 100644 --- a/reference-configuration.md +++ b/reference-configuration.md @@ -14,6 +14,7 @@ compiling Frama-C+dev. - ocamlfind.1.9.5 - ocamlgraph.2.0.0 - ocp-indent.1.8.1 (for linting, optional) +- ppx_deriving_yaml.0.2.1 - ppx_deriving_yojson.3.7.0 - ppx_import.1.10.0 - why3.1.6.0 diff --git a/releases/27.0.md b/releases/27.0.md new file mode 100644 index 0000000000000000000000000000000000000000..f650a45758482e749082bcab405bed4ba5158804 --- /dev/null +++ b/releases/27.0.md @@ -0,0 +1,27 @@ +# Kernel +- Supports C11 `_Generic` +- New machdep mechanism, based on YAML files +- New script for generating machdeps from a C11 compiler + +# Aoraï +- Supports specification about floating-point variables. + +# Eva +- The octagon domain can now infer relations between any lvalues of integer or + pointer types. +- Fixes the bitwise domain on big-endian architectures. + +# WP +- Why3 version bumped to 1.6.0. +- New options for controlling goal automatic splitting +- Default timeout is now 2s + +# GTK GUI +- Removed GTK2 support + +# Ivette +- The Eva table can show the values of function parameters, the logical status + of ACSL predicates, and the values of C lvalues in these predicates. + It also shows the status of uninitialized and escaping variables. +- Information about C types are shown in the Inspector. +- Many bug fixes and user experience improvements.