merge changes from stable/nickel, 28.1

VERSION

-28.0+dev
+28.1+dev

bin/frama-c-build-scripts.sh

@@ -91,7 +91,7 @@ DuneProject () {
     echo "(maintainers \"anonymous\")"
     echo "(package (name ${PACKAGE})"
     echo "  (depends"
-    echo "    (\"frama-c\" (>= 28.0))"
+    echo "    (\"frama-c\" (>= 28.1))"
     echo "  )"
     echo " (tags (\"Frama-C scripts\"))"
     echo ")"

opam

 opam-version: "2.0"
 name: "frama-c"
 synopsis: "Platform dedicated to the analysis of source code written in C"
-version: "28.0+dev"
+version: "28.1+dev"
 description:"""
 Frama-C gathers several analysis techniques in a single collaborative
 framework, based on analyzers (called "plug-ins") that can build upon the
@@ -72,7 +72,7 @@ authors: [
 homepage: "https://frama-c.com/"
 license: "LGPL-2.1-only"
 dev-repo: "git+https://git.frama-c.com/pub/frama-c.git"
-doc: "http://frama-c.com/download/user-manual-28.0-Nickel.pdf"
+doc: "http://frama-c.com/download/user-manual-28.1-Nickel.pdf"
 bug-reports: "https://git.frama-c.com/pub/frama-c/issues"
 tags: [
   "deductive"
@@ -119,9 +119,13 @@ run-test: [
 ]
 
 depends: [
-  "dune" { >= "3.7.0" & < "3.13.0" }
+  "dune" { >= "3.7.0"
+         & != "3.13.0" # performance problem
+         }
   "dune-configurator"
-  "dune-site" { >= "3.7.0" & < "3.13.0" }
+  "dune-site" { >= "3.7.0"
+              & != "3.13.0" # performance problem
+              }
 
   ( "alt-ergo-free" | "alt-ergo" )
   "conf-graphviz" { post }

reference-configuration.md

 The following set of packages is known to be a working configuration for
-compiling Frama-C 28.0.
+compiling Frama-C 28.1.
 
 - OCaml 4.13.1
 - alt-ergo.2.4.2 (for wp, optional)

releases/28.1.md

+# Kernel
+
+- Fix Cil.isConstant on lvalues with offset.
+
+# Ivette
+
+- Fix Ivette shell wrapper on macOS.
+
+# WP
+
+- Fix interactive prover startup.

src/plugins/e-acsl/doc/Changelog

@@ -25,6 +25,10 @@
 Plugin E-ACSL <next-release>
 ###############################################################################
 
+###############################################################################
+Plugin E-ACSL 28.1 (Nickel)
+###############################################################################
+
 ###############################################################################
 Plugin E-ACSL 28.0 (Nickel)
 ###############################################################################

tools/hdrck/frama-c-hdrck.opam

 opam-version: "2.0"
 name: "frama-c-hdrck"
 synopsis: "Frama-C header check tool"
-version: "28.0"
+version: "28.1"
 description:"""
 Performs all checks related to file headers as required by the Frama-C
 continuous integration.

tools/lint/frama-c-lint.opam

 opam-version: "2.0"
 name: "frama-c-lint"
 synopsis: "Frama-C lint tool"
-version: "28.0"
+version: "28.1"
 description:"""
 Performs all checks related to source code formatting as required by the Frama-C
 continuous integration. Namely: OCP-indent for ML files, clang-format for E-ACSL