diff --git a/Makefile b/Makefile
index 38eefec0e91d155acd37a67ac01ac643af43af71..340b7d67badb8a1f15a9b36bb2b2cbcfb069d4fb 100644
--- a/Makefile
+++ b/Makefile
@@ -1301,11 +1301,9 @@ ALL_GUI_CMO= $(ALL_CMO) $(GRAPH_GUICMO) $(GUICMO)
ALL_GUI_CMX= $(patsubst %.cma,%.cmxa,$(ALL_GUI_CMO:.cmo=.cmx))
ifeq ($(LABLGTK_VERSION),3)
-ifeq ($(NATIVE_THREADS),yes)
THREAD=-thread
else
-THREAD=-vmthread
-endif
+THREAD=
endif
bin/viewer.byte$(EXE): BYTE_LIBS+= $(GRAPH_GUICMO)
@@ -1378,7 +1376,7 @@ include Makefile.generating
# Tests #
#########
-ifeq ($(PTESTSBEST),opt)
+ifeq ($(OCAMLBEST),opt)
PTESTS_FILES=ptests_config.cmi ptests_config.cmx ptests_config.o
else
PTESTS_FILES=ptests_config.cmi ptests_config.cmo
@@ -1400,9 +1398,9 @@ update_external_tests: external_tests
oracles: byte opt ptests
$(PRINT_MAKING) oracles
- ./bin/ptests.$(PTESTSBEST)$(EXE) -make "$(MAKE)" $(PLUGIN_TESTS_LIST) \
+ ./bin/ptests.$(OCAMLBEST)$(EXE) -make "$(MAKE)" $(PLUGIN_TESTS_LIST) \
> /dev/null 2>&1
- ./bin/ptests.$(PTESTSBEST)$(EXE) -make "$(MAKE)" -update \
+ ./bin/ptests.$(OCAMLBEST)$(EXE) -make "$(MAKE)" -update \
$(PLUGIN_TESTS_LIST)
btests: byte ./bin/ptests.byte$(EXE)
@@ -1412,13 +1410,13 @@ btests: byte ./bin/ptests.byte$(EXE)
tests_dist: dist ptests
$(PRINT_EXEC) ptests
- time -p ./bin/ptests.$(PTESTSBEST)$(EXE) -make "$(MAKE)" \
+ time -p ./bin/ptests.$(OCAMLBEST)$(EXE) -make "$(MAKE)" \
$(PLUGIN_TESTS_LIST)
# test only one test suite : make suite_tests
%_tests: opt ptests
$(PRINT_EXEC) ptests
- ./bin/ptests.$(PTESTSBEST)$(EXE) -make "$(MAKE)" $($*_TESTS_OPTS) $*
+ ./bin/ptests.$(OCAMLBEST)$(EXE) -make "$(MAKE)" $($*_TESTS_OPTS) $*
# full test suite
wp_TESTS_OPTS=-j 1
@@ -1993,8 +1991,8 @@ install:: install-lib-$(OCAMLBEST)
if [ -x bin/viewer.byte$(EXE) ] ; then \
$(CP) bin/viewer.byte$(EXE) $(BINDIR)/frama-c-gui.byte$(EXE); \
fi
- $(CP) bin/ptests.$(PTESTSBEST)$(EXE) \
- $(BINDIR)/ptests.$(PTESTSBEST)$(EXE)
+ $(CP) bin/ptests.$(OCAMLBEST)$(EXE) \
+ $(BINDIR)/ptests.$(OCAMLBEST)$(EXE)
if [ -x bin/fc-config$(EXE) ] ; then \
$(CP) bin/fc-config$(EXE) $(BINDIR)/frama-c-config$(EXE); \
fi
@@ -2031,7 +2029,7 @@ install:: install-lib-$(OCAMLBEST)
.PHONY: uninstall
uninstall::
$(PRINT_RM) installed binaries
- $(RM) $(BINDIR)/frama-c* $(BINDIR)/ptests.$(PTESTSBEST)$(EXE)
+ $(RM) $(BINDIR)/frama-c* $(BINDIR)/ptests.$(OCAMLBEST)$(EXE)
$(PRINT_RM) installed shared files
$(RM) -R $(FRAMAC_DATADIR)
$(PRINT_RM) installed libraries
@@ -2346,22 +2344,16 @@ PTESTS_SRC=ptests/ptests_config.ml ptests/ptests.ml
# that does not contain a 'tests' dir
PTESTS_CONFIG:= $(shell if test -d tests; then echo tests/ptests_config; fi)
-ifeq ($(NATIVE_THREADS),yes)
-PTEST_THREAD=-thread
-ptests: bin/ptests.$(PTESTSBEST)$(EXE) $(PTESTS_CONFIG)
-else
-PTEST_THREAD=-vmthread
-ptests: bin/ptests.byte$(EXE) $(PTESTS_CONFIG)
-endif
+ptests: bin/ptests.$(OCAMLBEST)$(EXE) $(PTESTS_CONFIG)
bin/ptests.byte$(EXE): $(PTESTS_SRC)
$(PRINT_LINKING) $@
- $(OCAMLC) -I ptests -dtypes $(PTEST_THREAD) -g -o $@ \
+ $(OCAMLC) -I ptests -dtypes -thread -g -o $@ \
unix.cma threads.cma str.cma dynlink.cma $^
bin/ptests.opt$(EXE): $(PTESTS_SRC)
$(PRINT_LINKING) $@
- $(OCAMLOPT) -I ptests -dtypes $(PTEST_THREAD) -o $@ \
+ $(OCAMLOPT) -I ptests -dtypes -thread -o $@ \
unix.cmxa threads.cmxa str.cmxa dynlink.cmxa $^
GENERATED+=ptests/ptests_config.ml tests/ptests_config
diff --git a/configure.in b/configure.in
index b109af187f96381f0df6e82a27d8294578f11935..54f3e157cd2d36381976271133d8258f25da720b 100644
--- a/configure.in
+++ b/configure.in
@@ -411,8 +411,6 @@ if test "$OCAML_OS_TYPE" = "Win32"; then
PLATFORM=Win32
OCAMLWIN32=yes
EXE=.exe
- # OCaml on Win32 does not support vmthreads, use native ones.
- HAS_NATIVE_THREADS=yes
else
OCAMLWIN32=no
if test "$OCAML_OS_TYPE" = "Cygwin"; then
@@ -429,21 +427,6 @@ else
fi
EXE=
fi
-
- # OCaml native threads
- AC_MSG_CHECKING([OCaml native threads])
- echo "let f = Thread.create (fun () -> ())" > test_native_threads.ml
- if
- ($OCAMLC -thread -o test_native_threads unix.cma threads.cma \
- test_native_threads.ml) 2> /dev/null
- then
- HAS_NATIVE_THREADS=yes
- AC_MSG_RESULT([ok.]);
- else
- HAS_NATIVE_THREADS=no
- AC_MSG_WARN([unsupported.]);
- fi
- rm -f test_native_threads*;
fi
# C and POSIX standard headers used by C bindings.
@@ -977,21 +960,6 @@ configure_library([LABLGTK],
configure_tool([DOT],[dot],[dot not found: you should install GraphViz],no)
-# Checking some other things which cannot be done too early
-###########################################################
-
-# Native version of ptests can be used only if
-# - a native compiler exists
-# - native threads are usable
-
-PTESTSBEST=byte
-if test \
- "$OCAMLBEST" = "opt" -a \
- "$HAS_NATIVE_THREADS" = "yes"; \
-then
- PTESTSBEST=opt;
-fi
-
########################
# Plug-in dependencies #
########################
@@ -1040,8 +1008,6 @@ AC_SUBST(CC)
AC_SUBST(EXTERNAL_PLUGINS)
-AC_SUBST(HAS_NATIVE_THREADS)
-AC_SUBST(PTESTSBEST)
AC_SUBST(LABLGTK_PATH)
# m4_foreach_w is not supported in some old autoconf versions.
diff --git a/share/Makefile.config.in b/share/Makefile.config.in
index 7370b7bcf278c1036f03aa5e305508f0127f0f37..a22fd9b13c70f632e3e45c1b23087daf19588524 100644
--- a/share/Makefile.config.in
+++ b/share/Makefile.config.in
@@ -89,9 +89,7 @@ HAS_OCAML407 ?=@HAS_OCAML407@
HAS_OCAML408 ?=@HAS_OCAML408@
PLATFORM ?=@PLATFORM@
-NATIVE_THREADS ?=@HAS_NATIVE_THREADS@
OCAMLWIN32 ?=@OCAMLWIN32@
-PTESTSBEST ?=@PTESTSBEST@
DEVELOPMENT ?=@DEVELOPMENT@
diff --git a/share/Makefile.dynamic_config.external b/share/Makefile.dynamic_config.external
index e76a1aa89899864ff5f1c29830e04a997b0f855c..f6fcc64d248232b764886887fef561006096b205 100644
--- a/share/Makefile.dynamic_config.external
+++ b/share/Makefile.dynamic_config.external
@@ -27,7 +27,7 @@ export FRAMAC_BYTE=$(BINDIR)/frama-c.byte$(EXE)
export FRAMAC_INCLUDES=-I "$(FRAMAC_LIBDIR)"
-export PTESTS=$(BINDIR)/ptests.$(PTESTSBEST)$(EXE)
+export PTESTS=$(BINDIR)/ptests.$(OCAMLBEST)$(EXE)
export FRAMAC_LIB=$(FRAMAC_LIBDIR)
export DOC_DIR=$(FRAMAC_SHARE)/doc/code
diff --git a/share/Makefile.dynamic_config.internal b/share/Makefile.dynamic_config.internal
index 6c50e7bba80c9ccea20a91c6c08111c773703ba3..425dc8b759137c69dd72c06bcaa90ba696374169 100644
--- a/share/Makefile.dynamic_config.internal
+++ b/share/Makefile.dynamic_config.internal
@@ -27,7 +27,7 @@ export FRAMAC_BYTE=$(FRAMAC_ROOT_SRCDIR)/bin/toplevel.byte$(EXE)
export FRAMAC_INCLUDES=$(addprefix -I $(call winpath,$(FRAMAC_ROOT_SRCDIR))/,$(FRAMAC_SRC_DIRS) lib)
-export PTESTS=$(FRAMAC_ROOT_SRCDIR)/bin/ptests.$(PTESTSBEST)$(EXE)
+export PTESTS=$(FRAMAC_ROOT_SRCDIR)/bin/ptests.$(OCAMLBEST)$(EXE)
export FRAMAC_LIB=$(FRAMAC_ROOT_SRCDIR)/lib/fc
export DOC_DIR=$(FRAMAC_ROOT_SRCDIR)/doc/code