diff --git a/bin/build-src-distrib.sh b/bin/build-src-distrib.sh
deleted file mode 100755
index c4b43f1b3eb991cb8fe19c64be41c21770f3a785..0000000000000000000000000000000000000000
--- a/bin/build-src-distrib.sh
+++ /dev/null
@@ -1,837 +0,0 @@
-#! /usr/bin/env bash
-##########################################################################
-# #
-# This file is part of Frama-C. #
-# #
-# Copyright (C) 2007-2024 #
-# 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). #
-# #
-##########################################################################
-
-set -u
-
-# Search "BEGIN SCRIPT" to skip functions
-
-# Set it to "no" in order to really execute the commands.
-# Otherwise, they are only printed.
-DEBUG=no
-
-# Set variable VERBOSE_MAKE_DOC to see all latex messages during manuals build
-
-# Executing this script requires bash 4.0 or higher
-# (special use of the 'case' construct)
-if test `echo $BASH_VERSION | sed "s/\([0-9]\).*/\1/" ` -lt 4; then
- echo "bash version >= 4 is required."
- exit 127
-fi
-
-# git-lfs needs to be installed
-if ! command -v git-lfs >/dev/null 2>/dev/null; then
- echo "git-lfs is required"
- exit 127
-fi
-
-# grep needs to be installed
-if ! command -v grep --version >/dev/null 2>/dev/null; then
- echo "grep is required"
- exit 127
-fi
-
-function run {
- cmd=$1
- echo "$cmd"
- if test "$DEBUG" == "no"; then
- sh -c "$cmd" || { echo "Aborting step ${STEP}."; exit "${STEP}"; }
- fi
-}
-
-function step {
- STEP=$1
- echo
- echo "Step $1: $2"
-}
-
-# find_repository_DIRECTORY_BRANCH path url
-# - path: path to the directory
-# - url: URL of the repository
-# Checks:
-# - master branch
-# Sets:
-# DIRECTORY: path to the directory
-function find_repository_DIRECTORY_BRANCH {
- name=$1
- url=$2
- if test \! -d $name/.git ; then
- echo "### WARNING: $name/.git directory not found; do you want to clone it? (y/n)"
- read CHOICE
- case "${CHOICE}" in
- "Y"|"y")
- run "git clone $url $name"
- ;;
- *)
- echo "The $url repository must be linked at $name (clone or symbolic link)"
- exit 1
- ;&
- esac
- fi
- DIRECTORY=$name
- BRANCH=`git --git-dir=$name/.git rev-parse --abbrev-ref HEAD`
- if [ "$BRANCH" != "master" ]; then
- echo "### WARNING: $name repository is on branch $BRANCH"
- proceed_anyway "Reset the branch to 'master', then run the script again."
- fi
-}
-
-# proceed_anyway message
-# - message: text to display if we have to stop
-# Ask if the user wants to continue and display the message if not (then exit)
-function proceed_anyway {
- message=$1
- echo "Proceed anyway? [y/N]"
- read CHOICE
- case "${CHOICE}" in
- "Y"|"y")
- ;;
- *)
- echo "$message"
- exit 1
- esac
-}
-
-function look_for_uncommited_changes {
- run "git update-index --refresh"
- if ! git diff-index HEAD --; then
- echo ""
- echo "### WARNING: uncommitted git changes will be discarded when creating archive!"
- proceed_anyway "Stash or commit local changes, then run the script again."
- fi
-}
-
-function look_for_frama_c_dev {
- grep -Iir "frama-c+dev" src &> /dev/null
- if [ "$?" == "0" ]; then
- echo "### WARNING: Remaining frama-c+dev occurrences in 'src'"
- proceed_anyway "Update API, then run the script again"
- fi
-}
-
-function assert_build_dir {
- if test \! -d "$BUILD_DIR" ; then
- echo "ERROR: $BUILD_DIR does not exist, possibly removed by another step"
- exit 1
- fi
-}
-
-function assert_out_dir {
- if test \! -d "$OUT_DIR" ; then
- echo "ERROR: $OUT_DIR does not exist, possibly removed by another step"
- exit 1
- fi
-}
-
-# diff_validation repository file
-# - repository: target repository
-# - file: target file
-# Ask for user validation before staging changes in [file] on the [repository].
-# Stops the script if the user refuses the changes
-function diff_validation {
- repo=$1
- file=$2
- run "git -C $repo diff $file"
- echo
- echo "Is the above diff correct for $file? [y/N]"
- read CHOICE
- case "${CHOICE}" in
- "Y"|"y")
- ;;
- *)
- echo "Something went wrong, you may want to clean $repo"
- exit 1
- esac
- run "git -C $repo add $file"
-}
-
-# Manuals choice
-
-function get_MANUAL_NAME {
- case "$1" in
- "user") MANUAL_NAME="Frama-C user manual" ;;
- "plugin-dev") MANUAL_NAME="Frama-C plug-in development guide" ;;
- "api") MANUAL_NAME="Frama-C API bundle" ;;
- "acsl-1") MANUAL_NAME="ACSL manual" ;;
- "acsl-impl") MANUAL_NAME="ACSL implementation" ;;
- "aorai") MANUAL_NAME="Aorai manual" ;;
- "e-acsl-1") MANUAL_NAME="E-ACSL reference" ;;
- "e-acsl-impl") MANUAL_NAME="E-ACSL implementation" ;;
- "e-acsl-man") MANUAL_NAME="E-ACSL manual" ;;
- "eva") MANUAL_NAME="EVA manual" ;;
- "metrics") MANUAL_NAME="Metrics manual" ;;
- "rte") MANUAL_NAME="RTE manual" ;;
- "wp") MANUAL_NAME="WP manual" ;;
- *) MANUAL_NAME="Not a manual identifier: $1" ;;
- esac
-}
-
-function check_manual {
- value=$1
- if [[ ! " ${AVAILABLE_MANUALS[@]} " =~ " ${value} " ]]; then
- echo "### ERROR: in $INCLUDED_MANUALS_CONFIG: $value is not a valid manual identifier"
- exit 1
- fi
-}
-
-function show_generated_manuals {
- echo
- echo "The following manuals will be included."
- for i in ${INCLUDED_MANUALS[@]}; do
- get_MANUAL_NAME $i
- echo "- $MANUAL_NAME"
- done
- echo
-}
-
-function create_manuals_config {
- echo -n > $INCLUDED_MANUALS_CONFIG
- for i in ${AVAILABLE_MANUALS[@]}; do
- get_MANUAL_NAME $i
- echo "Include $MANUAL_NAME? [y/N]"
- read CHOICE
- case "${CHOICE}" in
- "Y"|"y")
- echo $i >> $INCLUDED_MANUALS_CONFIG ;;
- *) ;;
- esac
- done
-}
-
-function check_manual_path_MUST_ADD {
- MUST_ADD="no"
- for i in ${INCLUDED_MANUALS[@]}; do
- if [[ $1 == "$i"* ]]; then
- MUST_ADD="yes"
- fi
- done
-}
-
-# WIKI generation
-
-function fill_wiki {
- PAGE_NAME=Frama-C-${FRAMAC_VERSION_AND_CODENAME}.md
- WIKI_PAGE=$WIKI_DIR/$PAGE_NAME
- run "mkdir -p $WIKI_DIR/manuals"
- run "sed -e '/<!-- LAST RELEASE -->/a\\
-- [${FRAMAC_VERSION} (${FRAMAC_VERSION_CODENAME})](Frama-C-${FRAMAC_VERSION_AND_CODENAME})' -i.bak $WIKI_DIR/Home.md"
- run "rm -f $WIKI_DIR/Home.md.bak"
- if test "$FINAL_RELEASE" = "yes"; then
- release_type="FINAL"
- else
- release_type="BETA"
- fi
- run "sed -e '/<!-- LAST ${release_type} RELEASE -->/a\\
-- [${FRAMAC_VERSION} (${FRAMAC_VERSION_CODENAME})](Frama-C-${FRAMAC_VERSION_AND_CODENAME})' -i.bak $WIKI_DIR/_sidebar.md"
- run "rm -f $WIKI_DIR/_sidebar.md.bak"
- echo "# Frama-C release ${FRAMAC_VERSION} (${FRAMAC_VERSION_CODENAME})" > $WIKI_PAGE
- echo "## Sources" >> $WIKI_PAGE
- run "cp $OUT_DIR/$TARGZ_FILENAME $WIKI_DIR/downloads"
- run "git -C $WIKI_DIR add downloads/$TARGZ_FILENAME"
- echo " - [$TARGZ_FILENAME](downloads/$TARGZ_FILENAME)" >> $WIKI_PAGE
- echo "" >> $WIKI_PAGE
- echo "## Manuals" >> $WIKI_PAGE
- for fpath in $OUT_DIR/manuals/* ; do
- f=$(basename $fpath)
- check_manual_path_MUST_ADD $f
- if [[ $MUST_ADD == "yes" ]]; then
- f_no_ext=${f%.*}
- f_no_pdf_ext="${f%.pdf}"
- echo "- [${f_no_pdf_ext%-${FRAMAC_VERSION_AND_CODENAME}}](manuals/$f)" >> $WIKI_PAGE
- run "cp $fpath $WIKI_DIR/manuals/"
- run "git -C $WIKI_DIR add manuals/$f"
- fi
- done
- echo "" >> $WIKI_PAGE
- echo "## Main changes" >> $WIKI_PAGE
- sed 's/\(\#.*\)/##\1/' $CHANGES >> $WIKI_PAGE
- run "git -C $WIKI_DIR add $PAGE_NAME"
- diff_validation $WIKI_DIR "Home.md"
- diff_validation $WIKI_DIR "_sidebar.md"
-}
-
-# WEBSITE pages generation
-
-function add_install_page {
- INSTALL_WEBPAGE=html/installations/$FRAMAC_VERSION_CODENAME_LOWER.md
- INSTALL_WEBPAGE_PATH=$WEBSITE_DIR/$INSTALL_WEBPAGE
- EXT="$FRAMAC_VERSION_CODENAME (released on $(date +%Y-%m-%d))"
- echo "---" > $INSTALL_WEBPAGE_PATH
- echo "layout: installation_page" >> $INSTALL_WEBPAGE_PATH
- echo "version: $FRAMAC_VERSION_CODENAME_LOWER" >> $INSTALL_WEBPAGE_PATH
- echo "title: Installation instructions for $FRAMAC_VERSION_CODENAME" >> $INSTALL_WEBPAGE_PATH
- echo "---" >> $INSTALL_WEBPAGE_PATH
- echo >> $INSTALL_WEBPAGE_PATH
- cat ./INSTALL.md |\
- sed -e "s/^\(# Installing Frama-C\)$/\1 $EXT/" >> $INSTALL_WEBPAGE_PATH
-
- run "git -C $WEBSITE_DIR add $INSTALL_WEBPAGE"
-}
-
-function add_event_page {
- EVENT_WEBPAGE=_events/framac-$FRAMAC_VERSION_SAFE.md
- EVENT_WEBPAGE_PATH=$WEBSITE_DIR/$EVENT_WEBPAGE
-
- if [ "$VERSION_MINOR" != 0 ]; then
- PREVIOUS=$VERSION_MAJOR
- else
- PREVIOUS=$(( $VERSION_MAJOR-1 ))
- fi
- PREVIOUS_NAME=$(git show $PREVIOUS.0:VERSION_CODENAME)
-
- TEXTUAL_VERSION="Frama-C $FRAMAC_VERSION ($FRAMAC_VERSION_CODENAME)"
- TEXTUAL_PREVIOUS="Frama-C $PREVIOUS ($PREVIOUS_NAME)"
-
- echo "---" > $EVENT_WEBPAGE_PATH
- echo "layout: default" >> $EVENT_WEBPAGE_PATH
- echo "date: $(date +\"%d-%m-%Y\")" >> $EVENT_WEBPAGE_PATH
- echo "short_title: $TEXTUAL_VERSION" >> $EVENT_WEBPAGE_PATH
- echo -n "title: " >> $EVENT_WEBPAGE_PATH
- if [ "$FINAL_RELEASE" = "no" ]; then
- echo -n "Beta release " >> $EVENT_WEBPAGE_PATH
- else
- echo -n "Release " >> $EVENT_WEBPAGE_PATH
- fi
- echo "of $TEXTUAL_VERSION" >> $EVENT_WEBPAGE_PATH
- VERSION_PAGE="/fc-versions/$FRAMAC_VERSION_CODENAME_LOWER.html"
- echo "link: $VERSION_PAGE" >> $EVENT_WEBPAGE_PATH
- echo "---" >> $EVENT_WEBPAGE_PATH
- echo >> $EVENT_WEBPAGE_PATH
- echo "$TEXTUAL_VERSION is out. Download it [here]($VERSION_PAGE)." >> $EVENT_WEBPAGE_PATH
- echo >> $EVENT_WEBPAGE_PATH
- echo "Main changes with respect to $TEXTUAL_PREVIOUS include:" >> $EVENT_WEBPAGE_PATH
- echo >> $EVENT_WEBPAGE_PATH
- sed 's/\(\#.*\)/###\1/' $CHANGES >> $EVENT_WEBPAGE_PATH
-
- run "git -C $WEBSITE_DIR add $EVENT_WEBPAGE"
-}
-
-function add_version_page {
- VERSION_WEBPAGE="_fc-versions/$FRAMAC_VERSION_CODENAME_LOWER.md"
- VERSION_WEBPAGE_PATH=$WEBSITE_DIR/$VERSION_WEBPAGE
- ACSL_VERSION=$(ls $OUT_DIR/manuals | sed -n 's/^acsl-1.\([0-9][0-9]\).pdf/\1/p')
- echo "---" > $VERSION_WEBPAGE_PATH
- echo "layout: version" >> $VERSION_WEBPAGE_PATH
- echo "number: $VERSION_MAJOR" >> $VERSION_WEBPAGE_PATH
- echo "name: $FRAMAC_VERSION_CODENAME" >> $VERSION_WEBPAGE_PATH
- if [ "$FINAL_RELEASE" = "no" ]; then
- echo "beta: true" >> $VERSION_WEBPAGE_PATH
- else
- echo "acsl: $ACSL_VERSION" >> $VERSION_WEBPAGE_PATH
- fi
- echo "releases:" >> $VERSION_WEBPAGE_PATH
- echo " - number: $VERSION_MINOR" >> $VERSION_WEBPAGE_PATH
- echo " categories:" >> $VERSION_WEBPAGE_PATH
- echo " - name: Frama-C v$FRAMAC_VERSION $FRAMAC_VERSION_CODENAME" >> $VERSION_WEBPAGE_PATH
- echo " files:" >> $VERSION_WEBPAGE_PATH
- echo " - name: Source distribution" >> $VERSION_WEBPAGE_PATH
- echo " link: /download/$TARGZ_FILENAME" >> $VERSION_WEBPAGE_PATH
- echo " help: Compilation instructions" >> $VERSION_WEBPAGE_PATH
- echo " help_link: /html/installations/$FRAMAC_VERSION_CODENAME_LOWER.html" >> $VERSION_WEBPAGE_PATH
- check_manual_path_MUST_ADD "user"
- if [[ $MUST_ADD == "yes" ]]; then
- echo " - name: User manual" >> $VERSION_WEBPAGE_PATH
- echo " link: /download/user-manual-$FRAMAC_VERSION_AND_CODENAME.pdf" >> $VERSION_WEBPAGE_PATH
- fi
- check_manual_path_MUST_ADD "plugin-dev"
- if [[ $MUST_ADD == "yes" ]]; then
- echo " - name: Plug-in development guide" >> $VERSION_WEBPAGE_PATH
- echo " link: /download/plugin-development-guide-$FRAMAC_VERSION_AND_CODENAME.pdf" >> $VERSION_WEBPAGE_PATH
- echo " help: Hello plug-in tutorial archive" >> $VERSION_WEBPAGE_PATH
- echo " help_link: /download/hello-$FRAMAC_VERSION_AND_CODENAME.tar.gz" >> $VERSION_WEBPAGE_PATH
- fi
- check_manual_path_MUST_ADD "api"
- if [[ $MUST_ADD == "yes" ]]; then
- echo " - name: API Documentation" >> $VERSION_WEBPAGE_PATH
- echo " link: /download/frama-c-$FRAMAC_VERSION_AND_CODENAME-api.tar.gz" >> $VERSION_WEBPAGE_PATH
- fi
- check_manual_path_MUST_ADD "acsl-impl"
- if [[ $MUST_ADD == "yes" ]]; then
- echo " - name: ACSL 1.$ACSL_VERSION ($FRAMAC_VERSION_CODENAME implementation)" >> $VERSION_WEBPAGE_PATH
- echo " link: /download/acsl-implementation-$FRAMAC_VERSION_AND_CODENAME.pdf" >> $VERSION_WEBPAGE_PATH
- fi
- echo " - name: Plug-in Manuals" >> $VERSION_WEBPAGE_PATH
- echo " sort: true" >> $VERSION_WEBPAGE_PATH
- echo " files:" >> $VERSION_WEBPAGE_PATH
- check_manual_path_MUST_ADD "aorai"
- if [[ $MUST_ADD == "yes" ]]; then
- echo " - name: Aoraï manual" >> $VERSION_WEBPAGE_PATH
- echo " link: /download/aorai-manual-$FRAMAC_VERSION_AND_CODENAME.pdf" >> $VERSION_WEBPAGE_PATH
- echo " help: Aoraï example" >> $VERSION_WEBPAGE_PATH
- echo " help_link: /download/aorai-example-$FRAMAC_VERSION_AND_CODENAME.tar.gz" >> $VERSION_WEBPAGE_PATH
- fi
- check_manual_path_MUST_ADD "metrics"
- if [[ $MUST_ADD == "yes" ]]; then
- echo " - name: Metrics manual" >> $VERSION_WEBPAGE_PATH
- echo " link: /download/metrics-manual-$FRAMAC_VERSION_AND_CODENAME.pdf" >> $VERSION_WEBPAGE_PATH
- fi
- check_manual_path_MUST_ADD "rte"
- if [[ $MUST_ADD == "yes" ]]; then
- echo " - name: Rte manual" >> $VERSION_WEBPAGE_PATH
- echo " link: /download/rte-manual-$FRAMAC_VERSION_AND_CODENAME.pdf" >> $VERSION_WEBPAGE_PATH
- fi
- check_manual_path_MUST_ADD "eva"
- if [[ $MUST_ADD == "yes" ]]; then
- echo " - name: Eva manual" >> $VERSION_WEBPAGE_PATH
- echo " link: /download/eva-manual-$FRAMAC_VERSION_AND_CODENAME.pdf" >> $VERSION_WEBPAGE_PATH
- fi
- check_manual_path_MUST_ADD "wp"
- if [[ $MUST_ADD == "yes" ]]; then
- echo " - name: WP manual" >> $VERSION_WEBPAGE_PATH
- echo " link: /download/wp-manual-$FRAMAC_VERSION_AND_CODENAME.pdf" >> $VERSION_WEBPAGE_PATH
- fi
- check_manual_path_MUST_ADD "e-acsl-man"
- if [[ $MUST_ADD == "yes" ]]; then
- echo " - name: E-ACSL manual" >> $VERSION_WEBPAGE_PATH
- echo " link: /download/e-acsl/e-acsl-manual-$FRAMAC_VERSION_AND_CODENAME.pdf" >> $VERSION_WEBPAGE_PATH
- fi
- echo "---" >> $VERSION_WEBPAGE_PATH
-
- run "git -C $WEBSITE_DIR add $VERSION_WEBPAGE"
-}
-
-function add_downloads {
- DOWNLOAD_DIR="$WEBSITE_DIR/download"
- DOWNLOAD_PATH="download"
- for fpath in $OUT_DIR/manuals/* ; do
- f=$(basename $fpath)
- f_no_ext=${f%.*}
-
- check_manual_path_MUST_ADD $f
- if [[ $MUST_ADD == "yes" ]]; then
- if [[ $f_no_ext =~ ^e-acsl.*$ ]]; then
- BASE="e-acsl/$f"
- else
- BASE="$f"
- fi
-
- if [[ $f_no_ext =~ ^(e-)?acsl-[0-9].[0-9][0-9]$ ]]; then
- REPL=$(echo $BASE | sed -e "s/-[0-9].[0-9][0-9]//")
- elif [[ $f_no_ext =~ ^e-acsl-* ]]; then
- REPL=$(echo $BASE | sed -e "s/-$FRAMAC_VERSION_AND_CODENAME//")
- else
- REPL=$(echo $BASE | sed -e "s/\(.*\)-$FRAMAC_VERSION_AND_CODENAME/frama-c-\1/")
- fi
-
- run "cp $fpath $DOWNLOAD_DIR/$BASE"
- run "git -C $WEBSITE_DIR add $DOWNLOAD_PATH/$BASE"
-
- # we change generic files ONLY for FINAL release
- if test "$FINAL_RELEASE" = "yes"; then
- run "cp $fpath $DOWNLOAD_DIR/$REPL"
- run "git -C $WEBSITE_DIR add $DOWNLOAD_PATH/$REPL"
- fi
- fi
- done
-
- # Particular case for the value analysis manual:
- EVA_FILE="$OUT_DIR/manuals/eva-manual-$FRAMAC_VERSION_AND_CODENAME.pdf"
- VALUE_PATH="$DOWNLOAD_DIR/frama-c-value-analysis.pdf"
- VALUE_GIT_PATH="$DOWNLOAD_PATH/frama-c-value-analysis.pdf"
- # we change generic files ONLY for FINAL release
- if test "$FINAL_RELEASE" = "yes"; then
- run "cp $EVA_FILE $VALUE_PATH"
- run "git -C $WEBSITE_DIR add $VALUE_GIT_PATH"
- fi
-
- # Examples:
- HELLO="hello-$FRAMAC_VERSION_AND_CODENAME.tar.gz"
- check_manual_path_MUST_ADD "plugin-dev"
- if [[ $MUST_ADD == "yes" ]]; then
- run "cp $OUT_DIR/$HELLO $DOWNLOAD_DIR"
- run "git -C $WEBSITE_DIR add $DOWNLOAD_PATH/$HELLO"
- # we change generic files ONLY for FINAL release
- if test "$FINAL_RELEASE" = "yes"; then
- run "cp $OUT_DIR/$HELLO $DOWNLOAD_DIR"
- run "git -C $WEBSITE_DIR add $DOWNLOAD_PATH/hello.tar.gz"
- fi
- fi
-
- # Source distribution:
- run "cp $OUT_DIR/$TARGZ_FILENAME $DOWNLOAD_DIR"
- run "git -C $WEBSITE_DIR add $DOWNLOAD_PATH/$TARGZ_FILENAME"
- if test "$FINAL_RELEASE" = "yes"; then
- run "cp $OUT_DIR/$TARGZ_FILENAME $DOWNLOAD_DIR/frama-c-source-dist.tar.gz"
- run "git -C $WEBSITE_DIR add $DOWNLOAD_PATH/frama-c-source-dist.tar.gz"
- fi
-
- # API
- run "cp $OUT_DIR/frama-c-api.tar.gz $DOWNLOAD_DIR/frama-c-$FRAMAC_VERSION_AND_CODENAME-api.tar.gz"
- run "git -C $WEBSITE_DIR add $DOWNLOAD_PATH/frama-c-$FRAMAC_VERSION_AND_CODENAME-api.tar.gz"
-}
-
-function fill_website {
- add_install_page
- add_event_page
- add_version_page
- add_downloads
-}
-
-# Commit changes
-
-function create_website_branch {
- if test "$FINAL_RELEASE" = "yes"; then
- BRANCH_NAME="release/stable-$FRAMAC_VERSION_SAFE-$FRAMAC_VERSION_CODENAME_LOWER"
- else
- BRANCH_NAME="release/beta-$FRAMAC_VERSION_SAFE-$FRAMAC_VERSION_CODENAME_LOWER"
- fi
- # Chech whether release/<release> exists on the website
- git -C $WEBSITE_DIR show-ref --verify --quiet refs/heads/$BRANCH_NAME
- if [[ "$?" == "0" ]]; then
- echo "### Warning: branch $BRANCH_NAME already exists in $WEBSITE_DIR"
- echo "The script will ERASE this branch"
- proceed_anyway "Rename or erase the branch, then run the script again."
- run "git -C $WEBSITE_DIR checkout master"
- run "git -C $WEBSITE_DIR branch -D $BRANCH_NAME"
- fi
-
- # Set release/<release> and displays changes to be committed
- run "git -C $WEBSITE_DIR checkout --quiet -b $BRANCH_NAME"
- run "git -C $WEBSITE_DIR status"
-
- echo "Commit locally the previous changes on $WEBSITE_DIR:$BRANCH_NAME? [y/N]"
- read CHOICE
- case "${CHOICE}" in
- "Y"|"y")
- ;;
- *)
- echo "Abort website branch creation, reset to master."
- run "git -C $WEBSITE_DIR checkout master"
- exit 1
- esac
- run "git -C $WEBSITE_DIR commit -m \"$FRAMAC_VERSION_SAFE-$FRAMAC_VERSION_CODENAME release\""
-}
-
-function commit_wiki {
- run "git -C $WIKI_DIR status"
-
- echo "Commit locally the previous changes on $WIKI_DIR? [y/N]"
- read CHOICE
- case "${CHOICE}" in
- "Y"|"y")
- ;;
- *)
- echo "Abort wiki update."
- exit 1
- esac
- run "git -C $WIKI_DIR commit -m \"$FRAMAC_VERSION_SAFE-$FRAMAC_VERSION_CODENAME release\""
-}
-
-
-function propagate_changes {
- create_website_branch
- commit_wiki
-}
-
-function last_step_validation {
- # if test "$FRAMAC_VERSION" != "$FRAMAC_TAG"; then
- # echo "To go further, the last commit must be tagged with the right version"
- # exit 1
- # fi
- echo "
- This step will:
-
- - ask for a validation of the changes to website
- - create a NEW local branch for the website
-
- - ask for a validation of the changes to wiki
- - commit changes to the wiki MASTER local branch
-
- If you want to perform some additional checks it is probably time to stop.
-
- Generated files are available in: $OUT_DIR.
- "
- echo -n "If you are ready to continue, type exactly \"RELEASE\": "
- read CHOICE
- case "${CHOICE}" in
- "RELEASE")
- ;;
- *)
- echo "Aborting"
- exit 1
- esac
-}
-
-
-# BEGIN SCRIPT
-GITLAB_FRAMA_C_PUBLIC="git@git.frama-c.com:pub"
-GITLAB_WIKI="$GITLAB_FRAMA_C_PUBLIC/frama-c.wiki.git"
-GITLAB_WEBSITE="$GITLAB_FRAMA_C_PUBLIC/pub.frama-c.com.git"
-GITLAB_ACSL="git@github.com:acsl-language/acsl.git"
-GITLAB_FRAMA_C_PRIVATE="git@git.frama-c.com:frama-c/frama-c.git"
-
-if test \! -e .git ; then
- echo "ERROR: .git directory not found"
- echo "This script must be run at the root of a Frama-C repository"
- exit 1
-fi
-FRAMAC_BRANCH=`git --git-dir=.git rev-parse --abbrev-ref HEAD`
-
-if test \! -f VERSION ; then
- echo "ERROR: VERSION file not found"
- echo "This script must be run at the root of a Frama-C repository"
- exit 1
-fi
-
-FRAMAC_VERSION=$(cat VERSION)
-FRAMAC_VERSION_SAFE="$(echo ${FRAMAC_VERSION} | sed -e "s/~/-/")"
-FRAMAC_TAG=$(git describe --tag)
-FRAMAC_VERSION_CODENAME=$(cat VERSION_CODENAME)
-FRAMAC_VERSION_CODENAME_LOWER=$(echo "$FRAMAC_VERSION_CODENAME" | tr '[:upper:]' '[:lower:]')
-FRAMAC_VERSION_AND_CODENAME="${FRAMAC_VERSION_SAFE}-${FRAMAC_VERSION_CODENAME}"
-TARGZ_FILENAME=frama-c-${FRAMAC_VERSION_AND_CODENAME}.tar.gz
-
-VERSION_MODIFIER=$(cat VERSION | sed -e s/[0-9.]*\\\(.*\\\)/\\1/)
-VERSION_MAJOR=$(cat VERSION | sed -e s/\\\([0-9]*\\\).[0-9]*.*/\\1/)
-VERSION_MINOR=$(cat VERSION | sed -e s/[0-9]*.\\\([0-9]*\\\).*/\\1/)
-
-if test -n "$VERSION_MODIFIER"; then FINAL_RELEASE=no; else FINAL_RELEASE=yes; fi
-if [ "$VERSION_MODIFIER" == "+dev" ]; then
- echo "### WARNING: The VERSION is a development version"
- proceed_anyway "Update VERSION and run the script again"
-fi
-
-if test "$FRAMAC_VERSION_SAFE" != "$FRAMAC_TAG"; then
- echo "### WARNING: The current commit is not tagged with the current version:"
- echo "Frama-C Version: $FRAMAC_VERSION"
- echo "Frama-C Tag : $FRAMAC_TAG"
-fi
-
-# Find specific repositories
-
-find_repository_DIRECTORY_BRANCH "./frama-c.wiki" $GITLAB_WIKI
-WIKI_DIR=$DIRECTORY
-WIKI_BRANCH=$BRANCH
-
-find_repository_DIRECTORY_BRANCH "./website" $GITLAB_WEBSITE
-WEBSITE_DIR=$DIRECTORY
-WEBSITE_BRANCH=$BRANCH
-
-find_repository_DIRECTORY_BRANCH "./doc/acsl" $GITLAB_ACSL
-ACSL_DIR=$DIRECTORY
-
-CHANGES="./main_changes.md"
-if test \! -f $CHANGES ; then
- echo "### WARNING: The $CHANGES file is missing"
- echo "Do you want to create an empty one? [y/N]"
- read CHOICE
- case "${CHOICE}" in
- "Y"|"y")
- touch $CHANGES;;
- *)
- echo "Create a changes file and run the script again"
- exit 1
- esac
-fi
-
-AVAILABLE_MANUALS=("user" "api" "plugin-dev" "acsl-1" "acsl-impl" "aorai" "e-acsl-1" "e-acsl-man" "e-acsl-impl" "eva" "metrics" "rte" "wp")
-INCLUDED_MANUALS_CONFIG="./included_manuals"
-INCLUDED_MANUALS=()
-
-if test "$FINAL_RELEASE" = "yes"; then
- # In final release mode, all manuals must be distributed
- for i in ${AVAILABLE_MANUALS[@]}; do
- INCLUDED_MANUALS+=($i)
- done
-else
- if test \! -f $INCLUDED_MANUALS_CONFIG ; then
- echo "### WARNING: The $INCLUDED_MANUALS_CONFIG file is missing"
- echo "Do you want to create one? [y/N]"
- read CHOICE
- case "${CHOICE}" in
- "Y"|"y")
- create_manuals_config
- for i in $(cat $INCLUDED_MANUALS_CONFIG); do
- check_manual $i
- INCLUDED_MANUALS+=($i)
- done
- ;;
- *)
- echo "NO manuals will be included"
- ;;
- esac
- else
- for i in $(cat $INCLUDED_MANUALS_CONFIG); do
- check_manual $i
- INCLUDED_MANUALS+=($i)
- done
- fi
-fi
-
-MANUALS_DIR="./doc/manuals"
-
-FILTER=""
-if [ -z ${VERBOSE_MAKE_DOC+x} ]; then
- if command -v texfot --version >/dev/null 2>/dev/null; then
- FILTER="texfot --ignore '(Warning|Overfull|Underfull|Version)'"
- fi
-fi
-
-BUILD_DIR_ROOT="/tmp/release"
-BUILD_DIR="$BUILD_DIR_ROOT/frama-c"
-
-OUT_DIR="./distributed"
-
-echo "############################# Frama-C Info ##############################"
-echo ""
-echo "Frama-C Version : $FRAMAC_VERSION"
-echo "Final release : $FINAL_RELEASE"
-echo "Frama-C Branch : $FRAMAC_BRANCH"
-echo "Frama-C Wiki Dir : $WIKI_DIR"
-echo "Website Dir : $WEBSITE_DIR"
-echo "Changes file : $CHANGES"
-echo "Build Dir : $BUILD_DIR"
-echo "Output Dir : $OUT_DIR"
-echo ""
-echo "############################# Manuals ##############################"
-echo ""
-echo "Manuals Dir : $MANUALS_DIR"
-echo "ACSL Dir : $ACSL_DIR"
-show_generated_manuals
-
-echo "#########################################################################"
-
-export LC_CTYPE=en_US.UTF-8
-
-echo -n "
-Steps are:
-
- N) previous information is wrong, STOP the script
- 0) ERASE $OUT_DIR
- 1) compile PDF manuals (will ERASE $MANUALS_DIR!)
- 2) build the source distribution
- 3) build API bundle
- 4) build documentation companions
- 5) clean $BUILD_DIR
- 6) prepare wiki (will RESET HARD $WIKI_DIR:$WIKI_BRANCH)
- 7) prepare website (will RESET HARD $WEBSITE_DIR:$WEBSITE_BRANCH)
- 8) check generated distribution
- 9) generate opam file
- 10) commit changes
-
-Start at which step? (default is N, which cancels everything)
-- If this is the first time running this script, start at 0
-- Otherwise, start at the latest step before failure
-"
-read STEP
-
-case "${STEP}" in
- ""|"N")
- echo "Exiting without doing anything.";
- exit 0;
- ;&
- 0)
- step 0 "PREPARE DISTRIBUTION DIRECTORY"
- run "rm -rf $OUT_DIR"
- run "mkdir -p $OUT_DIR"
- ;&
-
- 1)
- step 1 "COMPILING PDF MANUALS"
- run "rm -rf $MANUALS_DIR"
- run "mkdir -p $MANUALS_DIR"
- run "$FILTER make -C doc all"
- run "rm -rf $OUT_DIR/manuals"
- run "mkdir -p $OUT_DIR/manuals"
- run "cp $MANUALS_DIR/* $OUT_DIR/manuals"
- ;&
- 2)
- step 2 "BUILDING THE SOURCE DISTRIBUTION"
- look_for_uncommited_changes
- look_for_frama_c_dev
- run "mkdir -p $BUILD_DIR_ROOT"
- run "rm -rf $BUILD_DIR"
- run "git worktree add -f --detach $BUILD_DIR $FRAMAC_BRANCH"
- run "cd $BUILD_DIR; autoconf"
- run "cd $BUILD_DIR; ./configure"
- run "cd $BUILD_DIR; make -j OPEN_SOURCE=yes DISTRIB=frama-c-${FRAMAC_VERSION_AND_CODENAME} src-distrib"
- # sanity check: markdown-report must be distributed
- run "tar tf $BUILD_DIR/$TARGZ_FILENAME | grep -q src/plugins/markdown-report"
- run "cp $BUILD_DIR/$TARGZ_FILENAME $OUT_DIR"
- ;&
- 3)
- step 3 "BUILDING THE API BUNDLE"
- assert_build_dir
- run "cd $BUILD_DIR; make -j doc-distrib"
- run "cp $BUILD_DIR/frama-c-api.tar.gz $OUT_DIR"
- ;&
- 4)
- step 4 "BUILDING THE DOCUMENTATION COMPANIONS"
- assert_build_dir
- run "cd $BUILD_DIR; make -j doc-companions"
- run "cp $BUILD_DIR/hello-${FRAMAC_VERSION_AND_CODENAME}.tar.gz $OUT_DIR"
- ;&
- 5)
- step 5 "CLEAN $BUILD_DIR"
- run "rm -rf $BUILD_DIR"
- run "git worktree prune"
- ;&
- 6)
- step 6 "PREPARE WIKI"
- assert_out_dir
- run "git -C $WIKI_DIR checkout master"
- run "git -C $WIKI_DIR fetch origin"
- run "git -C $WIKI_DIR reset --hard origin/master"
- fill_wiki
- ;&
- 7)
- step 7 "PREPARE WEBSITE"
- assert_out_dir
- run "git -C $WEBSITE_DIR checkout master"
- run "git -C $WEBSITE_DIR fetch origin"
- run "git -C $WEBSITE_DIR reset --hard origin/master"
- fill_website
- ;&
- 8)
- step 8 "CHECK GENERATED DISTRIBUTION"
- assert_out_dir
- TEST_DIR="$BUILD_DIR_ROOT/frama-c-${FRAMAC_VERSION_AND_CODENAME}"
- run "mkdir -p $BUILD_DIR_ROOT"
- run "rm -rf $TEST_DIR"
- run "cp $OUT_DIR/$TARGZ_FILENAME $BUILD_DIR_ROOT"
- run "cd $BUILD_DIR_ROOT ; tar xzf $TARGZ_FILENAME"
- run "./doc/release/checktar.sh $TEST_DIR"
- run "cd $TEST_DIR ; ./configure && make -j && make tests PTESTS_OPTS=\"-error-code\""
- run "rm -rf $TEST_DIR"
- ;&
- 9)
- step 9 "GENERATE OPAM FILE"
- assert_out_dir
- cat opam | grep -v "^version\:" | grep -v "^name\:" > $OUT_DIR/opam
- echo >> "$OUT_DIR/opam"
- echo "url {" >> "$OUT_DIR/opam"
- echo " src: \"https://git.frama-c.com/pub/frama-c/-/wikis/downloads/$TARGZ_FILENAME\"" >> "$OUT_DIR/opam"
- echo " checksum: \"sha256=$(sha256sum $OUT_DIR/$TARGZ_FILENAME | cut -d" " -f1)\"" >> "$OUT_DIR/opam"
- echo "}" >> "$OUT_DIR/opam"
- ;&
- 10)
- step 10 "COMMIT CHANGES"
- last_step_validation
- propagate_changes
- ;;
- *)
- echo "Bad entry: ${STEP}"
- echo "Exiting without doing anything.";
- exit 31
-esac
-
-exit 0
diff --git a/bin/frama-c-build-scripts.sh b/bin/frama-c-build-scripts.sh
deleted file mode 100755
index a73efcce1156e04b6e39a14308b09ca128fa9582..0000000000000000000000000000000000000000
--- a/bin/frama-c-build-scripts.sh
+++ /dev/null
@@ -1,194 +0,0 @@
-#!/bin/bash
-##########################################################################
-# #
-# This file is part of Frama-C. #
-# #
-# Copyright (C) 2007-2024 #
-# 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). #
-# #
-##########################################################################
-
-PACKAGE="frama-c-scripts"
-
-CMD="init"
-
-THIS_SCRIPT="$0"
-Usage () {
- echo "Usage: $(basename ${THIS_SCRIPT}) [<command>] [options] <script-dir> [<modules>]"
- echo " Builds a script library to be used by the Frama-C kernel."
- echo ""
- echo "Commands:"
- echo "- init: generates dune files (default command)"
- echo "- build: performs the compilation of the script libraries via \"dune build @install\""
- echo "- install: performs the installation of the script libraries via \"dune install\""
- echo ""
- echo "Options:"
- echo " -help: prints usage information"
- echo " -package-name <name>: sets the <name> of the package of the libraries (defaults to \"${PACKAGE}\")."
- echo " note: once the dune-project file has been created, don't set another name."
- echo ""
- echo "Arguments:"
- echo " <script-dir>: directory that contains the script files:"
- echo " - the basename of this directory fixes the name of the script library: ${PACKAGE}.<basename>"
- echo " - a 'dune' file is created (if it does not exist) in this directory"
- echo " - a 'dune-project' file is created (if it does not exist) in the parent directory"
- echo " - note: the parent directory is './' when the script directory is also './'"
- echo " <modules>: names of the OCaml modules that compose the script (defaults to all OCaml modules of the script directory)"
-}
-
-Error () {
- echo "Error: $@"
- Usage
- exit 1
-}
-
-###############
-# Command line processing
-
-case "$1" in
- "init"|"build"|"install") CMD="$1"; shift;;
- *) ;;
-esac
-
-while [ "$1" != "" ]; do
- case "$1" in
- "-package-name") shift ; PACKAGE="$1";;
- "-h"|"-help"|"--help") Usage; exit 0;;
- *) break ;;
- esac
- shift
-done
-
-[ "$PACKAGE" != "" ] || Error "missing option value: package name"
-[ "$1" != "" ] || Error "missing argument: script directory"
-
-SCRIPT_DIR="$1"
-shift
-SCRIPT_FILES="$@"
-SCRIPT_LIBS=""
-
-[ -d "${SCRIPT_DIR}" ] || Error "Script directory does not exist: ${SCRIPT_DIR})"
-
-###############
-
-DuneProject () {
- echo "(lang dune 3.13)"
- echo "(generate_opam_files true)"
- echo "(name ${PACKAGE})"
- echo "(maintainers \"anonymous\")"
- echo "(package (name ${PACKAGE})"
- echo " (depends"
- echo " (\"frama-c\" (>= 28.1))"
- echo " )"
- echo " (tags (\"Frama-C scripts\"))"
- echo ")"
-}
-
-Dune () {
- echo "(rule"
- echo " (alias ${PACKAGE})"
- echo " (deps (universe))"
- echo " (action (echo \"- Script ${SCRIPT_NAME}:\" %{lib-available:${PACKAGE}.${SCRIPT_NAME}} \"\\\\n\"))"
- echo ")"
- echo ""
- echo "(library"
- echo " (name ${SCRIPT_NAME})"
- echo " (optional)"
- echo " (public_name ${PACKAGE}.${SCRIPT_NAME})"
- [ "${SCRIPT_FILES}" = "" ] || echo " (modules ${SCRIPT_FILES})"
- echo " (flags -open Frama_c_kernel :standard -w -9)"
- echo " (libraries frama-c.kernel ${SCRIPT_LIBS})"
- echo ")"
-}
-
-###############
-
-GenerateFile () {
- if [ -e "$2" ]; then
- echo "$1 file already exists: $2"
- else
- echo "- Creating $1 file: $2"
- $1 | while read p; do
- echo "$p" >> "$2"
- done
- fi
-}
-
-###############
-
-SCRIPT_NAME="$(basename "${SCRIPT_DIR}")"
-DUNE_PROJECT_DIR="$(dirname "${SCRIPT_DIR}")"
-DUNE_PROJECT="${DUNE_PROJECT_DIR}/dune-project"
-case "${SCRIPT_DIR}" in
- */) DUNE_FILE="${SCRIPT_DIR}dune" ;;
- *) DUNE_FILE="${SCRIPT_DIR}/dune" ;;
-esac
-
-###############
-
-EchoDuneCmd() {
- if [ "${DUNE_PROJECT_DIR}" = "." ]; then
- echo " > $@"
- else
- echo " > (cd ${DUNE_PROJECT_DIR} && $@)"
- fi
-}
-
-DuneBuild() {
- echo ""
- echo "- Compiling the script library \"${PACKAGE}.${SCRIPT_NAME}\" via \"dune build @install\" command..."
- dune build @install
- [ "$?" = "0" ] || Error "compilation failure"
-}
-
-DuneInstall() {
- echo ""
- echo "- Install the script library \"${PACKAGE}.${SCRIPT_NAME}\" via \"dune install\" command..."
- dune install
-}
-
-###############
-
-[ "$(basename "${DUNE_FILE}")" = "dune" ] || Error "Wrong basename for a dune file: ${DUNE_FILE}"
-[ "$(basename "${DUNE_PROJECT}")" = "dune-project" ] || Error "Wrong basename for a dune-project file: ${DUNE_PROJECT}"
-
-GenerateFile DuneProject "${DUNE_PROJECT}"
-GenerateFile Dune "${DUNE_FILE}"
-
-if [ "$CMD" = "init" ]; then
- echo ""
- echo "To compile all scripts defined inside this 'dune project' \"${PACKAGE}\", run:"
- EchoDuneCmd "dune build @install"
-else
- DuneBuild
-fi
-echo ""
-echo "Script libraries have been compiled and installed into the local '_build' directory."
-echo "An 'opam' file \"${PACKAGE}.opam\" has been created/updated, allowing a global installation of all script libraries."
-echo ""
-echo "To load this script library from Frama-C, run the following command:"
-EchoDuneCmd "dune exec -- frama-c -load-library ${PACKAGE}.${SCRIPT_NAME} ..."
-
-if [ "$CMD" = "install" ]; then
- DuneInstall
-else
- echo ""
- echo "All libraries of this 'dune project' \"${PACKAGE}\" can also be installed via 'dune' using from the generated 'opam' file: \"${PACKAGE}.opam\""
- EchoDuneCmd "dune install"
-fi
-echo ""
-echo "After installation, this script library can be directly loaded by Frama-C with:"
-echo " > frama-c -load-library ${PACKAGE}.${SCRIPT_NAME} ..."
diff --git a/bin/indent.sh b/bin/indent.sh
deleted file mode 100755
index ddd1f05cf9cde5bb86f1c93a136de2cbab07110a..0000000000000000000000000000000000000000
--- a/bin/indent.sh
+++ /dev/null
@@ -1,57 +0,0 @@
-##########################################################################
-# #
-# This file is part of Frama-C. #
-# #
-# Copyright (C) 2007-2024 #
-# 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). #
-# #
-##########################################################################
-
-# Help
-
-case "$1" in
- "-h"|"--help")
- echo "indent [-h|--help] [DIR|FILE]"
- echo ""
- echo " Re-indent and remove trailing spaces in OCaml sources."
- echo " By default, find sources in '.', but can be applied on a"
- echo " directory or on a single file."
- echo ""
- echo " Only applies to writable '*.ml' and '*.mli' files."
- exit 0 ;;
-esac
-
-# Root file or directory
-
-ROOT="."
-if [ "$1" != "" ]
-then
- ROOT="$1"
-fi
-
-# re-indent and de-spacify all files
-
-for file in $(find $ROOT \( -name "*.ml" -or -name "*.mli" \) -perm -u+w); do
- if file $file | grep -wq "ISO-8859"; then
- echo "Convert $file";
- iconv -f ISO-8859-1 -t UTF-8 $file > $file.tmp;
- mv $file.tmp $file;
- fi;
- echo "Indent $file"
- sed -e's/[[:space:]]*$//' $file > $file.tmp;
- mv $file.tmp $file;
- ocp-indent -i $file;
-done
diff --git a/bin/merge-master.sh b/bin/merge-master.sh
deleted file mode 100755
index 3b46ad97dec09f0b7f13f47e55dd719bb78eb40f..0000000000000000000000000000000000000000
--- a/bin/merge-master.sh
+++ /dev/null
@@ -1,40 +0,0 @@
-#!/bin/sh
-##########################################################################
-# #
-# This file is part of Frama-C. #
-# #
-# Copyright (C) 2007-2024 #
-# 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). #
-# #
-##########################################################################
-
-if test -z "$1"; then
- echo "Syntax: $0 <release name>";
- exit 1
-fi
-
-# Name of the release branch to merge in master
-BRANCH="stable/$1"
-
-# Last merge commit between master and the release
-ANCESTOR=$(git merge-base $BRANCH master)
-
-# Find Gitlab text ('See merge request') and extract merge numbers
-MR=$(git log --format='%b' --merges $ANCESTOR..$BRANCH \
- | sed -n 's/See merge request \(![0-9]*\)/\1/p' \
- | tr '\n' ' ' )
-
-git merge $BRANCH -m "Merging $BRANCH into master ($MR)"
diff --git a/bin/rebuild.sh b/bin/rebuild.sh
deleted file mode 100755
index 299572f98adb2efb74022d2cb84572360d0cbc6b..0000000000000000000000000000000000000000
--- a/bin/rebuild.sh
+++ /dev/null
@@ -1,24 +0,0 @@
-#!/bin/sh
-##########################################################################
-# #
-# This file is part of Frama-C. #
-# #
-# Copyright (C) 2007-2024 #
-# 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). #
-# #
-##########################################################################
-
-make -k clean && make -k
diff --git a/bin/sed_get_binutils_version b/bin/sed_get_binutils_version
deleted file mode 100644
index ba83d8517ed91e1509ed3826944df33707335217..0000000000000000000000000000000000000000
--- a/bin/sed_get_binutils_version
+++ /dev/null
@@ -1 +0,0 @@
-s|^GNU.* \([0-9.]\+\)[^ ]*|\1|p
diff --git a/bin/sed_get_make_major b/bin/sed_get_make_major
deleted file mode 100644
index cc2b89a466d4cd9e92e33869bbcc7a329db40d50..0000000000000000000000000000000000000000
--- a/bin/sed_get_make_major
+++ /dev/null
@@ -1 +0,0 @@
-s/.* Make[^0-9]*\([0-9]*\)\..*$/\1/p
diff --git a/bin/sed_get_make_minor b/bin/sed_get_make_minor
deleted file mode 100644
index b8b7d6c5d0ca0ba5563fbad8ad7521deb9c364eb..0000000000000000000000000000000000000000
--- a/bin/sed_get_make_minor
+++ /dev/null
@@ -1 +0,0 @@
-s/.* Make[^0-9]*[0-9]*\.\([0-9]*\).*$/\1/p
diff --git a/bin/shift_oracles.sh b/bin/shift_oracles.sh
deleted file mode 100755
index 431ffdceb4b8ff0a3103adc3a1a387521d805749..0000000000000000000000000000000000000000
--- a/bin/shift_oracles.sh
+++ /dev/null
@@ -1,177 +0,0 @@
-#!/bin/bash -eu
-##########################################################################
-# #
-# This file is part of Frama-C. #
-# #
-# Copyright (C) 2007-2024 #
-# 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). #
-# #
-##########################################################################
-
-# [shift_oracles.sh [commit] source.c -- test1.oracle test2.oracle ...]
-# modifies the set of oracles w.r.t. [source.c], using `git diff` to
-# estimate how many lines were added/removed and then replacing line numbers
-# accordingly, to reduce noise when diffing files.
-# Note: the oracles must be pristine, because calling multiple times this
-# script will modify the oracles at each call.
-# Also, because the script uses `git diff`, the modified source must not be
-# in the index.
-
-###### Command-line parsing-related code ######
-
-function usage_error {
- echo "usage: $0 [--dry-run] [commit [commit]] modified_source -- oracles"
- echo ""
- echo " example:"
- echo " $0 tests/my_test/test.c -- tests/**/*.oracle"
- echo ""
- echo " --dry-run: do not run sed, instead print command line"
- echo " commit numbers/names: optional, passed to 'git diff'"
- echo " modified_source: a single file that has been modified"
- echo " oracles: 1 or more ptests .oracle files"
- exit 1
-}
-
-if [ $# -lt 3 ]; then usage_error; fi
-
-if [ "$1" = "--dry-run" ]; then
- dry_run=1
- shift
-else
- dry_run=0
-fi
-
-file=""
-git_diff_args=""
-oracles=
-for i in $(seq $#); do
- if [ ${!i} = "--" ]; then
- # found '--', use it to determine other arguments
- if [ $i -eq 1 -o $i -eq $# ]; then
- usage_error
- fi
- file_i=$((i-1))
- file="${!file_i}"
- echo "file = $file"
- if [ ! -f "$file" ]; then
- echo "$file is not a file"
- exit 1
- fi
- git_diff_args=${@:1:$((i-1))}
- oracles=("${@:$((i+1))}")
- break
- fi
-done
-if [ "$file" = "" ]; then # no '--' found, or no file before '--'
- usage_error
-fi
-
-###### Actual script code ######
-
-lines=$(wc -l "$file" | cut -d' ' -f1)
-line_shift= #empty array
-# initialize all lines to "no shift"
-for i in $(seq $lines); do
- line_shift[$i]=0
-done
-
-# compute the amount to be shifted for each line, using `git diff -U0 source.c`
-# the regex is complex because some elements are optional
-# (e.g., when the number of modified lines is 1, ",1" is omitted)
-start_line=1
-first_hunk=1
-shift_amount=0
-while read -r hunk
-do
- IFS=' ' read a b c d e f < <(echo "$hunk")
- first_line1=$a
- #echo "a=$a -- b=$b -- c=$c -- d=$d -- e=$e -- f=$f"
- if [[ $b =~ ^, ]]; then
- n_lines1=$c
- first_line2=$d
- if [[ $e =~ ^, ]]; then n_lines2=$f; else n_lines2=1; fi
- else
- n_lines1=1
- first_line2=$b
- if [[ $c =~ ^, ]]; then n_lines2=$d; else n_lines2=1; fi
- fi
- #echo "first_line1=$first_line1 -- n_lines1=$n_lines1 -- first_line2=$first_line2 -- n_lines2=$n_lines2"
- if [ $first_hunk -eq 1 ]; then
- first_hunk=0
- start_line=$first_line1
- hunk_diff=$((n_lines2 - n_lines1))
- shift_amount=$hunk_diff
- echo "processing hunk: $first_line1,$n_lines1 $first_line2,$n_lines2 (shift amount: $shift_amount)"
- else
- end_line=$first_line1
- for i in $(seq $start_line $((end_line - 1))); do
- line_shift[$i]=$shift_amount
- done
- start_line=$end_line
- hunk_diff=$((n_lines2 - n_lines1))
- shift_amount=$((shift_amount + hunk_diff))
- echo "processing hunk: $first_line1,$n_lines1 $first_line2,$n_lines2 (shift amount: $shift_amount)"
- fi
-done < <(git diff --unified=0 $git_diff_args | grep -P '^@@.*@@' | sed -r -e 's/@@ [+-]([0-9]+)(,([0-9]+))? [+-]([0-9]+)(,([0-9]+))? @@.*$/\1 \2 \3 \4 \5 \6/')
-
-if [ $first_hunk -eq 1 ]; then
- echo "error: no hunks found in git diff: git diff $git_diff_args"
- exit 1
-fi
-
-# after finishing all hunks, shift until end of file
-end_line=$lines
-for i in $(seq $start_line $((end_line - 1))); do
- line_shift[$i]=$shift_amount
-done
-
-# Note: sources in the Frama-C libc may be printed in two ways, either with
-# "share/libc/..." or "FRAMAC_SHARE/libc/...", so we must account for them.
-# This may be fixed in a later Frama-C version.
-source_in_libc=0
-if [[ $file =~ share/libc/(.*) ]]; then
- source_in_libc=1
- source="share/libc/${BASH_REMATCH[1]}"
- source2="FRAMAC_SHARE/libc/${BASH_REMATCH[1]}"
- echo "replacing expressions: \"$source\" or \"$source2\""
-else
- source="$file"
- echo "replacing expressions: \"$source\""
-fi
-
-# build the large regex that will be given to sed
-sed_regex=""
-for n in $(seq $lines); do
- if [ ${line_shift[$n]} -ne 0 ]; then
- shifted_n=$((n+line_shift[$n]))
- sed_regex+="s|$source:$n\b|$source:$shifted_n|g; t ;"
- if [ $source_in_libc -ne 0 ]; then
- sed_regex+="s|$source2:$n\b|$source2:$shifted_n|g; t ;"
- fi
- fi
-done
-
-if [ $dry_run -eq 1 ] ; then
- echo "dry run: will not run sed"
- echo "final command: sed -i '$sed_regex' ${oracles[@]}"
-else
- echo "modifying ${#oracles[@]} oracle(s) in-place..."
- if [ ${#oracles[@]} -gt 500 ]; then
- echo "(this may take a few minutes)"
- fi
- sed -i "$sed_regex" ${oracles[@]}
- echo "done."
-fi