From a75eee4b3fbdf1ed20dd41e2276b5fad74875940 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Wed, 2 Nov 2022 17:14:55 +0100
Subject: [PATCH] [lint/headers] pre-push hook
---
dev/git-hooks/pre-push.sh | 66 +++++++++++++++++++++++++++++++++++++++
1 file changed, 66 insertions(+)
create mode 100755 dev/git-hooks/pre-push.sh
diff --git a/dev/git-hooks/pre-push.sh b/dev/git-hooks/pre-push.sh
new file mode 100755
index 00000000000..4521eb81400
--- /dev/null
+++ b/dev/git-hooks/pre-push.sh
@@ -0,0 +1,66 @@
+#!/bin/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). #
+# #
+##########################################################################
+
+# Examples of installation of this pre-push hook (client side):
+# - cp ./dev/git-hooks/pre-push.sh .git/hooks/pre-push
+# - (cd .git/hooks/ && ln -s ../../dev/git-hooks/pre-push.sh pre-push)
+
+echo "Pre-push Hook..."
+
+STAGED=$(git diff --diff-filter ACMR --name-only --cached origin/$(git rev-parse --abbrev-ref HEAD) | sort)
+UNSTAGED=$(git diff --diff-filter DMR --name-only | sort)
+
+if [ "$STAGED" = "" ];
+then
+ echo "No diff since last push, nothing to do"
+ exit 0
+fi
+
+if [ "$UNSTAGED" != "" ];
+then
+ INTER=$(comm -12 <(ls $STAGED) <(ls $UNSTAGED))
+
+ if [ "$INTER" != "" ];
+ then
+ echo "Cannot validate push."
+ echo "The following staged files have been modified, renamed or deleted."
+ for file in $INTER ; do
+ echo "- $file"
+ done
+ exit 1
+ fi
+fi
+
+STAGED=$(echo $STAGED | tr '\n' ' ')
+
+TMP=$(mktemp)
+
+cleanup () {
+ rm "$TMP"
+}
+trap cleanup exit
+
+git check-attr -za $STAGED > "$TMP"
+make lint LINTCK_FILES_INPUT="$TMP" || exit 1
+git check-attr -z header_spec $STAGED > "$TMP"
+make check-headers HDRCK_FILES_INPUT="$TMP" HDRCK_EXTRA="-quiet" || exit 1
--
GitLab