Merge branch 'fix/andre/check-newlines' into 'master'

[Makefile] replace shell scripts with more efficient OCaml-based ones

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

.gitignore

@@ -24,6 +24,7 @@ frama_c_journal.ml
 /frama-c-*.tar.gz
 /.merlin
 /headers/hdrck
+/headers/hdrck.exe
 
 #build
 
@@ -64,6 +65,10 @@ autom4te.cache
 /devel_tools/fc-time
 /devel_tools/fc-memuse
 /bin/ocamldep_transitive_closure
+/bin/check_newlines
+/bin/check_newlines.exe
+/bin/isutf8
+/bin/isutf8.exe
 
 #share
 /share/Makefile.config

Makefile

@@ -243,7 +243,7 @@ DISTRIB_FILES:=\
       $(THEME_ICONS_FLAT)                                               \
       man/frama-c.1 doc/README						\
       doc/code/docgen.ml                                                \
-      doc/code/*.css doc/code/intro_plugin.txt				\
+      $(wildcard doc/code/*.css) doc/code/intro_plugin.txt              \
       doc/code/intro_plugin_D_and_S.txt                                 \
       doc/code/intro_plugin_default.txt                                 \
       doc/code/intro_kernel_plugin.txt					\
@@ -329,12 +329,17 @@ DISTRIB_FILES:=\
 
 # Test files to be included in the distribution (without header checking).
 # Plug-ins should use PLUGIN_DISTRIB_TESTS to export their test files.
-DISTRIB_TESTS=$(shell git ls-files \
+DISTRIB_TESTS=$(shell find \
                   tests \
                   src/plugins/aorai/tests \
                   src/plugins/report/tests \
-                  src/plugins/wp/tests | $(SED) 's/ /@/g')
-
+                  src/plugins/wp/tests \
+                  -type d -name result -prune -false \
+                  -o -type d -name 'result_*' -prune -false \
+                  -o -path 'tests/crowbar/*' -type d \! -name input -prune -false \
+                  -o -type f \! -name "*\.log" \! -name "*\.o" \
+                    \! -name '*~' \! -name "*\.cm*"  \! -name "*.sav" \
+                    -perm /u+w | sed -e 's/ /@/g')
 
 # files that are needed to compile API documentation of external plugins
 DOC_GEN_FILES:=$(addprefix doc/code/,\
@@ -2133,7 +2138,7 @@ else
 endif
 
 hdrck-clean:
-	$(RM) headers/hdrck headers/hdrck.o
+	$(RM) $(HDRCK) headers/hdrck.o
 	$(RM) headers/hdrck.cmx headers/hdrck.cmi headers/hdrck.cmp
 
 clean:: hdrck-clean
@@ -2141,6 +2146,55 @@ clean:: hdrck-clean
 CURRENT_HEADERS?=open-source
 CURRENT_HEADER_DIRS?=$(addsuffix /$(CURRENT_HEADERS),$(HEADER_DIRS))
 
+CHECK_NEWLINES:=./bin/check_newlines$(EXE)
+
+$(CHECK_NEWLINES): bin/check_newlines.ml
+	$(PRINT_MAKING)	$@
+ifeq ($(OCAMLBEST),opt)
+	$(OCAMLOPT) unix.cmxa $< -o $@
+else
+	$(OCAMLC) unix.cma $< -o $@
+endif
+
+check-newlines-clean:
+	$(RM) $(CHECK_NEWLINES) bin/check_newlines.cm* bin/check_newlines.o
+
+clean:: check-newlines-clean
+
+ISUTF8:=./bin/isutf8$(EXE)
+
+$(ISUTF8): bin/isutf8.ml
+	$(PRINT_MAKING)	$@
+ifeq ($(OCAMLBEST),opt)
+	$(OCAMLOPT) $< -o $@
+else
+	$(OCAMLC) $< -o $@
+endif
+
+isutf8-clean:
+	$(RM) $(ISUTF8) bin/isutf8.cm* bin/isutf8.o
+
+clean:: isutf8-clean
+
+FILES_WITHOUT_NEWLINE := \
+  VERSION \
+  VERSION_CODENAME
+
+BINARY_DISTRIB_FILES := \
+  $(sort $(wildcard ivette/src/dome/doc/template/static/fonts/*)) \
+  $(sort $(wildcard share/*.ico share/*.png share/theme/*/*.png))
+
+BINARY_DISTRIB_TESTS := \
+  tests/misc/oracle/interpreted_automata_dataflow_backward.dot \
+  tests/misc/oracle/interpreted_automata_dataflow_forward.dot \
+  tests/verisec/suite/programs/apps/SpamAssassin/BID-6679/message_write/test \
+  tests/verisec/suite/programs/apps/sendmail/CVE-1999-0047/mime7to8/array_vs_pointer.ods \
+  tests/verisec/suite/programs/apps/sendmail/CVE-1999-0047/mime7to8/data_testing.ods \
+
+TESTS_WITHOUT_NEWLINE := \
+  $(BINARY_DISTRIB_TESTS) \
+  tests/spec/unfinished-oneline-acsl-comment.i \
+
 # OPEN_SOURCE: set it to 'yes' if you want to check open source headers
 # STRICT_HEADERS: set it to 'yes' if you want to consider warnings as errors
 # The target check-headers does the following checks:
@@ -2153,34 +2207,22 @@ CURRENT_HEADER_DIRS?=$(addsuffix /$(CURRENT_HEADERS),$(HEADER_DIRS))
 # because identical headers but with different encodings are not exactly
 # easy to distinguish
 .PHONY: check-headers
-check-headers: $(HDRCK)
+check-headers: $(HDRCK) $(CHECK_NEWLINES) $(ISUTF8)
 	$(PRINT) "Checking $(DISTRIB_HEADERS) headers (OPEN_SOURCE=$(OPEN_SOURCE), CURRENT_HEADERS=$(CURRENT_HEADERS))..."
 	$(PRINT) "- HEADER_SPEC_FILE=$(HEADER_SPEC_FILE)"
 	$(PRINT) "- CURRENT_HEADER_DIRS=$(CURRENT_HEADER_DIRS)"
 	$(PRINT) "- FORBIDDEN_HEADERS=$(DISTRIB_PROPRIETARY_HEADERS)"
-	 # Workaround to avoid "argument list too long" in make 3.82+ without
-	 # using 'file' built-in, only available on make 4.0+
-	 # for make 4.0+, using the 'file' function could be a better solution,
-	 # although it seems to segfault in 4.0 (but not in 4.1)
-	$(RM) distrib_files.tmp distrib_tests.tmp header_exceptions.tmp
-	@$(foreach file,$(DISTRIB_FILES),\
-			echo $(file) >> distrib_files.tmp$(NEWLINE))
-	@$(foreach file,$(DISTRIB_TESTS),\
-			echo $(file) >> distrib_tests.tmp$(NEWLINE))
-	@$(foreach file,$(HEADER_EXCEPTIONS),\
-			echo $(file) >> header_exceptions.tmp$(NEWLINE))
-
+	# Workaround to avoid "argument list too long" in Cygwin
+	$(file >distrib_files.tmp) $(foreach O,$(DISTRIB_FILES),$(file >>distrib_files.tmp,$O))
+	$(file >distrib_tests.tmp) $(foreach O,$(DISTRIB_TESTS),$(file >>distrib_tests.tmp,$(subst @, ,$(O))))
+	$(file >header_exceptions.tmp) $(foreach O,$(HEADER_EXCEPTIONS),$(file >>header_exceptions.tmp,$O))
 	echo "Checking that distributed files terminate with a newline..."
-	bin/check_newline.sh distrib_files.tmp
-	bin/check_newline.sh distrib_tests.tmp
-	@if command -v file >/dev/null 2>/dev/null; then \
-		echo "Checking that distributed files do not use iso-8859..."; \
-		file --mime-encoding -f distrib_files.tmp -f distrib_tests.tmp | \
-			grep "iso-8859" \
-			| $(SED) "s/^/error: invalid encoding in /" \
-			| ( ! grep "error: invalid encoding" ); \
-	else echo "command 'file' not found, skipping encoding checks"; \
-	fi
+	$(CHECK_NEWLINES) distrib_files.tmp $(FILES_WITHOUT_NEWLINE) $(BINARY_DISTRIB_FILES)
+	$(CHECK_NEWLINES) distrib_tests.tmp $(TESTS_WITHOUT_NEWLINE) $(BINARY_DISTRIB_TESTS)
+	echo "Checking that distributed files do not use iso-8859..."
+	$(ISUTF8) distrib_files.tmp $(BINARY_DISTRIB_FILES)
+	$(ISUTF8) distrib_tests.tmp $(BINARY_DISTRIB_TESTS)
+	echo "Checking headers..."
 	$(HDRCK) \
 		$(HDRCK_EXTRA) \
 		$(addprefix -header-dirs ,$(CURRENT_HEADER_DIRS)) \
@@ -2481,13 +2523,10 @@ else
 endif
 	$(RM) -r $(CLIENT_DIR)
 	$(MKDIR) -p $(CLIENT_DIR)
-	@#Workaround to avoid "argument list too long" in make 3.82+ without
-	@#using 'file' built-in, only available on make 4.0+
-	@#for make 4.0+, using the 'file' function could be a better solution,
-	@#although it seems to segfault in 4.0 (but not in 4.1)
-	$(RM) file_list_to_archive.tmp
-	@$(foreach file,$(DISTRIB_FILES) $(DISTRIB_TESTS),\
-			echo $(file) | $(SED) 's/@/ /g' >> file_list_to_archive.tmp$(NEWLINE))
+	#Workaround to avoid "argument list too long" in Cygwin
+	$(file >file_list_to_archive.tmp)
+	$(foreach f,$(DISTRIB_FILES), \
+             $(file >>file_list_to_archive.tmp,$(subst @, ,$(f))))
 	$(TAR) -cf - --files-from file_list_to_archive.tmp | $(TAR) -C $(CLIENT_DIR) -xf -
 	$(RM) file_list_to_archive.tmp
 	$(PRINT_MAKING) files

bin/check_newline.sh

-#!/bin/bash -e
-
-# $1: file containing the list of files to check
-# prints a warning for each file not finishing with a newline,
-# unless it is one of a few well-known exceptions (e.g. VERSION).
-# Note: requires the 'file' command-line tool to check which files are text.
-
-if [ $# -lt 1 ]; then
-    echo "usage: $0 file_list.txt"
-    exit 2
-fi
-
-is_likely_text_file() {
-    case $(file -b --mime-type - < "$1") in
-        (text/*) echo "1"
-    esac
-}
-
-errors=0
-
-IFS=''
-while read file
-do
-    if [ -n "$(is_likely_text_file "$file")" ]; then
-        x=$(tail -c 1 "$file")
-        if [ "$x" != "" ] && [ "$file" != "VERSION" ] && [ "$file" != "VERSION_CODENAME" ]; then
-            echo "error: no newline at end of file: $file"
-            errors=$((errors+1))
-        fi
-    fi
-done < <(file -f "$1" --mime | grep '\btext' | cut -d: -f1)
-
-if [ $errors -gt 0 ]; then
-    echo "Found $errors file(s) with errors."
-    exit 1
-fi

bin/check_newlines.ml

+module StringSet = Set.Make(String)
+
+(* returns true for empty files *)
+let is_last_byte_newline filename =
+  try
+    let ic = open_in filename in
+    try
+      let fd = Unix.descr_of_in_channel ic in
+      ignore (Unix.lseek fd (-1) Unix.SEEK_END);
+      let buf = Bytes.create 1 in
+      let n_bytes_read = Unix.read fd buf 0 1 in
+      close_in ic;
+      n_bytes_read <= 0 || Bytes.get buf 0 = '\n'
+    with
+    | Unix.Unix_error _ ->
+      (* probably an empty file; ignoring *)
+      close_in ic;
+      true
+  with
+  | Sys_error msg ->
+    (* possibly a non-existing file (e.g. with spaces); ignoring *)
+    Format.printf "check_newlines: cannot open, ignoring file: %s (%s)@."
+      filename msg;
+    true
+
+(* usage: first argument is a file name containing a list of files
+   (one per line) to be checked; the remaining arguments are a list of
+   files to be ignored during checking
+   (i.e. they do not terminate with newlines). *)
+let () =
+  if Array.length Sys.argv < 2 then begin
+    Format.printf "usage: %s file_list.txt [ignore1 ignore2 ...]@." Sys.argv.(0);
+    exit 0
+  end;
+  let errors = ref 0 in
+  let file_list_ic = open_in Sys.argv.(1) in
+  let to_ignore = StringSet.of_list (List.tl (Array.to_list Sys.argv)) in
+  begin
+    try
+      while true; do
+        let filename = input_line file_list_ic in
+        if not (StringSet.mem filename to_ignore) &&
+           not (is_last_byte_newline filename) then begin
+          incr errors;
+          Format.printf "error: no newline at end of file: %s@." filename
+        end
+      done
+    with End_of_file ->
+      close_in file_list_ic
+  end;
+  if !errors > 0 then begin
+    Format.printf "Found %d file(s) with errors.@." !errors;
+    exit 1
+  end else
+    exit 0

bin/isutf8.ml

+module StringSet = Set.Make(String)
+
+exception False
+
+let is_valid_utf8 filename =
+  let buf = Bytes.create 1024 in
+  try
+    let ic = open_in_bin filename in
+    let extra = ref 0 in
+    try
+      while true do
+        let n_bytes_read = input ic buf 0 1024 in
+        if n_bytes_read = 0 then raise End_of_file;
+        for i = 0 to n_bytes_read - 1 do
+          let c = Bytes.get_uint8 buf i in
+          (*Format.printf "extra: %d, read byte: %d (0x%x, char %c)@."
+            !extra c c (Char.chr c);*)
+          if !extra > 0 then begin
+            decr extra;
+            if c lsr 6 <> 2 then raise False
+          end
+          else
+          if c > 127 then begin
+            if c lsr 5 = 6 then extra := 1
+            else if c lsr 4 = 14 then extra := 2
+            else if c lsr 3 = 30 then extra := 3
+            else raise False
+          end;
+        done;
+      done;
+      close_in ic;
+      !extra = 0
+    with
+    | End_of_file ->
+      close_in ic;
+      !extra = 0
+    | False ->
+      close_in ic;
+      false
+  with
+  | Sys_error msg ->
+    (* possibly a non-existing file (e.g. with spaces); ignoring *)
+    Format.printf "isutf8: cannot open, ignoring file: %s (%s)@."
+      filename msg;
+    true
+
+(* usage: first argument is a file name containing a list of files
+   (one per line) to be checked; the remaining arguments are filenames
+   to be ignored during checking. *)
+let () =
+  if Array.length Sys.argv < 2 then begin
+    Format.printf "usage: %s file_list.txt [ignore1 ignore2 ...]@." Sys.argv.(0);
+    exit 0
+  end;
+  let errors = ref 0 in
+  let file_list_ic = open_in Sys.argv.(1) in
+  let to_ignore = StringSet.of_list (List.tl (Array.to_list Sys.argv)) in
+  begin
+    try
+      while true; do
+        let filename = input_line file_list_ic in
+        if not (StringSet.mem filename to_ignore)
+        && not (is_valid_utf8 filename) then begin
+          incr errors;
+          Format.printf "error: invalid UTF-8 in file: %s@." filename
+        end
+      done
+    with End_of_file ->
+      close_in file_list_ic
+  end;
+  if !errors > 0 then begin
+    Format.printf "Found %d file(s) with errors.@." !errors;
+    exit 1
+  end else
+    exit 0

configure.in

@@ -63,10 +63,9 @@ MAKE_DISTRIB=`sh -c "$MAKE -v | sed -n -e 's/\(.*\) Make.*$/\1/p'"`
 MAKE_MAJOR=`sh -c "$MAKE -v | sed -n  -f bin/sed_get_make_major"`
 MAKE_MINOR=`sh -c "$MAKE -v | sed -n -f bin/sed_get_make_minor"`
 AC_MSG_RESULT($MAKE_MAJOR.$MAKE_MINOR)
-if test "$MAKE_DISTRIB" != GNU -o "$MAKE_MAJOR" -lt 3 \
-   -o "$MAKE_MAJOR" = 3 -a "$MAKE_MINOR" -lt 81
+if test "$MAKE_DISTRIB" != GNU -o "$MAKE_MAJOR" -lt 4
 then
-   AC_MSG_ERROR([unsupported version; GNU Make version 3.81
+   AC_MSG_ERROR([unsupported version; GNU Make version 4.0
                  or higher is required.]);
 fi
 

ivette/Makefile

@@ -81,7 +81,7 @@ update-distrib-files:
 	@rm -f $(SRC_HEADERS)
 	@for f in `git ls-files .` ;\
 	 do \
-		echo "DISTRIB_FILES += \"ivette/$$f\"" >> $(SRC_DISTRIB) ;\
+		echo "DISTRIB_FILES += ivette/$$f" >> $(SRC_DISTRIB) ;\
 		headers/register.sh "$$f" >> $(SRC_HEADERS) ; \
 	 done
 	@chmod a-w $(SRC_DISTRIB)

src/plugins/aorai/tests/ya/saveload.i

 /* run.config
 NOFRAMAC:
-EXECNOW: LOG @PTEST_NAME@.res.0.log BIN @PTEST_NAME@.sav @frama-c@ -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya @PTEST_FILE@ -save @PTEST_DIR@/result/@PTEST_NAME@.sav > @PTEST_DIR@/result/@PTEST_NAME@.res.0.log
-EXECNOW: LOG @PTEST_NAME@.res.1.log @frama-c@ -load @PTEST_DIR@/result/@PTEST_NAME@.sav -then-on aorai -eva > @PTEST_DIR@/result/@PTEST_NAME@.res.1.log
+EXECNOW: LOG @PTEST_NAME@.res.0.log.txt BIN @PTEST_NAME@.sav @frama-c@ -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya @PTEST_FILE@ -save @PTEST_DIR@/result/@PTEST_NAME@.sav > @PTEST_DIR@/result/@PTEST_NAME@.res.0.log.txt
+EXECNOW: LOG @PTEST_NAME@.res.1.log.txt @frama-c@ -load @PTEST_DIR@/result/@PTEST_NAME@.sav -then-on aorai -eva > @PTEST_DIR@/result/@PTEST_NAME@.res.1.log.txt
 */
 /* run.config_prove
 DONTRUN:

tests/pdg/call.c

 /* run.config
    
-   STDOPT: +"-lib-entry -main g -pdg -pdg-dot tests/pdg/call "
+   STDOPT: +"-lib-entry -main g -pdg -pdg-dot tests/pdg/result/call "
 */
 
 /* Ne pas modifier : exemple utilisé dans le rapport. */

tests/pdg/doc_dot.c

 /* run.config
- STDOPT: +"-lib-entry -main g -fct-pdg g -pdg-dot tests/pdg/doc"
+ STDOPT: +"-lib-entry -main g -fct-pdg g -pdg-dot tests/pdg/result/doc"
 */
 /* To build the svg file:
- * dot -Tsvg tests/pdg/doc.g.dot > tests/pdg/doc.g.svg
+ * dot -Tsvg tests/pdg/result/doc.g.dot > tests/pdg/result/doc.g.svg
  */
 int G1, G2, T[10];
 

tests/pdg/dyn_dpds.ml

@@ -23,7 +23,7 @@ let main _ =
   let kf =  Globals.Functions.find_def_by_name "main" in
   let pdg = !Db.Pdg.get kf in
   Format.printf "%a@." (!Db.Pdg.pretty ~bw:false) pdg;
-  !Db.Pdg.extract pdg "tests/pdg/dyn_dpds_0.dot";
+  !Db.Pdg.extract pdg "tests/pdg/result/dyn_dpds_0.dot";
   let assert_sid = 5 in (* assert ( *p>G) *)
   let assert_stmt, kf = Kernel_function.find_from_sid assert_sid in
   let _assert_node =
@@ -44,6 +44,6 @@ let main _ =
   Format.printf "Warning : cannot select %a in this function...@\n"
     Locations.Zone.pretty undef;
   Format.printf "%a@." (!Db.Pdg.pretty ~bw:false) pdg;
-  !Db.Pdg.extract pdg "tests/pdg/dyn_dpds_1.dot"
+  !Db.Pdg.extract pdg "tests/pdg/result/dyn_dpds_1.dot"
 
 let () = Db.Main.extend main

tests/pdg/oracle/call.res.oracle

@@ -22,12 +22,12 @@
 [eva] done for function g
 [pdg] computing for function f
 [pdg] done for function f
-[pdg] dot file generated in tests/pdg/call.f.dot
+[pdg] dot file generated in tests/pdg/result/call.f.dot
 [pdg] computing for function g
 [from] Computing for function f
 [from] Done for function f
 [pdg] done for function g
-[pdg] dot file generated in tests/pdg/call.g.dot
+[pdg] dot file generated in tests/pdg/result/call.g.dot
 [pdg] ====== PDG GRAPH COMPUTED ======
 [pdg] PDG for f
  {n1}: InCtrl

tests/pdg/oracle/doc_dot.res.oracle

@@ -16,7 +16,7 @@
 [from] Computing for function f
 [from] Done for function f
 [pdg] done for function g
-[pdg] dot file generated in tests/pdg/doc.g.dot
+[pdg] dot file generated in tests/pdg/result/doc.g.dot
 [pdg] PDG for g
  {n1}: InCtrl
  {n2}: VarDecl : x

tests/pdg/oracle/dyn_dpds.res.oracle

@@ -94,7 +94,7 @@ RESULT for main:
    -[--d]-> 13
  {n16}: OutRet
    -[--d]-> 15
-[pdg] dot file generated in tests/pdg/dyn_dpds_0.dot
+[pdg] dot file generated in tests/pdg/result/dyn_dpds_0.dot
 Warning : cannot select G in this function...
 RESULT for main:
  {n1}: InCtrl
@@ -142,4 +142,4 @@ RESULT for main:
    -[--d]-> 13
  {n16}: OutRet
    -[--d]-> 15
-[pdg] dot file generated in tests/pdg/dyn_dpds_1.dot
+[pdg] dot file generated in tests/pdg/result/dyn_dpds_1.dot