From 7a8b68df1c8afd53b97258ef1c686c0c6735925e Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Mon, 25 Jul 2022 14:48:14 +0200
Subject: [PATCH] [dev] tool for disabling plugins
---
dev/disable-plugins.sh | 73 ++++++++++++++++++++++++++++++++++++++++++
1 file changed, 73 insertions(+)
create mode 100755 dev/disable-plugins.sh
diff --git a/dev/disable-plugins.sh b/dev/disable-plugins.sh
new file mode 100755
index 00000000000..96ce47d2b42
--- /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"
--
GitLab