diff --git a/dev/disable-plugins.sh b/dev/disable-plugins.sh new file mode 100755 index 0000000000000000000000000000000000000000..96ce47d2b42971f6e6fc6a21511fe6477d1a2222 --- /dev/null +++ b/dev/disable-plugins.sh @@ -0,0 +1,73 @@ +#!/usr/bin/env bash +########################################################################## +# # +# 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). # +# # +########################################################################## + +if [ ! -f VERSION ]; then + echo "This script is meant to be run from the root directory of Frama-C" + exit 2 +fi + +if [ $# == "0" ]; then + rm -f src/plugins/dune + echo "All plugin enabled" + echo "Make sure to clean the current directory before rebuilding" + exit 0 +fi + +PLUGINS= +for PLUGIN in "$@" ; do + PLUGINS="$PLUGINS $PLUGIN" +done + +cat > src/plugins/dune <<EOL +;; File generated by ./dev/disable-plugins.sh <PLUGINS> +(include_subdirs no) +;; Disabled plugin list: +(data_only_dirs ${PLUGINS}) +(rule + (alias "frama-c-configure") + (deps (universe)) + (action (progn + (echo "Disabled plug-in(s):") +EOL + +for PLUGIN in "$@" ; do + echo " (echo \"- src/plugins/$PLUGIN\")" >> src/plugins/dune +done + +cat >> src/plugins/dune <<EOL +))) +;; Test +(alias (name ptests) (deps (alias ptests_config))) +(rule + (alias "ptests_config") + (deps (universe)) + (action (progn + (echo "Testing with disabled plug-in(s):") +EOL +for PLUGIN in "$@" ; do + echo " (echo \"- src/plugins/$PLUGIN\")" >> src/plugins/dune +done +echo ")))" >> src/plugins/dune + +echo "Disabled plug-ins: $PLUGINS" +echo "Make sure to clean the current directory before rebuilding"