From 06ac1a8d6f42554037e7dfd63aaa81ff1cd51409 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Virgile=20Pr=C3=A9vosto?= <virgile.prevosto@cea.fr>
Date: Thu, 23 Apr 2009 16:57:04 +0000
Subject: [PATCH] fix bug in rules for tests in Makefiles
---
.make-clean-stamp | 2 +-
Makefile.in | 23 ++++++++-----
doc/ltl_to_acsl/Makefile | 12 +++----
ptests/config.ml | 24 -------------
ptests/ptests.ml | 12 +++++--
share/Makefile.config.in | 67 ++++++++++++++++++++++++++++++++++++
share/Makefile.plugin | 57 +-----------------------------
tests/spec/rewrite_ensures.c | 7 ++--
8 files changed, 105 insertions(+), 99 deletions(-)
delete mode 100644 ptests/config.ml
diff --git a/.make-clean-stamp b/.make-clean-stamp
index b8626c4cff2..7ed6ff82de6 100644
--- a/.make-clean-stamp
+++ b/.make-clean-stamp
@@ -1 +1 @@
-4
+5
diff --git a/Makefile.in b/Makefile.in
index b2304f430e0..3ab737dcf5c 100644
--- a/Makefile.in
+++ b/Makefile.in
@@ -1271,6 +1271,10 @@ MODULES_TODOC += src/logic/fol.mli src/logic/logic_interp.mli \
PLUGIN_TESTS_LIST += spec
+.PRECIOUS: spec_TESTS_LIB spec_TESTS_LIB_BYTE
+
+$(eval $(call COMPILE_TESTS_ML_FILES,spec,spec))
+
##########################################################################
# Common startup module #
# All link command should add it as last linked module and depend on it. #
@@ -1562,7 +1566,7 @@ $(VERSIONFILE): VERSION share/Makefile.config
#########
.PHONY: tests oracles btests tests_dist
-tests: byte opt ptests ptests_config.cmo
+tests: byte opt ptests
$(PRINT_EXEC) ptests
time -p ./bin/ptests.byte$(EXE) $(PLUGIN_TESTS_LIST)
for plugin in $(EXTERNAL_PLUGINS); do \
@@ -1967,6 +1971,7 @@ clean:: $(PLUGIN_LIST:=_CLEAN) $(PLUGIN_DYN_LIST:=_CLEAN) \
done
$(PRINT_RM) generated files
$(RM) $(GENERATED)
+ $(RM) ptests_config.* # temporary clean-up of svn version
$(PRINT_RM) binaries
$(RM) bin/*.byte$(EXE) bin/*.opt$(EXE) bin/*.top$(EXE)
@@ -2048,18 +2053,20 @@ endif
# $(OCAMLOPT) -I ptests -dtypes -thread -o $@ \
# unix.cmxa threads.cmxa str.cmxa dynlink.cmxa $^
-ptests_config.ml: Makefile $(PTESTS_SRC)
+ptests/config.ml: Makefile
$(PRINT_MAKING) $@
$(RM) $@
$(ECHO) \
- "Config.default_suites := [" $(PLUGIN_TESTS_LIST:%='"%";') "]" > $@
+ "let default_suites = ref [" $(PLUGIN_TESTS_LIST:%='"%";') "];;" > $@
+ $(ECHO) \
+ "let no_native_dynlink = " \
+ $(subst yes,false,$(subst no,true,$(USABLE_NATIVE_DYNLINK))) ";;" \
+ >> $@
+ $(ECHO) \
+ "let toplevel_path = ref \"bin/toplevel.$(OCAMLBEST)$(EXE)\";;" >> $@
$(CHMOD_RO) $@
-GENERATED+=ptests_config.ml
-
-FILES_FOR_OCAMLDEP+=ptests_config.ml
-
-ptests_config.cmo: BFLAGS=-I ptests -c -g
+GENERATED+=ptests/config.ml
#######################
# source distribution #
diff --git a/doc/ltl_to_acsl/Makefile b/doc/ltl_to_acsl/Makefile
index 8b8778e1830..f507da4570d 100644
--- a/doc/ltl_to_acsl/Makefile
+++ b/doc/ltl_to_acsl/Makefile
@@ -1,4 +1,4 @@
-.PHONY: all clean
+.PHONY: all clean
DWNLDDIR=../manuals
DOCNAME=aorai-manual.pdf
@@ -9,7 +9,7 @@ all: main.pdf
main.ps: main.dvi
dvips $^ -o $@
-main.dvi: main.tex
+main.dvi: main.tex
latex main
# makeindex main
# bibtex main
@@ -19,15 +19,15 @@ main.dvi: main.tex
main.pdf: main.ps
ps2pdfwr $^
@echo ""
- @echo "Comilation Done (Not installed yet : [make install] needed)"
+ @echo "Compilation Done (Not installed yet : [make install] needed)"
-install: main.pdf
+install: main.pdf
@echo "copying main.pdf in $(DWNLDDIR)/$(DOCNAME)"
@cp main.pdf "$(DWNLDDIR)/$(DOCNAME)"
- @if [ -f example.tgz ] ; then rm example.tgz ; fi
+ @if [ -f example.tgz ] ; then rm example.tgz ; fi
@echo "copying example.tgz in ${DWNLDDIR}/$(ARCHIVENAME)"
- @tar -czf $(ARCHIVENAME) example --exclude=\.svn
+ @tar -czf $(ARCHIVENAME) example --exclude=\.svn
@cp $(ARCHIVENAME) "${DWNLDDIR}/$(ARCHIVENAME)"
diff --git a/ptests/config.ml b/ptests/config.ml
deleted file mode 100644
index 1851ab77833..00000000000
--- a/ptests/config.ml
+++ /dev/null
@@ -1,24 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2009 *)
-(* CEA (Commissariat à l'Énergie Atomique) *)
-(* *)
-(* 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). *)
-(* *)
-(**************************************************************************)
-
-let default_suites: string list ref = ref []
-
-let toplevel_path = ref (Filename.concat "bin" "toplevel.opt")
diff --git a/ptests/ptests.ml b/ptests/ptests.ml
index fe96d308ad5..f11f851abe8 100644
--- a/ptests/ptests.ml
+++ b/ptests/ptests.ml
@@ -49,7 +49,10 @@ let opt_to_byte =
let execnow_opt_to_byte =
let opt = Str.regexp "tests/\\(.+\\)[.]opt\\($\\|[ \t]\\)" in
- fun cmd -> Str.global_replace opt "tests/\\1.byte\\2" cmd
+ let cmxs = Str.regexp "tests/\\(.+\\)[.]cmxs\\($\\|[ \t]\\)" in
+ fun cmd ->
+ let cmd = Str.global_replace opt "tests/\\1.byte\\2" cmd in
+ Str.global_replace cmxs "tests/\\1.cmo\\2" cmd
let base_path = Filename.current_dir_name
(* (Filename.concat
@@ -350,7 +353,12 @@ let scan_test_file default dir f =
(fun name ->
if not
(!special_config = "" && name = ""
- || name = "_" ^ !special_config)
+ || name = "_" ^ !special_config
+ || (name = "_no_nat_dynlink" && !special_config=""
+ && Config.no_native_dynlink)
+ || (name = "_no_nat_dynlink_" ^ !special_config &&
+ Config.no_native_dynlink)
+ )
then
(ignore (scan_options dir scan_buffer default);
scan_config ()))
diff --git a/share/Makefile.config.in b/share/Makefile.config.in
index 8f6f7b209d3..ce75bdb9b25 100644
--- a/share/Makefile.config.in
+++ b/share/Makefile.config.in
@@ -215,6 +215,73 @@ PRINT_LATEX =$(PRINT) 'Latex '#
PRINT_DVIPS =$(PRINT) 'Dvips '#
PRINT_HEVEA =$(PRINT) 'Hevea '#
+#########
+# Tests #
+#########
+
+define COMPILE_TESTS_ML_FILES
+# Function with two arguments:
+# - $(1) is the test directory under consideration.
+# - $(2) is the name of Frama-C component under test (plugin or some core part)
+.PRECIOUS: $(patsubst %.ml, %.cmo %.cmx, $(wildcard tests/$(1)/*.ml))
+
+# $(2)_TESTS_TMP_$(1) only exists in order to deduce some variable
+# names using $(2) in the body of the rule.
+# touching the file in order to prevent unnecessarily 'make' actions
+tests/$(1)/$(2)_TESTS_TMP_$(1):
+ touch $$@
+
+# [JS 2009/03/18] in the 4 rules below, don't print anything while VERBOSEMAKE
+# is not set (otherwise "make tests" is too much verbose)
+
+# Strictly speaking, it does not depend on all cmx, but it is safer that way
+# need to launch ocamldep on tests directories to be more precise...
+tests/$(1)/%.cmx: tests/$(1)/$(2)_TESTS_TMP_$(1) \
+ tests/$(1)/%.ml $$(ALL_CMX) $$(GEN_OPT_LIBS)
+ $$(OCAMLOPT) -c $$(OFLAGS) \
+ $$(addprefix -I tests/,\
+ $$($$(patsubst tests/$(1)/%_TESTS_TMP_$(1),%_TESTS_DIRS, $$<))) \
+ $$(patsubst %.cmx,%.ml,$$@)
+
+tests/$(1)/%.cmxs: tests/$(1)/$(2)_TESTS_TMP_$(1) \
+ tests/$(1)/%.ml $$(ALL_CMX) $$(GEN_OPT_LIBS)
+ $$(OCAMLOPT) $$(OFLAGS) -shared -o $$@ \
+ $$(addprefix -I tests/,\
+ $$($$(patsubst tests/$(1)/%_TESTS_TMP_$(1),%_TESTS_DIRS, $$<))) \
+ $$(patsubst %.cmxs,%.ml,$$@)
+
+tests/$(1)/%.opt: tests/$(1)/$(2)_TESTS_TMP_$(1) \
+ $$($(2)_TESTS_LIB) \
+ tests/$(1)/%.cmx \
+ bin/toplevel.opt$$(EXE)
+ $$(OCAMLOPT) $$(OLINKFLAGS) -o $$@ \
+ $$(addprefix -I tests/,\
+ $$($$(patsubst tests/$(1)/%_TESTS_TMP_$(1),%_TESTS_DIRS, $$<))) \
+ $$(OPT_LIBS) $$(ALL_CMX) \
+ $$($$(patsubst tests/$(1)/%_TESTS_TMP_$(1),%_TESTS_LIB, $$<)) \
+ $$(STARTUPCMX) $$(patsubst %.opt,%.cmx,$$@)
+
+# See above for the dependency on all cmi
+tests/$(1)/%.cmo: tests/$(1)/$(2)_TESTS_TMP_$(1) \
+ tests/$(1)/%.ml $$(ALL_CMI) $$(GEN_BYTE_LIBS)
+ $$(OCAMLC) -c $$(BFLAGS) \
+ $$(addprefix -I tests/,\
+ $$($$(patsubst tests/$(1)/%_TESTS_TMP_$(1),%_TESTS_DIRS, $$<))) \
+ $$(patsubst %.cmo,%.ml,$$@)
+
+tests/$(1)/%.byte: tests/$(1)/$(2)_TESTS_TMP_$(1) \
+ $$($(2)_TESTS_LIB_BYTE) \
+ tests/$(1)/%.cmo \
+ bin/toplevel.byte$$(EXE)
+ $$(OCAMLC) $$(BLINKFLAGS) -o $$@ \
+ $$(addprefix -I tests/,\
+ $$($$(patsubst tests/$(1)/%_TESTS_TMP_$(1),%_TESTS_DIRS, $$<))) \
+ $$(BYTE_LIBS) $$(ALL_CMO) \
+ $$($$(patsubst tests/$(1)/%_TESTS_TMP_$(1),%_TESTS_LIB_BYTE, $$<)) \
+ $$(STARTUPCMO) $$(patsubst %.byte,%.cmo,$$@)
+
+endef #COMPILE_TESTS_ML_FILES
+
#################
# Generic rules #
#################
diff --git a/share/Makefile.plugin b/share/Makefile.plugin
index 37b2c936ef6..89518246784 100644
--- a/share/Makefile.plugin
+++ b/share/Makefile.plugin
@@ -496,62 +496,7 @@ $(PLUGIN_NAME)_TESTS_LIB_BYTE:=$(PLUGIN_TESTS_LIB:%=%.cmo)
# unnecessarily recompile those files.
.PRECIOUS: $($(PLUGIN_NAME)_TESTS_LIB) $($(PLUGIN_NAME)_TESTS_LIB_BYTE)
-define COMPILE_TESTS_ML_FILES
-# Function with one argument: $(1) is the test directory under consideration.
-
-.PRECIOUS: $(patsubst %.ml, %.cmo %.cmx, $(wildcard tests/$(1)/*.ml))
-
-# $(PLUGIN_NAME)_TESTS_TMP_$(1) only exists in order to deduce some variable
-# names using $(PLUGIN_NAME) in the body of the rule.
-# touching the file in order to prevent unnecessarily 'make' actions
-tests/$(1)/$$(PLUGIN_NAME)_TESTS_TMP_$(1):
- touch $$@
-
-# [JS 2009/03/18] in the 4 rules below, don't print anything while VERBOSEMAKE
-# is not set (otherwise "make tests" is too much verbose)
-
-# Strictly speaking, it does not depend on all cmx, but it is safer that way
-# need to launch ocamldep on tests directories to be more precise...
-tests/$(1)/%.cmx: tests/$(1)/$$(PLUGIN_NAME)_TESTS_TMP_$(1) \
- tests/$(1)/%.ml $$(ALL_CMX) $$(GEN_OPT_LIBS)
- $$(OCAMLOPT) -c $$(OFLAGS) \
- $$(addprefix -I tests/,\
- $$($$(patsubst tests/$(1)/%_TESTS_TMP_$(1),%_TESTS_DIRS, $$<))) \
- $$(patsubst %.cmx,%.ml,$$@)
-
-tests/$(1)/%.opt: tests/$(1)/$$(PLUGIN_NAME)_TESTS_TMP_$(1) \
- $$($$(PLUGIN_NAME)_TESTS_LIB) \
- tests/$(1)/%.cmx \
- bin/toplevel.opt$$(EXE)
- $$(OCAMLOPT) $$(OLINKFLAGS) -o $$@ \
- $$(addprefix -I tests/,\
- $$($$(patsubst tests/$(1)/%_TESTS_TMP_$(1),%_TESTS_DIRS, $$<))) \
- $$(OPT_LIBS) $$(ALL_CMX) \
- $$($$(patsubst tests/$(1)/%_TESTS_TMP_$(1),%_TESTS_LIB, $$<)) \
- $$(STARTUPCMX) $$(patsubst %.opt,%.cmx,$$@)
-
-# See above for the dependency on all cmi
-tests/$(1)/%.cmo: tests/$(1)/$$(PLUGIN_NAME)_TESTS_TMP_$(1) \
- tests/$(1)/%.ml $$(ALL_CMI) $$(GEN_BYTE_LIBS)
- $$(OCAMLC) -c $$(BFLAGS) \
- $$(addprefix -I tests/,\
- $$($$(patsubst tests/$(1)/%_TESTS_TMP_$(1),%_TESTS_DIRS, $$<))) \
- $$(patsubst %.cmo,%.ml,$$@)
-
-tests/$(1)/%.byte: tests/$(1)/$$(PLUGIN_NAME)_TESTS_TMP_$(1) \
- $$($$(PLUGIN_NAME)_TESTS_LIB_BYTE) \
- tests/$(1)/%.cmo \
- bin/toplevel.byte$$(EXE)
- $$(OCAMLC) $$(BLINKFLAGS) -o $$@ \
- $$(addprefix -I tests/,\
- $$($$(patsubst tests/$(1)/%_TESTS_TMP_$(1),%_TESTS_DIRS, $$<))) \
- $$(BYTE_LIBS) $$(ALL_CMO) \
- $$($$(patsubst tests/$(1)/%_TESTS_TMP_$(1),%_TESTS_LIB_BYTE, $$<)) \
- $$(STARTUPCMO) $$(patsubst %.byte,%.cmo,$$@)
-
-endef #COMPILE_TESTS_ML_FILES
-
-$(foreach d,$(PLUGIN_TESTS_DIRS),$(eval $(call COMPILE_TESTS_ML_FILES,$d)))
+$(foreach d,$(PLUGIN_TESTS_DIRS),$(eval $(call COMPILE_TESTS_ML_FILES,$d,$(PLUGIN_NAME))))
endif # PLUGIN_ENABLE
diff --git a/tests/spec/rewrite_ensures.c b/tests/spec/rewrite_ensures.c
index cc7970291c4..2c65b84c557 100644
--- a/tests/spec/rewrite_ensures.c
+++ b/tests/spec/rewrite_ensures.c
@@ -1,6 +1,9 @@
-/* run.config
- DONTRUN: dependencies of .cmxs for tests are broken
+/* run.config_no_native_dynlink
EXECNOW: make -s tests/spec/rewrite_ensures.cmo
+ CMD: FRAMAC_DYN_PATH=tests/spec bin/toplevel.byte
+ OPT: -print
+*/
+/* run.config
EXECNOW: make -s tests/spec/rewrite_ensures.cmxs
CMD: FRAMAC_DYN_PATH=tests/spec bin/toplevel.opt
OPT: -print
--
GitLab