Merge stable/nickel into master

Changelog

@@ -18,6 +18,10 @@
 Open Source Release <next-release>
 ###############################################################################
 
+###############################################################################
+Open Source Release 28.0 (Nickel)
+###############################################################################
+
 -!  Kernel    [2023-10-09] Remove options -no-type and -no-obj and related
               functions.
 o!  Kernel    [2023-10-03] New mechanism for generating default specifications

INSTALL.md

@@ -95,7 +95,7 @@ why3 config detect
 ### Reference configuration
 
 See file [reference-configuration.md](reference-configuration.md)
-for a set of packages that is known to work with Frama-C+dev.
+for a set of packages that is known to work with this version of Frama-C.
 
 ### Installing Custom Versions of Frama-C
 
@@ -182,8 +182,8 @@ opam depext --install -y frama-c
 
 #### Running the Frama-C GUI on WSL
 
-If you have WSL2: a known issue with Frama-C 24.0 (Chromium), lablgtk3 and
-Wayland require prefixing the command running the Frama-C GUI with
+If you have WSL2: a known issue with some versions of Frama-C, lablgtk3 and
+Wayland requires prefixing the command running the Frama-C GUI with
 `GDK_BACKEND=x11`, as in:
 
     GDK_BACKEND=x11 frama-c-gui <options>

VERSION

-27.1+dev
+28.0~beta

VERSION_CODENAME

-Cobalt
+Nickel

bin/frama-c-build-scripts.sh

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

dev/set-version.sh

@@ -52,7 +52,7 @@ CURRENT_MINOR=$(echo "$CURRENT" | $SED -e s/[0-9]*.\\\([0-9]*\\\).*/\\1/)
 CURRENT_CODENAME=$(grep "$CURRENT_MAJOR " ./doc/release/periodic-elements.txt | cut -d " " -f2)
 
 if [[ $NEXT == "dev" ]]; then
-  echo "Set VERSION to $CURRENT+dev"
+  echo "Set VERSION to $CURRENT_MAJOR.$CURRENT_MINOR+dev"
   echo "Continue? [y/N] "
   read CHOICE
   case "${CHOICE}" in
@@ -60,10 +60,10 @@ if [[ $NEXT == "dev" ]]; then
   *) exit 1 ;;
   esac
 
-  echo "$CURRENT+dev" >VERSION
-  $SED -i "s/^version: .*/version: \"$CURRENT+dev\"/g" opam
-  $SED -i "s/^version: .*/version: \"$CURRENT+dev\"/g" tools/lint/frama-c-lint.opam
-  $SED -i "s/^version: .*/version: \"$CURRENT+dev\"/g" tools/hdrck/frama-c-hdrck.opam
+  echo "$CURRENT_MAJOR.$CURRENT_MINOR+dev" >VERSION
+  $SED -i "s/^version: .*/version: \"$CURRENT_MAJOR.$CURRENT_MINOR+dev\"/g" opam
+  $SED -i "s/^version: .*/version: \"$CURRENT_MAJOR.$CURRENT_MINOR+dev\"/g" tools/lint/frama-c-lint.opam
+  $SED -i "s/^version: .*/version: \"$CURRENT_MAJOR.$CURRENT_MINOR+dev\"/g" tools/hdrck/frama-c-hdrck.opam
 else
   NEXT_MAJOR=$(echo "$NEXT" | $SED -e s/\\\([0-9]*\\\).[0-9]*.*/\\1/)
   NEXT_MINOR=$(echo "$NEXT" | $SED -e s/[0-9]*.\\\([0-9]*\\\).*/\\1/)
@@ -88,7 +88,7 @@ else
   echo "$NEXT_CODENAME" >VERSION_CODENAME
 
   # Opam files
-  $SED -i "s/^version: .*/version: \"$NEXT_MAJOR.$NEXT_MINOR\"/g" opam
+  $SED -i "s/^version: .*/version: \"$NEXT\"/g" opam
   $SED -i "s/\(.*\)$CURRENT_MAJOR.$CURRENT_MINOR-$CURRENT_CODENAME\(.*\)/\1$NEXT_MAJOR.$NEXT_MINOR-$NEXT_CODENAME\2/g" opam
 
   $SED -i "s/^version: .*/version: \"$NEXT_MAJOR.$NEXT_MINOR\"/g" tools/lint/frama-c-lint.opam
@@ -113,7 +113,7 @@ else
   $SED -i "s/\($WP_CL_MSG_FUTURE\)/\1\n$FC_CL_LIN\n\n$FC_CL_LIN\n$WP_CL_MSG_NEXT/g" src/plugins/wp/Changelog
 
   # API doc
-  find src -name '*.ml*' -exec $SED -i -e "s/Frama-C+dev/${NEXT}-${NEXT_CODENAME}/gI" '{}' ';'
+  find src -name '*.ml*' -exec $SED -i -e "s/Frama-C+dev/${NEXT_MAJOR}.${NEXT_MINOR}-${NEXT_CODENAME}/gI" '{}' ';'
 
   # Manuals changes
   $SED -i "s/\(^\\\\section\*{Frama-C+dev}\)/%\1\n\n\\\\section\*{$NEXT_MAJOR.$NEXT_MINOR ($NEXT_CODENAME)}/g" \
@@ -124,4 +124,12 @@ else
     doc/aorai/main.tex
   $SED -i "s/\(^\\\\section\*{E-ACSL \\\\eacslpluginversion \\\\eacslplugincodename}\)/%\1\n\n\\\\section\*{E-ACSL $NEXT_MAJOR.$NEXT_MINOR $NEXT_CODENAME}/g" \
     src/plugins/e-acsl/doc/userman/changes.tex
+
+  # Frama-C build script
+  $SED -i "s/(\\\\\\\"frama-c\\\\\\\" (>= [1-9][0-9]\.[0-9]))/(\\\\\\\"frama-c\\\\\\\" (>= $NEXT_MAJOR.$NEXT_MINOR))/g" bin/frama-c-build-scripts.sh
+
+  # Reference configuration
+  $SED -i "s/Frama-C [1-9][0-9]\.[0-9]/Frama-C $NEXT_MAJOR.$NEXT_MINOR/gI" \
+    reference-configuration.md
+
 fi

doc/LICENSE

-Copyright (C) 2007-2022
+Copyright (C) 2007-2023
 CEA (Commissariat à l'énergie atomique et aux énergies alternatives)
 
 Except where otherwise noted, content on this directory is licensed under a

doc/developer/check_api/check_and_compare.ml

@@ -2,7 +2,7 @@
 (*                                                                        *)
 (*  This file is part of Frama-C.                                         *)
 (*                                                                        *)
-(*  Copyright (C) 2007-2022                                               *)
+(*  Copyright (C) 2007-2023                                               *)
 (*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
 (*         alternatives)                                                  *)
 (*                                                                        *)

doc/developer/check_api/check_code.ml

@@ -2,7 +2,7 @@
 (*                                                                        *)
 (*  This file is part of Frama-C.                                         *)
 (*                                                                        *)
-(*  Copyright (C) 2007-2022                                               *)
+(*  Copyright (C) 2007-2023                                               *)
 (*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
 (*         alternatives)                                                  *)
 (*                                                                        *)

doc/developer/check_api/check_index_lexer.mll

@@ -2,7 +2,7 @@
 (*                                                                        *)
 (*  This file is part of Frama-C.                                         *)
 (*                                                                        *)
-(*  Copyright (C) 2007-2022                                               *)
+(*  Copyright (C) 2007-2023                                               *)
 (*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
 (*         alternatives)                                                  *)
 (*                                                                        *)

doc/developer/developer.tex

@@ -107,7 +107,9 @@ This is the documentation of the \framac
 implementation\footnote{\url{http://frama-c.com}} which aims at
 helping developers integrate new plug-ins inside this platform.
 
-The content of this document corresponds to the version \framacversion,released on \today,of \framac. However the development of \framac is still ongoing: features
+The content of this document corresponds to the version \framacversion,
+released on \today, of \framac.
+However the development of \framac is still ongoing: features
 described here may still evolve in the future.
 
 \section*{Acknowledgements}

doc/developer/tutorial/hello/src/dune

@@ -2,7 +2,7 @@
 ;;                                                                        ;;
 ;;  This file is part of Frama-C.                                         ;;
 ;;                                                                        ;;
-;;  Copyright (C) 2007-2022                                               ;;
+;;  Copyright (C) 2007-2023                                               ;;
 ;;    CEA (Commissariat à l'énergie atomique et aux énergies              ;;
 ;;         alternatives)                                                  ;;
 ;;                                                                        ;;

doc/developer/tutorial/hello/src/dune-project

@@ -3,7 +3,7 @@
 ;;                                                                        ;;
 ;;  This file is part of Frama-C.                                         ;;
 ;;                                                                        ;;
-;;  Copyright (C) 2007-2022                                               ;;
+;;  Copyright (C) 2007-2023                                               ;;
 ;;    CEA (Commissariat à l'énergie atomique et aux énergies              ;;
 ;;         alternatives)                                                  ;;
 ;;                                                                        ;;

doc/developer/tutorial/viewcfg/Makefile

@@ -2,7 +2,7 @@
 #                                                                        #
 #  This file is part of Frama-C.                                         #
 #                                                                        #
-#  Copyright (C) 2007-2022                                               #
+#  Copyright (C) 2007-2023                                               #
 #    CEA (Commissariat à l'énergie atomique et aux énergies              #
 #         alternatives)                                                  #
 #                                                                        #

doc/developer/tutorial/viewcfg/src/Makefile.split

@@ -2,7 +2,7 @@
 #                                                                        #
 #  This file is part of Frama-C.                                         #
 #                                                                        #
-#  Copyright (C) 2007-2022                                               #
+#  Copyright (C) 2007-2023                                               #
 #    CEA (Commissariat à l'énergie atomique et aux énergies              #
 #         alternatives)                                                  #
 #                                                                        #

doc/release/branch.tex

@@ -3,6 +3,13 @@
 
 That is the procedure for forking the release from \texttt{master}.
 
+\section{Creating the milestones}
+
+Create the milestone for the next releases on \textsf{Gitlab},
+in the Frama-C group. They will be used for development that will not
+be integrated into the upcoming release.
+\expertise{François, Julien}.
+
 \section{``Freezing'' master}
 
 When the ``freeze'' period arrives (usually a few weeks before the beta
@@ -48,15 +55,11 @@ and go through Merge-requests. Everything else should go in \texttt{master},
 which can then be reset to standard-level protection (Developers + Maintainers
 allowed to push/merge).
 
-\section{Creating the milestones}
-
-Create the milestone for the next release on \textsf{Gitlab},
-in the Frama-C group
-\expertise{François, Julien}.
-
-
 \section{GitLab issues}
 
+{\em This is currently done periodically in specific Frama-C meetings, so only
+  a final check is usually necessary.}~\\
+
 Check public issue tracker at \url{https://git.frama-c.com/pub/frama-c/issues/}.
 All issues should have been at least acknowledged: at least they should be
 assigned to someone, preferably tagged appropriately.
@@ -79,6 +82,8 @@ This will:
   \item update the \texttt{VERSION} and \texttt{VERSION\_CODENAME} files
   \item update the \texttt{opam} files (Frama-C, lint, hdrck)
   \item update the API doc
+  \item update the Frama-C build script
+  \item update the reference configuration
 \end{itemize}
 
 Merge the \texttt{stable} branch in the \texttt{master} branch.

doc/userman/userman.tex

@@ -44,7 +44,7 @@
 \addcontentsline{toc}{chapter}{Foreword}
 
 This is the user manual of \FramaC\footnote{\url{http://frama-c.com}}.  The
-content of this document corresponds to the version \framacversion, on \today, of
+content of this document corresponds to the version \framacversion, released on \today, of
 \FramaC.
 
 \section*{Acknowledgements}

opam

 opam-version: "2.0"
 name: "frama-c"
 synopsis: "Platform dedicated to the analysis of source code written in C"
-version: "27.1+dev"
+version: "28.0~beta"
 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-27.1-Cobalt.pdf"
+doc: "http://frama-c.com/download/user-manual-28.0-Nickel.pdf"
 bug-reports: "https://git.frama-c.com/pub/frama-c/issues"
 tags: [
   "deductive"

reference-configuration.md

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

releases/28.0.md

+# Kernel
+- Frama-C can now generate more default clauses (in particular terminates and exits)
+- Removed deprecated options `-no-type` and `-no-obj`
+
+# Alias
+- New plugin Alias, implements a points-to analysis
+
+# E-ACSL
+- More efficient code arithmetic calculations
+
+# Eva
+- Support for simple `\let` bindings
+- Removed deprecated Db.Value API
+- Fixed unsoundness about initialization with goto and switch
+
+# WP
+- New ACSL extensions for defining automatic proof strategies
+- WP generates default exits and terminates, removed old options `-wp-*-terminate`
+- Fixed cache for interactive provers
+
+# Ivette
+- Basic component for WP
+- Many bug fixes