Skip to content
Snippets Groups Projects

Compare revisions

Changes are shown as if the source revision was being merged into the target revision. Learn more about comparing revisions.

Source

Select target project
No results found

Target

Select target project
  • pub/frama-c
  • proidiot/frama-c
  • lthls/frama-c
3 results
Show changes
Expand all Hide whitespace changes
Inline Side-by-side
Showing
with 494 additions and 600 deletions
VERSION
View file @ a46de615
21.0-beta
30.0+dev
VERSION_CODENAME
View file @ a46de615
Scandium
Zinc
bin/build-src-distrib.sh deleted 100755 → 0
View file @ 3b09672b
#! /usr/bin/env bash
set -u
# 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 99
fi
# git-lfs needs to be installed
if ! command -v git-lfs >/dev/null 2>/dev/null; then
echo "git-lfs is required"
exit 99
fi
# Set it to "no" in order to really execute the commands.
# Otherwise, they are only printed.
DEBUG=no
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_TAG=$(git describe --tag)
FRAMAC_VERSION_CODENAME=$(cat VERSION_CODENAME)
FRAMAC_VERSION_AND_CODENAME="${FRAMAC_VERSION}-${FRAMAC_VERSION_CODENAME}"
TARGZ_FILENAME=frama-c-${FRAMAC_VERSION_AND_CODENAME}.tar.gz
VERSION_MODIFIER=$(cat VERSION | sed -e s/[0-9.]*\\\(.*\\\)/\\1/)
if test -n "$VERSION_MODIFIER"; then FINAL_RELEASE=no; else FINAL_RELEASE=yes; fi
if test "$FRAMAC_VERSION" != "$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
run () {
cmd=$1
echo "$cmd"
if test "$DEBUG" == "no"; then
sh -c "$cmd" || { echo "Aborting step ${STEP}."; exit "${STEP}"; }
fi
}
GITLAB_DIR=./pub-frama-c
GITLAB_GIT="git@git.frama-c.com:pub/frama-c.git"
if test ! -d $GITLAB_DIR/.git; then
echo "WARNING: $GITLAB_DIR/.git directory not found; do you want to clone it? (y/n)"
read CHOICE
case "${CHOICE}" in
"Y"|"y")
run "git clone $GITLAB_GIT $GITLAB_DIR"
;;
*)
echo "gitlab's public Frama-C project must be linked at $GITLAB_DIR \
(clone or symbolic link)"
exit 1
;&
esac
fi
GITLAB_BRANCH=$(git --git-dir=$GITLAB_DIR/.git rev-parse --abbrev-ref HEAD)
if test "$FRAMAC_BRANCH" != "$GITLAB_BRANCH"; then
echo "WARNING: switching pub-frama-c to current branch $FRAMAC_BRANCH"
run "git -C $GITLAB_DIR checkout -b $FRAMAC_BRANCH"
fi
GITLAB_WIKI_GIT="git@git.frama-c.com:pub/frama-c.wiki"
GITLAB_WIKI=./frama-c.wiki
if test ! -d $GITLAB_WIKI/.git; then
echo "WARNING: $GITLAB_WIKI/.git directory not found; do you want to clone it? (y/n)"
read CHOICE
case "${CHOICE}" in
"Y"|"y")
run "git clone $GITLAB_WIKI_GIT"
;;
*)
echo "pub/frama-c wiki must be linked at $GITLAB_WIKI \
(clone or symbolic link)"
exit 1
;&
esac
fi
GITLAB_WIKI_BRANCH=$(git --git-dir=$GITLAB_WIKI/.git rev-parse --abbrev-ref HEAD)
if test "$GITLAB_WIKI_BRANCH" != "master"; then
echo "WARNING: pub/frama-c's wiki is not on the master branch";
fi
ACSL_GIT="git@gitlab.com:acsl-language/acsl.git"
ACSL_DIR="./doc/acsl"
if test \! -d $ACSL_DIR/.git ; then
echo "WARNING: $ACSL_DIR/.git directory not found; do you want to clone it? (y/n)"
read CHOICE
case "${CHOICE}" in
"Y"|"y")
pushd "./doc"
run "git clone $ACSL_GIT"
popd
;;
*)
echo "The Github ACSL repository must be linked at $ACSL_DIR (clone or symbolic link)"
exit 1
;&
esac
fi
MANUALS_DIR="./doc/manuals"
# push on frama-c.com only for final releases
if test "$FINAL_RELEASE" = "yes"; then
WEBSITE_DIR="./website"
if test \! -d $WEBSITE_DIR/.git ; then
echo "ERROR: $WEBSITE_DIR/.git directory not found"
echo "The Frama-C website repository must be linked at $WEBSITE_DIR (clone or symbolic link)"
exit 1
fi
WEBSITE_BRANCH=`git --git-dir=$WEBSITE_DIR/.git rev-parse --abbrev-ref HEAD`
fi # FINAL_RELEASE == yes
BUILD_DIR_ROOT="/tmp/release"
BUILD_DIR="$BUILD_DIR_ROOT/frama-c"
echo "Frama-C Version : $FRAMAC_VERSION"
echo "Frama-C Branch : $FRAMAC_BRANCH"
echo "Final release : $FINAL_RELEASE"
echo "pub/frama-c dir : $GITLAB_DIR"
echo "pub/frama-c branch : $GITLAB_BRANCH"
echo "pub/frama-c wiki : $GITLAB_WIKI"
echo "Manuals Dir : $MANUALS_DIR"
if test "$FINAL_RELEASE" = "yes"; then
echo "Website Dir : $WEBSITE_DIR"
echo "Website Branch : $WEBSITE_BRANCH"
else
echo "Intermediate release: website not updated"
fi
echo "Build Dir : $BUILD_DIR"
DOWNLOAD_DIR="www/download"
step () {
STEP=$1
echo
echo "Step $1: $2"
}
export LC_CTYPE=en_US.UTF-8
echo -n "Steps are:
N) previous information is wrong, STOP the script
0) compile PDF manuals (will ERASE $MANUALS_DIR!)
1) reset local copy of target repositories
2) build the source distribution
3) build API bundle
4) build documentation companions
5) copy and stage locally the distributed manuals
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 "COMPILING PDF MANUALS"
run "rm -rf $MANUALS_DIR"
run "mkdir -p $MANUALS_DIR"
run "doc/build-manuals.sh"
;&
1)
run "git -C $GITLAB_DIR reset --hard"
run "git -C $GITLAB_WIKI reset --hard"
if test "$FINAL_RELEASE" = "yes"; then
run "git -C $WEBSITE_DIR reset --hard"
fi
;&
2)
step 2 "BUILDING THE SOURCE DISTRIBUTION"
# WARNING! MUST RUN git update-index BEFORE git diff-index!
# See: https://stackoverflow.com/questions/36367190/git-diff-files-output-changes-after-git-status
run "git update-index --refresh"
if ! git diff-index HEAD --; then
echo ""
echo "### WARNING: uncommitted git changes will be discarded when creating archive!"
echo "Proceed anyway? [y/N]"
read CHOICE
case "${CHOICE}" in
"Y"|"y")
;;
*)
echo "Stash or commit local changes, then run the script again."
exit 1
esac
fi
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 src-distrib"
# sanity check: markdown-report must be distributed
run "tar tf $BUILD_DIR/$TARGZ_FILENAME | grep -q src/plugins/markdown-report"
# populate release assets in wiki
run "mkdir -p $GITLAB_WIKI/downloads"
run "cp $BUILD_DIR/$TARGZ_FILENAME $GITLAB_WIKI/downloads/"
if test "$FINAL_RELEASE" = "yes"; then
SPEC_FILE="$DOWNLOAD_DIR/$TARGZ_FILENAME"
run "rm -f $WEBSITE_DIR/$SPEC_FILE"
run "cp $BUILD_DIR/$TARGZ_FILENAME $WEBSITE_DIR/$SPEC_FILE"
run "git -C $WEBSITE_DIR add $SPEC_FILE"
run "cp Changelog $WEBSITE_DIR/src/last-release/Changelog"
run "cp src/plugins/wp/Changelog $WEBSITE_DIR/src/wpChangelog"
run "cp src/plugins/wp/Changelog $WEBSITE_DIR/src/last-release/wpChangelog"
fi
;&
3)
#note: this step may fail if step 4 was performed,
# because it will erase BUILD_DIR
step 3 "BUILDING THE API BUNDLE"
if test \! -d "$BUILD_DIR" ; then
echo "ERROR: $BUILD_DIR does not exist, possibly removed by another step"
exit 1
fi
run "cd $BUILD_DIR; make -j doc-distrib"
if test "$FINAL_RELEASE" = "yes"; then
SPEC_FILE="$DOWNLOAD_DIR/frama-c-${FRAMAC_VERSION_AND_CODENAME}-api.tar.gz"
run "rm -f $WEBSITE_DIR/$SPEC_FILE"
run "cp $BUILD_DIR/frama-c-api.tar.gz $WEBSITE_DIR/$SPEC_FILE"
run "git -C $WEBSITE_DIR add $SPEC_FILE"
fi
;&
4)
step 4 "BUILDING THE DOCUMENTATION COMPANIONS"
if test \! -d "$BUILD_DIR" ; then
echo "ERROR: $BUILD_DIR does not exist, possibly removed by another step"
exit 1
fi
run "cd $BUILD_DIR; make -j doc-companions"
if test "$FINAL_RELEASE" = "yes"; then
SPEC_FILE="$DOWNLOAD_DIR/hello-${FRAMAC_VERSION_AND_CODENAME}.tar.gz"
RELE_FILE="$DOWNLOAD_DIR/hello.tar.gz"
run "rm -f $WEBSITE_DIR/$SPEC_FILE $WEBSITE_DIR/$RELE_FILE"
run "cp $BUILD_DIR/hello-${FRAMAC_VERSION_AND_CODENAME}.tar.gz $WEBSITE_DIR/$SPEC_FILE"
run "git -C $WEBSITE_DIR add $SPEC_FILE"
run "ln -s hello-${FRAMAC_VERSION_AND_CODENAME}.tar.gz $WEBSITE_DIR/$RELE_FILE";
run "git -C $WEBSITE_DIR add $RELE_FILE"
run "rm -rf $BUILD_DIR"
run "git worktree prune"
fi
;&
5)
step 5 "COPYING AND STAGING THE DISTRIBUTED MANUALS"
PAGE_NAME=Frama-C-${FRAMAC_VERSION_AND_CODENAME}.md
WIKI_PAGE=$GITLAB_WIKI/$PAGE_NAME
run "mkdir -p $GITLAB_WIKI/manuals"
run "sed -i -e '/<!-- LAST RELEASE -->/a \
- [${FRAMAC_VERSION} (${FRAMAC_VERSION_CODENAME})](Frama-C-${FRAMAC_VERSION_AND_CODENAME})' $GITLAB_WIKI/Home.md"
echo "# Frama-C release ${FRAMAC_VERSION} (${FRAMAC_VERSION_CODENAME})" > $WIKI_PAGE
echo "## Sources" >> $WIKI_PAGE
echo " - [$TARGZ_FILENAME](downloads/$TARGZ_FILENAME)" >> $WIKI_PAGE
echo "" >> $WIKI_PAGE
echo "## Manuals" >> $WIKI_PAGE
for fpath in $MANUALS_DIR/*; do
f=$(basename $fpath)
f_no_ext=${f%.*}
if [[ $f =~ ^frama-c ]]; then
echo "Skipping adding link to $f in wiki"
continue
fi
if [[ $f_no_ext = *${FRAMAC_VERSION_AND_CODENAME} ]]; then
echo "Skipping adding link to $f in wiki"
continue
fi
echo "- [$f](manuals/$f)" >> $WIKI_PAGE
run "cp $fpath $GITLAB_WIKI/manuals/"
run "git -C $GITLAB_WIKI add manuals/$f"
done
run "git -C $GITLAB_WIKI add $PAGE_NAME"
;;
*)
echo "Bad entry: ${STEP}"
echo "Exiting without doing anything.";
exit 31
;;
esac
exit 0
bin/check-reference-configuration.sh 0 → 100755
View file @ a46de615
#!/bin/bash -eu
##########################################################################
# #
# This file is part of Frama-C. #
# #
# Copyright (C) 2007-2025 #
# 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). #
# #
##########################################################################
# Displays the current working configuration of OCaml dependencies of Frama-C,
# comparing them with the one in `reference-configuration.md`.
if ! type "opam" > /dev/null; then
opam="NOT"
else
opam="$(opam --version)"
if [[ $opam =~ ^([0-9+]).([0-9+]) ]]; then
major="${BASH_REMATCH[1]}"
minor="${BASH_REMATCH[2]}"
if [[ "$major" -eq 2 && "$minor" -eq 0 ]]; then
echo "warning: opam > 2.1 expected, got $major.$minor."
echo " Suggested commands may not work properly."
fi
else
echo "warning: unknown opam version."
echo " Suggested commands may not work properly."
fi
fi
if ! type "ocaml" > /dev/null; then
ocaml="NOT"
else
ocaml=$(ocaml -vnum)
fi
version_via_opam() {
v=$(opam info -f installed-version "$1" 2>/dev/null)
if [ "$v" = "" ] || [ "$v" = "--" ]; then
echo "NOT"
else
echo "$v"
fi
}
SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )"
refconf="$SCRIPT_DIR/../reference-configuration.md"
packages=$(grep '^- [^ ]*\.' "$refconf" | sed 's/^- //' | sed 's/ .*//')
bold=$(tput bold)
normal=$(tput sgr0)
has_any_diffs=0
# Check OCaml version separately (not same syntax as the packages)
working_ocaml=$(grep "\- OCaml " "$refconf" | sed 's/.*OCaml //')
if [ "$working_ocaml" != "$ocaml" ]; then
echo -n "warning: OCaml ${bold}${ocaml}${normal} installed, "
echo "expected ${bold}${working_ocaml}${normal}"
has_any_diffs=1
fi
all_packages=""
for package in $packages; do
name=${package%%.*}
all_packages+=" $package"
working_version=$(echo "$package" | sed 's/^[^.]*\.//')
if [ "$opam" != "NOT" ]; then
actual_version=$(version_via_opam "$name")
else
echo "error: opam not found."
exit 1
fi
if [ "$working_version" != "$actual_version" ]; then
has_any_diffs=1
echo -n "warning: $name ${bold}${actual_version}${normal} installed, "
echo "expected ${bold}${working_version}${normal}"
fi
done
echo "All packages checked."
if [ $has_any_diffs -ne 0 ]; then
echo "Useful commands:"
echo " opam switch create ${working_ocaml}"
echo " opam install$all_packages"
echo " rm -f ~/.why3.conf && why3 config detect"
fi
bin/dune 0 → 100644
View file @ a46de615
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
;; ;;
;; Copyright (C) 2007-2025 ;;
;; 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). ;;
;; ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(install
(package frama-c)
(section bin)
(files
(frama-c-script as frama-c-script)
(frama-c-config as frama-c-config)
(test.sh as frama-c-test.sh)
)
)
bin/frama-c
View file @ a46de615
......@@ -3,7 +3,7 @@
# #
# This file is part of Frama-C. #
# #
# Copyright (C) 2007-2020 #
# Copyright (C) 2007-2025 #
# CEA (Commissariat à l'énergie atomique et aux énergies #
# alternatives) #
# #
......@@ -22,6 +22,4 @@
##########################################################################
. $(dirname $0)/local_export.sh
exec $BINDIR/toplevel.opt "$@"
dune exec --root=$(dirname $0)/.. --no-build --no-print-directory -- frama-c "$@"
bin/frama-c-config
View file @ a46de615
......@@ -3,7 +3,7 @@
# #
# This file is part of Frama-C. #
# #
# Copyright (C) 2007-2020 #
# Copyright (C) 2007-2025 #
# CEA (Commissariat à l'énergie atomique et aux énergies #
# alternatives) #
# #
......@@ -21,7 +21,4 @@
# #
##########################################################################
. $(dirname $0)/local_export.sh
exec $BINDIR/fc-config "$@"
exec $(dirname $0)/frama-c -no-autoload-plugins "$@"
bin/frama-c-gui
View file @ a46de615
......@@ -3,7 +3,7 @@
# #
# This file is part of Frama-C. #
# #
# Copyright (C) 2007-2020 #
# Copyright (C) 2007-2025 #
# CEA (Commissariat à l'énergie atomique et aux énergies #
# alternatives) #
# #
......@@ -22,6 +22,4 @@
##########################################################################
. $(dirname $0)/local_export.sh
exec $BINDIR/viewer.opt "$@"
dune exec --root=$(dirname $0)/.. --no-build frama-c-gui -- "$@"
bin/frama-c-gui.byte deleted 100755 → 0
View file @ 3b09672b
#!/bin/sh
##########################################################################
# #
# This file is part of Frama-C. #
# #
# Copyright (C) 2007-2020 #
# 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). #
# #
##########################################################################
. $(dirname $0)/local_export.sh
exec $BINDIR/viewer.byte "$@"
bin/frama-c-script
View file @ a46de615
This diff is collapsed.
bin/frama-c.byte deleted 100755 → 0
View file @ 3b09672b
#!/bin/sh
##########################################################################
# #
# This file is part of Frama-C. #
# #
# Copyright (C) 2007-2020 #
# 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). #
# #
##########################################################################
. $(dirname $0)/local_export.sh
exec $BINDIR/toplevel.byte "$@"
bin/frama-c.debug
View file @ a46de615
......@@ -3,7 +3,7 @@
# #
# This file is part of Frama-C. #
# #
# Copyright (C) 2007-2020 #
# Copyright (C) 2007-2025 #
# CEA (Commissariat à l'énergie atomique et aux énergies #
# alternatives) #
# #
......@@ -33,7 +33,6 @@ fi
OCAML_VERSION=$(ocamlc -version)
case $OCAML_VERSION in
4.05*|4.06*|4.07*) DYNLINK='load_printer "dynlink.cma"';;
4.08*)
echo "impossible to load dynlink in ocamldebug for version $OCAML_VERSION";
echo "pretty-printers will not be loaded";
......@@ -50,7 +49,6 @@ $DYNLINK
load_printer "extlib.cmo"
load_printer "filepath.cmo"
load_printer "integer.cmo"
load_printer "transitioning.cmo"
load_printer "pretty_utils.cmo"
load_printer "cil_types_debug.cmo"
load_printer "cabs_debug.cmo"
......@@ -66,8 +64,6 @@ install_printer Cil_types_debug.pp_global
install_printer Cil_types_debug.pp_typ
install_printer Cil_types_debug.pp_ikind
install_printer Cil_types_debug.pp_fkind
install_printer Cil_types_debug.pp_bitsSizeofTyp
install_printer Cil_types_debug.pp_bitsSizeofTypCache
install_printer Cil_types_debug.pp_attribute
install_printer Cil_types_debug.pp_attributes
install_printer Cil_types_debug.pp_attrparam
......@@ -80,7 +76,6 @@ install_printer Cil_types_debug.pp_varinfo
install_printer Cil_types_debug.pp_storage
install_printer Cil_types_debug.pp_exp
install_printer Cil_types_debug.pp_exp_node
install_printer Cil_types_debug.pp_exp_info
install_printer Cil_types_debug.pp_constant
install_printer Cil_types_debug.pp_unop
install_printer Cil_types_debug.pp_binop
......@@ -128,7 +123,6 @@ install_printer Cil_types_debug.pp_predicate
install_printer Cil_types_debug.pp_spec
install_printer Cil_types_debug.pp_acsl_extension
install_printer Cil_types_debug.pp_acsl_extension_kind
install_printer Cil_types_debug.pp_loop_pragma
install_printer Cil_types_debug.pp_slice_pragma
install_printer Cil_types_debug.pp_impact_pragma
install_printer Cil_types_debug.pp_pragma
......@@ -137,7 +131,6 @@ install_printer Cil_types_debug.pp_funspec
install_printer Cil_types_debug.pp_code_annotation
install_printer Cil_types_debug.pp_funbehavior
install_printer Cil_types_debug.pp_global_annotation
install_printer Cil_types_debug.pp_custom_tree
install_printer Cil_types_debug.pp_kinstr
install_printer Cil_types_debug.pp_cil_function
install_printer Cil_types_debug.pp_kernel_function
......
bin/frama-c.top deleted 100755 → 0
View file @ 3b09672b
#!/bin/sh
##########################################################################
# #
# This file is part of Frama-C. #
# #
# Copyright (C) 2007-2020 #
# 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). #
# #
##########################################################################
. $(dirname $0)/local_export.sh
exec $BINDIR/toplevel.top "$@"
bin/git.sh 0 → 100755
View file @ a46de615
This diff is collapsed.
bin/indent.sh deleted 100755 → 0
View file @ 3b09672b
# 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
bin/init-plugin.sh 0 → 100755
View file @ a46de615
#! /usr/bin/env bash
##########################################################################
# #
# This file is part of Frama-C. #
# #
# Copyright (C) 2007-2025 #
# 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 [[ $# != 1 && $# != 2 ]]; then
echo "Usage: $0 <plugin-name> [<directory>]"
exit 2
fi
if [[ $# == 1 ]]; then
directory="."
else
directory=$2
fi
if [[ ! -d $directory ]]; then
echo "'$directory': not such file or directory"
exit 17
fi
echo "Target directory is '$directory'"
dune_file=$directory/dune
if [[ -f $dune_file ]]; then
echo "'$dune_file' file already exists."
exit 17
fi
cat > $dune_file <<EOF
( library
(name $1)
(public_name frama-c-$1.core)
(flags -open Frama_c_kernel :standard)
(libraries frama-c.kernel)
)
(plugin (optional) (name $1) (libraries frama-c-$1.core) (site (frama-c plugins)))
EOF
bin/lint.sh
View file @ a46de615
This diff is collapsed.
bin/local_export.sh deleted 100644 → 0
View file @ 3b09672b
This diff is collapsed.
bin/merge-master.sh deleted 100755 → 0
View file @ 3b09672b
This diff is collapsed.
bin/migration_scripts/aluminium2silicon.sh
View file @ a46de615
......@@ -3,7 +3,7 @@
# #
# This file is part of Frama-C. #
# #
# Copyright (C) 2007-2020 #
# Copyright (C) 2007-2025 #
# CEA (Commissariat à l'énergie atomique et aux énergies #
# alternatives) #
# #
......