From ba07371f203ecf4f36ca185f318203246e3e3478 Mon Sep 17 00:00:00 2001 From: Andre Maroneze <andre.maroneze@cea.fr> Date: Fri, 5 Aug 2022 14:21:56 +0200 Subject: [PATCH] [dev] remove local-export.sh and update scripts --- bin/dune | 1 - bin/frama-c-gui.byte | 27 --------------------------- bin/frama-c.byte | 27 --------------------------- bin/frama-c.top | 27 --------------------------- bin/local_export.sh | 30 ------------------------------ dev/frama-c-callgrind.sh | 10 ++-------- 6 files changed, 2 insertions(+), 120 deletions(-) delete mode 100755 bin/frama-c-gui.byte delete mode 100755 bin/frama-c.byte delete mode 100755 bin/frama-c.top delete mode 100644 bin/local_export.sh diff --git a/bin/dune b/bin/dune index 05d52fe3f3c..fcb02ca1875 100644 --- a/bin/dune +++ b/bin/dune @@ -27,6 +27,5 @@ (frama-c-script as frama-c-script) (frama-c-config as frama-c-config) (test.sh as frama-c-test.sh) - (local_export.sh as local_export.sh) ) ) diff --git a/bin/frama-c-gui.byte b/bin/frama-c-gui.byte deleted file mode 100755 index 0252458a8e5..00000000000 --- a/bin/frama-c-gui.byte +++ /dev/null @@ -1,27 +0,0 @@ -#!/bin/sh -########################################################################## -# # -# This file is part of Frama-C. # -# # -# Copyright (C) 2007-2022 # -# 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 "$@" diff --git a/bin/frama-c.byte b/bin/frama-c.byte deleted file mode 100755 index 8a000c3bab4..00000000000 --- a/bin/frama-c.byte +++ /dev/null @@ -1,27 +0,0 @@ -#!/bin/sh -########################################################################## -# # -# This file is part of Frama-C. # -# # -# Copyright (C) 2007-2022 # -# 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 "$@" diff --git a/bin/frama-c.top b/bin/frama-c.top deleted file mode 100755 index 662f2cda8af..00000000000 --- a/bin/frama-c.top +++ /dev/null @@ -1,27 +0,0 @@ -#!/bin/sh -########################################################################## -# # -# This file is part of Frama-C. # -# # -# Copyright (C) 2007-2022 # -# 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 "$@" diff --git a/bin/local_export.sh b/bin/local_export.sh deleted file mode 100644 index 0a4ea448234..00000000000 --- a/bin/local_export.sh +++ /dev/null @@ -1,30 +0,0 @@ -########################################################################## -# # -# This file is part of Frama-C. # -# # -# Copyright (C) 2007-2022 # -# 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). # -# # -########################################################################## - -MYDIR=$(dirname $0) -BINDIR=$(cd $MYDIR && pwd) #more portable realpath -ROOTDIR=$BINDIR/.. - -export FRAMAC_PLUGIN_GUI="$ROOTDIR/lib/plugins/gui" -export FRAMAC_LIB="$ROOTDIR/lib/fc" -export FRAMAC_PLUGIN="$ROOTDIR/lib/plugins" -export FRAMAC_SHARE="$ROOTDIR/share" diff --git a/dev/frama-c-callgrind.sh b/dev/frama-c-callgrind.sh index 1de367e65fe..72bc33a4b3d 100755 --- a/dev/frama-c-callgrind.sh +++ b/dev/frama-c-callgrind.sh @@ -24,8 +24,6 @@ # Script for profiling Frama-C with callgrind (a valgrind tool). # Note: execution time with valgrind is about 15x-20x slower. # -# Use this script at the root of the repository, so local_export.sh can be found -# in bin. # For more focused results, you can activate the profiling only after entering # a specific function. For instance, to only profile Eva, add # @@ -42,11 +40,7 @@ # # kcachegrind callgrind.out -BASH_ARGV0="bin/frama-c" # hackish way to tell local_export that its dir is bin - -. bin/local_export.sh - -valgrind \ +dune exec -- valgrind \ --tool=callgrind --callgrind-out-file=callgrind.out --dump-instr=yes \ --separate-callers=2 --collect-jumps=yes --fn-skip='caml_*' \ - $BINDIR/toplevel.opt "$@" + frama-c "$@" -- GitLab