ALL_VERSIONS

 Version number			Date of release		Notes
 ==============			===============		=====
+24.0 (Chromium)                 2021, November 30
 23.1 (Vanadium)                 2021, July 20
 23.0 (Vanadium)                 2021, July 7
 22.0 (Titanium)                 2020, November 17

Changelog

@@ -17,6 +17,14 @@
 Open Source Release <next-release>
 ##################################
 
+o!  Kernel    [2021-12-03] Remove unused AST node Dcustom_annot and field
+              fpadding_in_bits. Do not cache size of types in the AST but in
+              a dedicated table.
+-*  Logic     [2021-11-30] Fix type of expressions whose value are functions
+o!  Kernel    [2021-11-29] Integer.pretty does not have the optional argument
+              hexa anymore. Use Integer.pretty_hex or Integer.pp_hex if you
+              want to print integers in hexadecimal format.
+
 ###################################
 Open Source Release 24.0 (Chromium)
 ###################################

VERSION

-24.0-beta+dev
+24.0+dev

bin/frama-c-script

@@ -21,13 +21,18 @@
 #                                                                        #
 ##########################################################################
 
-# Accept '-check' to avoid issues with ptests
-while [ $# -ge 1 ] && [ "$1" = "-check" ]; do
-    shift
+WORKING_DIR="."
+while [ "$1" != "" ] ; do
+    case "$1" in
+        -check) shift;;
+        -C) shift; WORKING_DIR="$1";;
+        *) break;;
+    esac
+   shift
 done
 
 usage() {
-   echo "usage: $0 cmd [args]"
+   echo "usage: $0 [-C working-dir] cmd [args]"
    echo ""
    echo "  where cmd is:"
    echo ""
@@ -111,6 +116,8 @@ if [ $# -lt 1 ]; then
 fi
 
 DIR="$( cd "$( dirname "$0" )" && pwd )"
+cd "$WORKING_DIR"
+
 # All scripts called by frama-c-script may rely on FRAMAC_BIN pointing to the
 # directory containing frama-c, frama-c-config and frama-c-script.
 export FRAMAC_BIN="$DIR"
@@ -118,6 +125,7 @@ FRAMAC_SHARE=$("${DIR}/frama-c-config" -print-share-path)
 if [ -z ${FRAMAC_SESSION+x} ]; then
     FRAMAC_SESSION="./.frama-c";
 fi
+
 command="$1"
 
 # [check_path_exists path]: if [path] exists,

bin/migration_scripts/chromium2manganese.sh

+#!/bin/bash
+##########################################################################
+#                                                                        #
+#  This file is part of Frama-C.                                         #
+#                                                                        #
+#  Copyright (C) 2007-2021                                               #
+#    CEA (Commissariat à l'énergie atomique et aux énergies              #
+#         alternatives)                                                  #
+#                                                                        #
+#  you can redistribute it and/or modify it under the terms of the GNU   #
+#  Lesser General Public License as published by the Free Software       #
+#  Foundation, version 2.1.                                              #
+#                                                                        #
+#  It is distributed in the hope that it will be useful,                 #
+#  but WITHOUT ANY WARRANTY; without even the implied warranty of        #
+#  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         #
+#  GNU Lesser General Public License for more details.                   #
+#                                                                        #
+#  See the GNU Lesser General Public License version 2.1                 #
+#  for more details (enclosed in the file licenses/LGPLv2.1).            #
+#                                                                        #
+##########################################################################
+
+#
+# Converts a Frama-C plugin from Frama-C 24 Chromium to Frama-C 25 Maganese,
+# on a best-efforts basis (no guarantee that the result is fully compatible).
+#
+# known missing features:
+# - doesn't follow symbolic links to directories
+
+DIR=
+
+# verbose on by default
+VERBOSE="v"
+
+# test once if sed supports -i (BSD/macOS does not)
+SED_HAS_I=$(sed --help 2>/dev/null | grep '\-i' 2>/dev/null)
+
+# [sedi file expressions] runs 'sed -i expressions' on the specified file;
+# if '-i' is not supported, creates a temporary file and overwrites the
+# original, like '-i' does.
+sedi ()
+{
+  file="$1"
+  shift
+  if [ -n "$SED_HAS_I" ]; then
+    sed -i "$@" "$file"
+  else
+    # option '-i' is not recognized by sed: use a tmp file
+    new_temp=`mktemp /tmp/frama-c.XXXXXXX` || exit 1
+    sed "$@" "$file" > "$new_temp"
+    mv -f "$new_temp" "$file"
+  fi
+}
+
+dirs ()
+{
+  if [ -z "$DIR" ]; then
+    DIR=.
+  fi
+}
+
+# [safe_goto d1 d2 cmd] goes to d1, runs cmd, and returns to d2
+safe_goto ()
+{
+  dir="$1"
+  cd "$dir"
+  $3
+  cd "$2"
+}
+
+goto ()
+{
+  if [ -d "$1" ]; then
+    safe_goto "$1" "$2" "$3"
+  else
+    echo "Directory '$1' does not exist. Omitted."
+  fi
+}
+
+process_file ()
+{
+  file="$1"
+  if [ "$VERBOSE" ]; then
+    echo "Processing file $file"
+  fi
+  sedi "$file" \
+   -e 's/(Integer\.pretty ~hexa:false)/Integer.pretty/g' \
+   -e 's/(Integer\.pretty ~hexa:true)/Integer.pretty_hex/g' \
+   -e 's/Integer\.pretty ~hexa:false/Integer.pretty/g' \
+   -e 's/Integer\.pretty ~hexa:true/Integer.pretty_hex/g' \
+   # this line left empty on purpose
+}
+
+apply_one_dir ()
+{
+  if [ "$VERBOSE" ]; then
+    echo "Processing directory `pwd`"
+  fi
+  for f in $(find . -maxdepth 1 -type f -name "*.ml*" 2> /dev/null); do
+    process_file "$f"
+  done
+}
+
+apply_recursively ()
+{
+    apply_one_dir
+    while IFS= read -r -d $'\0' d; do
+        if [ "$d" = "." ]; then
+            continue
+        fi
+        safe_goto "$d" .. apply_recursively
+    done < <(find . -maxdepth 1 -type d -print0)
+}
+
+applying_to_list ()
+{
+  dirs
+  tmpdir=`pwd`
+  for d in $DIR; do
+    goto "$d" "$tmpdir" "$1"
+  done
+}
+
+help ()
+{
+  echo "Usage: $0 [options | directories]
+
+Options are:
+  -r | --recursive       Check subdirectories recursively
+  -h | --help            Display help message
+  -q | --quiet           Quiet mode (i.e. non-verbose mode)
+  -v | --verbose         Verbose mode (default)"
+  exit 0
+}
+
+error ()
+{
+  echo "$1.
+Do \"$0 -h\" for help."
+  exit 1
+}
+
+FN="apply_one_dir"
+
+parse_arg ()
+{
+  case $1 in
+    -r | --recursive)     FN="apply_recursively";;
+    -h | -help      )     help; exit 0;;
+    -q | --quiet    )     VERBOSE=;;
+    -v | --verbose  )     VERBOSE="v";;
+    -* )                  error "Invalid option $1";;
+    * )                   DIR="$DIR $1";;
+  esac
+}
+
+cmd_line ()
+{
+  for s in "$@"; do
+    parse_arg "$s"
+  done
+  applying_to_list $FN
+}
+
+cmd_line "$@"
+exit 0

devel_tools/docker/Makefile

@@ -114,6 +114,62 @@ sed 's|@FRAMAC_TESTS@|sudo apk add ncurses \&\& cd /frama-c \&\& make tests PTES
 sed 's|@OCAMLV@|4.08|g' | \
 cat > $@
 
+24.0-stripped: Dockerfile.24.0
+	docker build . -t framac/frama-c:$@ --target frama-c-stripped -f $^ \
+--build-arg=from_archive=https://www.frama-c.com/download/frama-c-24.0-Chromium.tar.gz $(ARGS)
+TARGETS += 24.0-stripped
+
+24.0: Dockerfile.24.0
+	docker build . -t framac/frama-c:$@ --target frama-c-slim -f $^ \
+--build-arg=from_archive=https://www.frama-c.com/download/frama-c-24.0-Chromium.tar.gz $(ARGS)
+TARGETS += 24.0
+
+24.0-gui: Dockerfile.24.0
+	docker build . -t framac/frama-c-gui:24.0 --target frama-c-gui-slim -f $^ \
+--build-arg=from_archive=https://www.frama-c.com/download/frama-c-24.0-Chromium.tar.gz $(ARGS)
+TARGETS += 24.0-gui
+
+push-24.0: 24.0 24.0-gui 24.0-stripped
+	docker push framac/frama-c:24.0
+	docker push framac/frama-c-gui:24.0
+	docker push framac/frama-c:24.0-stripped
+
+# Note: alpine-3.14 has Z3 version 4.8.11, which is not supported in some
+# versions of Why3, so we remain with alpine-3.13 for now.
+Dockerfile.24.0: Makefile Dockerfile.template env.template
+	sed 's|@ALPINE_OPAM_BASE@|ocaml/opam:alpine-3.13-ocaml-4.08|g' Dockerfile.template | \
+sed 's|@ALPINE_BASE@|alpine:3.13|g' | \
+sed 's|@ENV@|$(shell cat env.template)|g' | \
+sed 's|@CVC4@|$(shell cat cvc4.template)|g' | \
+sed 's|@CVC4_VERSION@|1.7|g' | \
+sed 's|@Z3@|$(shell cat z3.template)|g' | \
+sed 's|@OPAM_CACHE_FIX@|opam repository set-url default https://opam.ocaml.org \&\&|g' | \
+sed 's|@OPAM_SWITCH@|true|g' | \
+sed 's|@OPAM_DEPS@|\\\
+alt-ergo.2.2.0 \\\
+apron.v0.9.12 \\\
+conf-graphviz.0.1 \\\
+mlgmpidl.1.2.12 \\\
+ocamlfind.1.8.1 \\\
+ocamlgraph.1.8.8 \\\
+ppx_deriving_yojson.3.5.2 \\\
+why3.1.4.0 \\\
+yojson.1.7.0 \\\
+zarith.1.9.1 \\\
+zmq.5.1.3 \\\
+conf-python-3.1.0.0 \\\
+conf-time.1|' | \
+sed 's|@PATCH_FRAMAC@|true|g' | \
+sed 's|@WP_REPORT@|-wp -report|g'| \
+sed 's|@WHY3_CONFIG@|why3 config detect|g' | \
+sed 's|@WP_TEST@|frama-c -wp wp_gallery/binary-multiplication-without-overflow.c -wp-prover alt-ergo,cvc4,z3|g' | \
+sed 's|@GUI_ALPINE_DEPS@||g' | \
+sed 's|@GUI_OPAM_DEPS@|lablgtk3 lablgtk3-sourceview3 conf-gtksourceview3|g' | \
+sed 's|@GUI_REMAKE@|make clean \&\& ./configure --enable-gui \&\& make -j \&\& sudo make install|g' | \
+sed 's|@FRAMAC_TESTS@|sudo apk add ncurses \&\& cd /frama-c \&\& make tests PTESTS_OPTS=-error-code|g' | \
+sed 's|@OCAMLV@|4.08|g' | \
+cat > $@
+
 23.1-stripped: Dockerfile.23.1
 	docker build . -t framac/frama-c:$@ --target frama-c-stripped -f $^ \
 --build-arg=from_archive=https://www.frama-c.com/download/frama-c-23.1-Vanadium.tar.gz $(ARGS)

devel_tools/docker/README.md

@@ -14,8 +14,8 @@ Frama-C versions. For each version, there are three images: one
 for the command-line version `frama-c`; a stripped-down version of the former,
 for a slimmer image, but which does not allow recompilation of Frama-C
 or of any external plugin; and a third image including the graphical
-interface (`frama-c-gui`), to be used with Singularity or other tools enabling
-graphical interfaces from within a Docker image.
+interface (`frama-c-gui`), to be used with Singularity, x11docker, or any other
+tool which enables running a graphical application from a Docker image.
 
 Run `make` to get a list of targets.
 
@@ -29,6 +29,14 @@ Some commands in this section are those used by the above Makefile;
 others allow creating different images (e.g. with the Frama-C sources)
 which are not directly available as Makefile targets.
 
+Note: a Dockerfile is needed for the commands below.
+      For most versions, running `make Dockerfile.dev` and then using it
+      (adding `-f Dockerfile.dev` to the commands below) is enough.
+      However, if specific build commands or dependencies are needed,
+      you can copy the generated Dockerfile
+      (e.g. `cp Dockerfile.dev Dockerfile`) and adapt it as needed,
+      before running one of the commands below.
+
 - Build slim development image (from public Git master branch):
 
         docker build . -t framac/frama-c:dev --target frama-c-slim

doc/LICENSE

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

doc/build-manuals.sh

@@ -42,6 +42,8 @@ mkdir -p manuals
 FC_SUFFIX=$(cat ../VERSION)-$(cat ../VERSION_CODENAME)
 FC_SUFFIX="$(echo ${FC_SUFFIX} | sed -e "s/~/-/")"
 ACSL_SUFFIX=$(grep acslversion acsl/version.tex | sed 's/.*{\([^{}\\]*\).*/\1/')
+FC_VERSION=$(cat ../VERSION)
+ACSL_IMPLEM_VERSION=$(grep fcversion acsl/version.tex | sed 's/.*{\([^{}\\]*\).*/\1/')
 EACSL_SUFFIX=$(grep 'newcommand{\\eacsllangversion' ../src/plugins/e-acsl/doc/refman/main.tex | sed 's/.*{\([^{}\\]*\).*/\1/')
 # sanity check
 if [ "$EACSL_SUFFIX" = "" ]; then
@@ -97,3 +99,6 @@ $EACSL_DOC/refman/e-acsl.pdf,e-acsl.pdf,$EACSL_SUFFIX
 if [ "$ACSL_SUFFIX" != "$EACSL_SUFFIX" ]; then
     echo "WARNING: different versions for ACSL and E-ACSL manuals: $ACSL_SUFFIX versus $EACSL_SUFFIX"
 fi
+if [ "$ACSL_IMPLEM_VERSION" != "$FC_VERSION" ]; then
+    echo "WARNING: ACSL implementation refers to a different Frama-C version: $ACSL_IMPLEM_VERSION versus $FC_VERSION"
+fi

doc/code/toc_tail.htm

@@ -22,8 +22,8 @@
 
 </ul>
 <div class="copyright">
-<a href="http://frama-c.com">frama-c.com</a><br>
-&copy; 2007-2020 CEA-LIST
+<a href="https://frama-c.com">frama-c.com</a><br>
+&copy; 2007-2021 CEA-LIST
 </div>
 </body>
 </html>

doc/developer/Makefile

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

doc/developer/check_api/Makefile

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

doc/developer/check_api/check_and_compare.ml

@@ -2,7 +2,7 @@
 (*                                                                        *)
 (*  This file is part of Frama-C.                                         *)
 (*                                                                        *)
-(*  Copyright (C) 2007-2020                                               *)
+(*  Copyright (C) 2007-2021                                               *)
 (*    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-2020                                               *)
+(*  Copyright (C) 2007-2021                                               *)
 (*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
 (*         alternatives)                                                  *)
 (*                                                                        *)

doc/developer/check_api/check_index_grammar.mly

@@ -2,7 +2,7 @@
 /*                                                                        */
 /*  This file is part of Frama-C.                                         */
 /*                                                                        */
-/*  Copyright (C) 2007-2020                                               */
+/*  Copyright (C) 2007-2021                                               */
 /*    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-2020                                               *)
+(*  Copyright (C) 2007-2021                                               *)
 (*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
 (*         alternatives)                                                  *)
 (*                                                                        *)

doc/developer/examples/callstack.ml

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

doc/developer/examples/syntactic_check.ml

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

doc/developer/examples/use_callstack.ml

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

doc/developer/tutorial/hello/Makefile

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