From fc86f9f5ec0826eeb08d4042a3bb05007719d6f5 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Tue, 24 Nov 2020 18:00:02 +0100
Subject: [PATCH] [kernel] Add a migration script from Titanium to Vanadium
---
bin/migration_scripts/titanium2vanadium.sh | 164 +++++++++++++++++++++
headers/header_spec.txt | 1 +
2 files changed, 165 insertions(+)
create mode 100755 bin/migration_scripts/titanium2vanadium.sh
diff --git a/bin/migration_scripts/titanium2vanadium.sh b/bin/migration_scripts/titanium2vanadium.sh
new file mode 100755
index 00000000000..6c374f21283
--- /dev/null
+++ b/bin/migration_scripts/titanium2vanadium.sh
@@ -0,0 +1,164 @@
+#! /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). #
+# #
+##########################################################################
+
+#
+# Converts a Frama-C plugin from Frama-C 22 Titanium to Frama-C 23 Vanadium,
+# on a best-efforts basis (no guarantee that the result is fully compatible).
+#
+# known missing features:
+# - doesn't work if a directory name contains spaces
+# - doesn't follow symbolic links to directories
+
+ARGS=$@
+
+DIR=
+
+# verbosing on by default
+VERBOSE="v"
+
+sedi ()
+{
+ if [ -n "`sed --help 2> /dev/null | grep \"\\-i\" 2> /dev/null`" ]; then
+ sed -i "$@"
+ else
+ # option '-i' is not recognized by sed: use a tmp file
+ new_temp=`mktemp /tmp/frama-c.XXXXXXX` || exit 1
+ sed "$@" > $new_temp
+ eval last=\${$#}
+ mv $new_temp $last
+ fi
+}
+
+dirs ()
+{
+ if [ -z "$DIR" ]; then
+ DIR=.
+ fi
+}
+
+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 \
+ -e 's/Cil\.Frama_c_builtins/Cil_builtins.Frama_c_builtins/g' \
+ -e 's/Cil\.is_builtin/Cil_builtins.is_builtin/g' \
+ -e 's/Cil\.is_unused_builtin/Cil_builtins.is_unused_builtin/g' \
+ -e 's/Cil\.is_special_builtin/Cil_builtins.is_special_builtin/g' \
+ -e 's/Cil\.add_special_builtin/Cil_builtins.add_special_builtin/g' \
+ -e 's/Cil\.add_special_builtin_family/Cil_builtins.add_special_builtin_family/g' \
+ -e 's/Cil\.init_builtins/Cil_builtins.init_builtins/g' \
+ -e 's/Cil\.Builtin_functions/Cil_builtins.Builtin_functions/g' \
+ -e 's/Cil\.builtinLoc/Cil_builtins.builtinLoc/g' \
+ $file
+}
+
+apply_one_dir ()
+{
+ if [ "$VERBOSE" ]; then
+ echo "Processing directory `pwd`"
+ fi
+ for f in `ls -p1 *.ml* 2> /dev/null`; do
+ process_file $f
+ done
+}
+
+apply_recursively ()
+{
+ apply_one_dir
+ for d in `ls -p1 | grep \/`; do
+ safe_goto $d .. apply_recursively
+ done
+}
+
+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 $ARGS; do
+ parse_arg $s
+ done
+ applying_to_list $FN
+}
+
+cmd_line
+exit 0
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 3b8202ed0b9..d52363f4281 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -41,6 +41,7 @@ bin/migration_scripts/sodium2magnesium.sh: CEA_LGPL
bin/migration_scripts/sulfur2chlorine.sh: CEA_LGPL
bin/migration_scripts/chlorine2argon.sh: CEA_LGPL
bin/migration_scripts/potassium2calcium.sh: CEA_LGPL
+bin/migration_scripts/titanium2vanadium.sh: CEA_LGPL
bin/sed_get_binutils_version: .ignore
bin/sed_get_make_major: .ignore
bin/sed_get_make_minor: .ignore
--
GitLab