Commits (205)
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
......
......@@ -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)
###################################
......
24.0-beta+dev
24.0+dev
......@@ -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/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
......@@ -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)
......
......@@ -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
......
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
......
......@@ -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
......@@ -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>
......@@ -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) #
# #
......
......@@ -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) #
# #
......
......@@ -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) *)
(* *)
......
......@@ -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) *)
(* *)
......
......@@ -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) */
/* */
......
......@@ -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) *)
(* *)
......
......@@ -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) *)
(* *)
......
......@@ -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) *)
(* *)
......
......@@ -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) *)
(* *)
......
......@@ -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) #
# #
......