Merge branch 'fix/dev/check-files-with-spaces' into 'master'

[dev] allow spaces in file names

See merge request frama-c/frama-c!4472

dev/check-files.sh

-#!/bin/bash
+#!/bin/bash -eu
 ##########################################################################
 #                                                                        #
 #  This file is part of Frama-C.                                         #
@@ -29,7 +29,7 @@ DO_HDRCK="yes"
 REFERENCE=
 MODE="all"
 
-while [ "$1" != "" ]
+while [ $# -gt 0 ]
 do
     case "$1" in
         "-h"|"-help"|"--help")
@@ -37,8 +37,8 @@ do
             echo "OPTIONS"
             echo "  -h|-help|--help    print this message and exit"
             echo "  -f|--fix           fix files"
-            echo "  -c|--commit        check modified files to be commited only"
-            echo "  -p|--push          check modified files to be pushed only"
+            echo "  -c|--commit        check modified files to be committed only"
+            echo "  -p|--push range    check modified files to be pushed only"
             echo "  --no-headers       do not check headers"
             echo "  --no-lint          do not check lint"
             exit 0
@@ -48,10 +48,12 @@ do
             HDRCK=headers
             ;;
         "-p"|"--push")
-            REFERENCE="origin/$(git rev-parse --abbrev-ref HEAD)"
+            shift
+            DIFF_ARG=$1
             MODE="push"
             ;;
         "-c"|"--commit")
+            DIFF_ARG=--cached
             MODE="commit"
             ;;
         "--no-headers")
@@ -70,53 +72,52 @@ done
 
 if [ "$MODE" = "all" ]; then
   if [ $DO_LINT = "yes" ] ; then
-    make $LINT || exit 1
+    make $LINT
   fi
   if [ $DO_HDRCK = "yes" ] ; then
     # Don't define HDRCK_EXTRA, that is required by external plugins
-    make $HDRCK || exit 1
+    make $HDRCK
   fi
 else
-  STAGED=$(git diff --diff-filter ACMR --name-only --cached $REFERENCE | sort)
-  UNSTAGED=$(git diff --diff-filter DMR --name-only | sort)
+  TMP_STAGED=$(mktemp)
+  TMP_UNSTAGED=$(mktemp)
+  TMP_INTER=$(mktemp)
+  TMP_INPUT=$(mktemp)
 
-  if [ "$STAGED" = "" ];
+  cleanup () {
+    rm -f "$TMP_STAGED" "$TMP_UNSTAGED" "$TMP_INPUT" "$TMP_INTER"
+  }
+  trap cleanup exit
+  git diff -z --diff-filter ACMR --name-only $DIFF_ARG | sort -z > "$TMP_STAGED"
+  git diff -z --diff-filter DMR --name-only | sort -z > "$TMP_UNSTAGED"
+
+  if [ ! -s "$TMP_STAGED" ];
   then
     echo "No staged modification since last $MODE, nothing to do."
     exit 0
   fi
 
-  if [ "$UNSTAGED" != "" ];
+  if [ -s "$TMP_UNSTAGED" ];
   then
-    INTER=$(comm -12 <(ls $STAGED) <(ls $UNSTAGED))
-
-    if [ "$INTER" != "" ];
+    comm -12 --zero-terminated "$TMP_STAGED" "$TMP_UNSTAGED" > "$TMP_INTER"
+    if [ -s "$TMP_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
+      while IFS= read -r -d $'\0' f; do
+        echo "- $f"
+      done < "$TMP_INTER"
       exit 1
     fi
   fi
 
-  STAGED=$(echo $STAGED | tr '\n' ' ')
-
-  TMP=$(mktemp)
-
-  cleanup () {
-    rm -f "$TMP"
-  }
-  trap cleanup exit
-
-  if [ $DO_LINT = "yes" ] ; then
-    git check-attr -za $STAGED > "$TMP"
-    make $LINT LINTCK_FILES_INPUT="$TMP" || exit 1
+  if [ $DO_LINT = "yes" -a -s "$TMP_STAGED" ] ; then
+    git check-attr -za --stdin < "$TMP_STAGED" > "$TMP_INPUT"
+    make $LINT LINTCK_FILES_INPUT="$TMP_INPUT"
   fi
-  if [ $DO_HDRCK = "yes" ] ; then
-    git check-attr -z header_spec $STAGED > "$TMP"
+  if [ $DO_HDRCK = "yes" -a -s "$TMP_STAGED" ] ; then
+    git check-attr -z header_spec --stdin < "$TMP_STAGED" > "$TMP_INPUT"
     # Don't define HDRCK_EXTRA, that is required by external plugins
-    make $HDRCK HDRCK_FILES_INPUT="$TMP" || exit 1
+    make $HDRCK HDRCK_FILES_INPUT="$TMP_INPUT"
   fi
 fi

dev/git-hooks/pre-commit.sh

@@ -23,8 +23,8 @@
 
 # Example of installation of this pre-commit hook (client side):
 # - (cd .git/hooks/ && ln -s ../../dev/git-hooks/pre-commit.sh pre-commit)
-# Note: if you decide to copy the file, the `SCRIPT_DIR` variable must be
-# fixed accordingly.
+
+ROOT=$(git rev-parse --show-toplevel)
 
 echo "Pre-commit Hook..."
 
@@ -36,5 +36,4 @@ then
   exit 0
 fi
 
-SCRIPT_DIR=$(dirname -- "$( readlink -f -- "$0"; )")
-"$SCRIPT_DIR/../check-files.sh" -c || exit 1
+"$ROOT/dev/check-files.sh" -c || exit 1

dev/git-hooks/pre-push.sh

@@ -21,20 +21,30 @@
 #                                                                        #
 ##########################################################################
 
-# Example of installation of this pre-push hook (client side):
-# - (cd .git/hooks/ && ln -s ../../dev/git-hooks/pre-push.sh pre-push)
-# Note: if you decide to copy the file, the `SCRIPT_DIR` variable must be
-# fixed accordingly.
+ROOT=$(git rev-parse --show-toplevel)
 
 echo "Pre-push Hook..."
 
-STAGED=$(git diff --diff-filter ACMR --name-only --cached origin/$(git rev-parse --abbrev-ref HEAD) | sort)
+empty=$(git hash-object --stdin </dev/null | tr '[0-9a-f]' '0')
 
-if [ "$STAGED" = "" ];
-then
-  echo "No diff since last push, nothing to do"
-  exit 0
-fi
+remote=$1
 
-SCRIPT_DIR=$(dirname -- "$( readlink -f -- "$0"; )")
-"$SCRIPT_DIR/../check-files.sh" -p || exit 1
+while read local_ref local_oid remote_ref remote_oid
+do
+    if test "$local_oid" = "$empty"
+    then
+        # Handle delete
+        :
+    else
+        if test "$remote_oid" = "$empty"
+        then
+            # New branch, examine commits starting
+            # the forking point from master
+            remote_oid=$(git merge-base $local_ref master);
+        fi
+        range="$remote_oid $local_oid";
+        "$ROOT/dev/check-files.sh" -p "$range" || exit 1;
+    fi;
+done
+
+exit 0

tests/misc/with-space.i

@@ -2,3 +2,4 @@
  LIBS: ../with\ space/module
    OPT:
  */
+