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.