[release] Create 30.0 Changelog

releases/30.0.md

+# Kernel
+
+- Frama-C now requires at least OCaml 4.14
+- Support for ACSL modules and for importing external modules in ACSL
+- Removed `loop pragma UNROLL` in favor of new ACSL extension `loop unfold`
+
+# Alias
+
+- No longer classify all casts as unsafe
+
+# E-ACSL
+
+- Partial support for labelled logic functions (only when called with `Here` label)
+- Fix typing of logic functions over rationals
+- Fix code generation for logic functions called in different, incompatible, contexts
+- Fix logic variable escaping its scope
+
+# Eva
+
+- Fix potential unsoundness when writing `0` on a set of contiguous locations with different size/alignment than the write
+- Fix missing signed overflow alarm on modulo
+- Fewer false alarms of signed overflow on division
+- Never emit an alarm on pointer conversions to `intptr_t` or `uintptr_t` 
+- Support for `calls` ACSL extension (indicating possible targets of indirect calls)
+
+# RTE
+
+- Fix missing signed overflow alarm on modulo
+- Never emit an alarm on pointer conversions to `intptr_t` or `uintptr_t`
+
+# Wp
+
+- Why3 module importer
+
+# Ivette
+
+- New Flamegraph component to visualize Eva analysis time
+- New callgraph features, including filtering, selecting, and showing alarms per function