diff --git a/Makefile b/Makefile index 78f43ee735682bb7ce238b88abd860759049e37c..503c3b09333789240d2c31df0c4d43182f2e2148 100644 --- a/Makefile +++ b/Makefile @@ -2339,7 +2339,7 @@ dist-clean distclean: clean clean-doc \ $(RM) src/dummy/*/*.cm* src/dummy/*/*.o src/dummy/*/*.a \ src/dummy/*/*.annot src/dummy/*/*~ src/dummy/*/*.output \ src/dummy/*/*.annot src/dummy/*/\#* - + $(RM) $(CHECK_NEWLINES) $(ISUTF8) ifeq ($(OCAMLWIN32),yes) # Use Win32 typical resources @@ -2525,7 +2525,7 @@ endif $(MKDIR) -p $(CLIENT_DIR) #Workaround to avoid "argument list too long" in Cygwin $(file >file_list_to_archive.tmp) - $(foreach f,$(DISTRIB_FILES), \ + $(foreach f,$(DISTRIB_FILES) $(DISTRIB_TESTS), \ $(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 diff --git a/nix/default.nix b/nix/default.nix index 3d1a1a7e696198b03ea3979ccb5159562ae0c691..e6718411b5a9cb7867c177d8deaf79d84c204bc3 100644 --- a/nix/default.nix +++ b/nix/default.nix @@ -140,9 +140,6 @@ pkgs.lib.makeExtensible buildInputs = self.buildInputs; opamPackages = [ "headache=1.05" ]; outputs = [ "out" ]; - postPatch = '' - patchShebangs . - ''; configurePhase = '' unset CC autoconf @@ -160,10 +157,14 @@ pkgs.lib.makeExtensible build-from-distrib-tarball = mk_deriv { name = "frama-c-build-from-distrib-tarball"; + doCheck = true; buildInputs = self.buildInputs; opamPackages = self.build-distrib-tarball.opamPackages; src = self.build-distrib-tarball.out ; outputs = [ "out" ]; + postPatch = '' + patchShebangs . + ''; configurePhase = '' unset CC autoconf @@ -172,6 +173,11 @@ pkgs.lib.makeExtensible buildPhase = '' make -j 4 ''; + checkPhase = '' + make clean_share_link + make create_share_link + make tests -j4 PTESTS_OPTS="-error-code -j 4" + ''; installPhase = '' true ''; diff --git a/share/analysis-scripts/analysis.mk b/share/analysis-scripts/analysis.mk index 3483b89d6d4689e36703eebed525d4ff2f79223a..4e545c9e747b46328d15a067ded5540408252f66 100644 --- a/share/analysis-scripts/analysis.mk +++ b/share/analysis-scripts/analysis.mk @@ -69,31 +69,19 @@ endif # nor Busybox' have it, in which case we ignore it) SED_UNBUFFERED:=sed$(shell sed --unbuffered //p /dev/null 2>/dev/null && echo " --unbuffered" || true) -# Test if on a Mac; -# test if /usr/bin/time is available, otherwise use the shell builtin -# (which has less options) -UNAME := $(shell uname -s) -ifeq ($(UNAME),Darwin) -ifneq (,$(wildcard /usr/bin/time)) +# If there is a GNU time in the PATH, which contains the desired options +# (-f and -o), use them; otherwise, use any time (be it a shell builtin +# or a command). 'env' allows bypassing shell builtins (if they exist), +# since they usually don't have the required options. +ifeq (OK,$(shell env time -f 'test' -o '/dev/null' echo OK || echo KO)) define time_with_output - /usr/bin/time -p + env time -f 'user_time=%U\nmemory=%M' -o "$(1)" endef else define time_with_output time endef endif -else -ifneq (,$(wildcard /usr/bin/time)) -define time_with_output - /usr/bin/time -f 'user_time=%U\nmemory=%M' -o "$(1)" -endef -else -define time_with_output - time -endef -endif -endif # --- Utilities --- diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in index a8a90519d288cf15a0b0ff217accc394186f4d97..b7383b8f2634b2be740589a10f6c878692604f29 100644 --- a/src/plugins/e-acsl/Makefile.in +++ b/src/plugins/e-acsl/Makefile.in @@ -338,7 +338,7 @@ EACSL_TEST_FILES = \ tests/temporal/test_config_dev \ tests/format/test_config \ tests/format/test_config_dev \ - tests/print.ml + tests/print.ml \ # Test files without header management EACSL_DISTRIB_TESTS = \ @@ -348,7 +348,9 @@ EACSL_DISTRIB_TESTS = \ $(dir)/test_config_dev \ $(dir)/oracle/* \ $(dir)/oracle_dev/* \ - ) + ) \ + tests/utils/signalled.h \ + EACSL_RTL_FILES = $(EACSL_RTL_SRC)