diff --git a/Makefile b/Makefile
index cb79521c39e81f01e0a4a8c8136919990c1c62b1..3243857e73d1a94237f0d46dbac0403732583e19 100644
--- a/Makefile
+++ b/Makefile
@@ -241,8 +241,7 @@ DISTRIB_FILES:=\
$(wildcard src/kernel_internals/runtime/*.ml*)) \
$(wildcard src/kernel_services/abstract_interp/*.ml*) \
$(wildcard src/plugins/gui/*.ml*) \
- $(filter-out src/libraries/stdlib/FCDynlink.ml, \
- $(wildcard src/libraries/stdlib/*.ml*)) \
+ $(wildcard src/libraries/stdlib/*.ml*) \
$(wildcard src/libraries/utils/*.ml*) \
$(wildcard src/libraries/utils/*.c) \
$(wildcard src/libraries/project/*.ml*) \
@@ -361,60 +360,6 @@ endif
# Frama-C Kernel #
##################
-# Dynlink library
-#################
-
-GENERATED += src/libraries/stdlib/FCDynlink.ml
-
-ifeq ($(USABLE_NATIVE_DYNLINK),yes) # native dynlink works
-
-src/libraries/stdlib/FCDynlink.ml: \
- src/libraries/stdlib/dynlink_native_ok.ml share/Makefile.config
- $(CP_IF_DIFF) $< $@
- $(CHMOD_RO) $@
-
-else # native dynlink doesn't work
-
-ifeq ($(NATIVE_DYNLINK),yes) # native dynlink does exist but doesn't work
-src/libraries/stdlib/lib/FCDynlink.ml: \
- src/libraries/stdlib/dynlink_native_ko.ml share/Makefile.config
- $(CP_IF_DIFF) $< $@
- $(CHMOD_RO) $@
-
-else # no dynlink at all (for instance no native compiler)
-
-# Just for ocamldep
-src/libraries/stdlib/FCDynlink.ml: \
- src/libraries/stdlib/dynlink_native_ok.ml share/Makefile.config
- $(CP_IF_DIFF) $< $@
- $(CHMOD_RO) $@
-
-# Add two different rules for bytecode and native since
-# the file FCDynlink.ml is not built from the same file in these cases.
-
-src/libraries/stdlib/FCDynlink.cmo: \
- src/libraries/stdlib/dynlink_native_ok.ml share/Makefile.config
- $(CP_IF_DIFF) $< src/libraries/stdlib/FCDynlink.ml
- $(CHMOD_RO) src/libraries/stdlib/FCDynlink.ml
- $(PRINT_OCAMLC) $@
- $(OCAMLC) -c $(BFLAGS) src/libraries/stdlib/FCDynlink.ml
-
-src/libraries/stdlib/FCDynlink.cmx: \
- src/libraries/stdlib/dynlink_no_native.ml share/Makefile.config
- $(CP_IF_DIFF) $< src/libraries/stdlib/FCDynlink.ml
- $(CHMOD_RO) src/libraries/stdlib/FCDynlink.ml
- $(PRINT_OCAMLOPT) $@
- $(OCAMLOPT) -c $(OFLAGS) src/libraries/stdlib/FCDynlink.ml
-
-# force dependency order between these two files in order to not generate them
-# in parallel since each of them generates the same .ml file
-src/libraries/stdlib/FCDynlink.cmx: src/libraries/stdlib/FCDynlink.cmo
-src/libraries/stdlib/FCDynlink.o: src/libraries/stdlib/FCDynlink.cmx
-
-endif
-endif
-
-
# Libraries which could be compiled fully independently
#######################################################
@@ -1098,9 +1043,6 @@ MODULES_TODOC+=$(filter-out $(MODULES_NODOC),\
ALL_BATCH_CMO= $(filter-out src/kernel_internals/runtime/gui_init.cmo,\
$(ALL_CMO))
-# ALL_BATCH_CMX is not a translation of ALL_BATCH_CMO with cmo -> cmx
-# in case native dynlink is not available: dynamic plugin are linked
-# dynamically in bytecode and statically in native code...
ALL_BATCH_CMX= $(filter-out src/kernel_internals/runtime/gui_init.cmx,\
$(ALL_CMX))
diff --git a/Makefile.generating b/Makefile.generating
index bf8b8ad3bfe7681da10b64b647352d4678a7b1bd..941c74256d79726bc1f6bbf273cc5856ba26cfff 100644
--- a/Makefile.generating
+++ b/Makefile.generating
@@ -24,10 +24,6 @@ ptests/ptests_config.ml: Makefile.generating share/Makefile.config
$(PRINT_MAKING) $@
$(RM) $@
$(TOUCH) $@
- $(ECHO) \
- "let no_native_dynlink = " \
- $(subst yes,false,$(subst no,true,$(USABLE_NATIVE_DYNLINK))) ";;" \
- >> $@
$(CHMOD_RO) $@
tests/ptests_config: Makefile.generating share/Makefile.config
diff --git a/configure.in b/configure.in
index da93b28d2b51d63c0098dd5e43f8c526d2880112..d3b3e3cba28f29a62b3fc2a57ae5c3177b766b9f 100644
--- a/configure.in
+++ b/configure.in
@@ -602,10 +602,6 @@ REQUIRE_LABLGTK=
USE_LABLGTK=
HAS_LABLGTK=
-REQUIRE_NATIVE_DYNLINK=
-USE_NATIVE_DYNLINK=
-HAS_NATIVE_DYNLINK=uncheck
-
# Tool declarations
####################
@@ -875,81 +871,28 @@ configure_library([LABLGTK],
configure_tool([DOT],[dot],[dot not found: you should install GraphViz],no)
-# Native dynlink
-################
-
-define([force_static_plugins],
- [# compile statically all dynamic plug-ins
- # except contrary instructions
- [USE_NATIVE_DYNLINK]="";
- for plugin in m4_flatten(PLUGINS_LIST); do
- n=NAME_$plugin
- d=DYNAMIC_$plugin
- s=STATIC_$plugin
- eval np=\$$n
- eval dp=\$$d
- eval sp=\$$s
- if test "$dp" = "yes"; then
- if test "$sp" = "no"; then
- # force to be dynamic
- USE_NATIVE_DYNLINK="${USE_NATIVE_DYNLINK} $np";
- else
- eval STATIC_$plugin=yes;
- eval DYNAMIC_$plugin=no;
- fi
- fi
- done])
-
-configure_library([NATIVE_DYNLINK],
- [$OCAMLLIB/dynlink.cmxa],
- [native dynlink unavailable],
- yes,
- [force_static_plugins])
-
# Checking some other things which cannot be done too early
###########################################################
-# Usable native dynlink
-
-# Checking internal invariant
-if test "$HAS_NATIVE_DYNLINK" = "uncheck"; then
- AC_MSG_ERROR([Internal error with check of native dynlink. Please report.])
-fi
-
-HAS_USABLE_NATIVE_DYNLINK=no
+# Check that native dynlink works
-if test "$HAS_NATIVE_DYNLINK" != "no" ; then
- echo "let f x y = Dynlink.loadfile \"foo\"; ignore (Dynlink.is_native); abs_float (x -. y)" > test_dynlink.ml
- if ($OCAMLOPT -shared -linkall -o test_dynlink.cmxs test_dynlink.ml) \
- 2> /dev/null ; \
- then
- HAS_USABLE_NATIVE_DYNLINK=yes
- AC_MSG_RESULT([native dynlink works fine. Great.])
- else
- REQUIRE_USABLE_NATIVE_DYNLINK=$REQUIRE_NATIVE_DYNLINK
- USE_USABLE_NATIVE_DYNLINK=$USE_NATIVE_DYNLINK
- HAS_USABLE_NATIVE_DYNLINK=no
-# we know that dynlink does not work:
-# configure a dummy library "dynlink" in order to
-# configure plug-ins depending on dynlink in a proper way
- configure_library([USABLE_NATIVE_DYNLINK],
- [dynlink],
- [native dynlink unsupported on this platform],
- yes,
- [force_static_plugins])
- fi
- rm -f test_dynlink.*
+echo "let f x y = Dynlink.loadfile \"foo\"; ignore (Dynlink.is_native); abs_float (x -. y)" > test_dynlink.ml
+if ($OCAMLOPT -shared -linkall -o test_dynlink.cmxs test_dynlink.ml) \
+ 2> /dev/null ; \
+then
+ AC_MSG_RESULT([native dynlink works fine. Great.])
+else
+ AC_MSG_ERROR([native dynlink does not work.])
fi
+rm -f test_dynlink.*
# Native version of ptests can be used only if
# - a native compiler exists
-# - native dynlink is usable
# - native threads are usable
PTESTSBEST=byte
if test \
"$OCAMLBEST" = "opt" -a \
- "$HAS_USABLE_NATIVE_DYNLINK" = "yes" -a \
"$HAS_NATIVE_THREADS" = "yes"; \
then
PTESTSBEST=opt;
@@ -999,7 +942,6 @@ AC_SUBST(CC)
AC_SUBST(EXTERNAL_PLUGINS)
-AC_SUBST(HAS_USABLE_NATIVE_DYNLINK)
AC_SUBST(HAS_NATIVE_THREADS)
AC_SUBST(PTESTSBEST)
AC_SUBST(LABLGTK_PATH)
diff --git a/doc/userman/user-plugins.tex b/doc/userman/user-plugins.tex
index 036b3a47f7099cd722715168ebb879db328d0386..e84d9e1021d955f8297e3df4d278b0cd8430f07a 100644
--- a/doc/userman/user-plugins.tex
+++ b/doc/userman/user-plugins.tex
@@ -24,8 +24,7 @@ Sections~\ref{sec:install-internal} and~\ref{sec:install-external}).
dynamic}:]\index{Plug-in!Static|bfit}\index{Plug-in!Dynamic|bfit} static
plug-ins are statically linked into a \FramaC executable (see
Section~\ref{sec:modes}) while dynamic plug-ins are loaded by an executable
- when it is run. Despite only being available on some environments (see
- Section~\ref{sec:install}), dynamic plug-ins are more flexible as explained
+ when it is run. Dynamic plug-ins are more flexible as explained
in Section~\ref{sec:use-plugins}.
\end{description}
@@ -46,8 +45,7 @@ entire \FramaC configuration to fail. You can also use the option
Internal dynamic plug-ins may be linked statically. This is achieved by passing
{\tt configure} the option \texttt{-{}-with-<plug-in name>-static}. It is also
possible to force all dynamic plug-ins to be linked statically with the option
-\optiondef{-{}-}{with-all-static}. This option is set by default on systems
-that do not support native dynamic loading.
+\optiondef{-{}-}{with-all-static}.
\section{Installing External Plug-ins}\label{sec:install-external}
\index{Plug-in!External}
@@ -65,15 +63,7 @@ sequence of commands \texttt{make \&\& make install}, possibly preceded by
plug-in's documentation for installation instructions.
External plug-ins are always dynamic plug-ins\index{Plug-in!Dynamic} by
-default. On systems where native dynamic linking is not supported, a new
-executable, called \texttt{frama-c-<plug-in name>}\footnote{With the extension
- \texttt{.exe} on Windows OS}, is automatically generated when an external
-plug-in is compiled. This executable contains the \FramaC kernel, all the
-static plug-ins\index{Plug-in!Static} previously installed and the external
-plug-in. On systems where native dynamic linking is available, this executable
-is not necessary for normal use.
-% but it may be generated with the command \texttt{make static}.
-
+default.
External dynamic plug-ins may be configured and compiled at the same time as
the \FramaC kernel by using the option
\texttt{-{}-enable-external=<path-to-plugin>}
diff --git a/doc/userman/user-start.tex b/doc/userman/user-start.tex
index dde8a043c8fafaf55a94261271fc7ac0a2409c13..ea67dda29a73d7892daf71e03a1896e514535abf 100644
--- a/doc/userman/user-start.tex
+++ b/doc/userman/user-start.tex
@@ -45,8 +45,7 @@ may be found in the file \texttt{INSTALL} of the source distribution.
Support for some plug-ins in native compilation mode (see
Section~\ref{sec:modes})\index{Native-compiled} requires the so-called
- \emph{native dynamic linking} feature of \caml. It is not available in all
- supported platforms.
+ \emph{native dynamic linking} feature of \caml.
\item[\tool{Gtk}-related
packages:]\codeidx{GTK+}\codeidx{Lablgtk}\codeidx{GtkSourceView} \tool{\sc
gtk+}\footnote{\url{http://www.gtk.org}} version 2.4 or higher,
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 9ac9bca0bf5f6dd811add4be4b12e8dfc85e3d57..0e46336feb75f248568ad142ed0dac20383e1910 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -538,6 +538,7 @@ src/libraries/project/state_topological.ml: MODIFIED_OCAMLGRAPH
src/libraries/project/state_topological.mli: MODIFIED_OCAMLGRAPH
src/libraries/stdlib/FCBuffer.ml: OCAML_STDLIB
src/libraries/stdlib/FCBuffer.mli: OCAML_STDLIB
+src/libraries/stdlib/FCDynlink.ml: CEA_LGPL
src/libraries/stdlib/FCDynlink.mli: CEA_LGPL
src/libraries/stdlib/FCHashtbl.ml: CEA_LGPL
src/libraries/stdlib/FCHashtbl.mli: CEA_LGPL
@@ -546,9 +547,6 @@ src/libraries/stdlib/FCMap.mli: OCAML_STDLIB
src/libraries/stdlib/FCSet.ml: OCAML_STDLIB
src/libraries/stdlib/FCSet.mli: OCAML_STDLIB
src/libraries/stdlib/README.md: .ignore
-src/libraries/stdlib/dynlink_native_ko.ml: CEA_LGPL
-src/libraries/stdlib/dynlink_native_ok.ml: CEA_LGPL
-src/libraries/stdlib/dynlink_no_native.ml: CEA_LGPL
src/libraries/stdlib/extlib.ml: CEA_LGPL
src/libraries/stdlib/extlib.mli: CEA_LGPL
src/libraries/stdlib/integer.ml: CEA_LGPL
diff --git a/ptests/ptests.ml b/ptests/ptests.ml
index 416586591b83eddaef2bf6457f2dfd27c91bbdae..5a4b796a0d4bbda646553db648767e236c4786c4 100644
--- a/ptests/ptests.ml
+++ b/ptests/ptests.ml
@@ -133,18 +133,6 @@ let opt_to_byte toplevel =
let opt_to_byte_options options =
str_global_replace regex_cmxs "\\1.cmo\\2" options
-let needs_byte =
- let load_something = Str.regexp ".*-load-\\(\\(script\\)\\|\\(module\\)\\)" in
- fun options ->
- Ptests_config.no_native_dynlink &&
- str_string_match load_something options 0
-
-let execnow_needs_byte =
- let make_cmxs = Str.regexp ".*make.*[.]cmxs" in
- fun cmd ->
- Ptests_config.no_native_dynlink &&
- str_string_match make_cmxs cmd 0
-
let execnow_opt_to_byte cmd =
let cmd = opt_to_byte cmd in
opt_to_byte_options cmd
@@ -924,8 +912,7 @@ let basic_command_string =
command.log_files <- logfiles;
let has_ptest_file_t, toplevel = replace_macros macros command.toplevel in
let has_ptest_file_o, options = replace_macros macros command.options in
- let needs_byte = !use_byte || needs_byte options in
- let toplevel = if needs_byte then opt_to_byte toplevel else toplevel in
+ let toplevel = if !use_byte then opt_to_byte toplevel else toplevel in
let options =
if str_string_match contains_toplevel_or_frama_c command.toplevel 0
then begin
@@ -934,7 +921,7 @@ let basic_command_string =
"-check " ^ opt_pre ^ " " ^ options ^ " " ^ opt_post
end else options
in
- let options = if needs_byte then opt_to_byte_options options else options in
+ let options = if !use_byte then opt_to_byte_options options else options in
if has_ptest_file_t || has_ptest_file_o || command.execnow then
toplevel ^ " " ^ options
else
@@ -1247,7 +1234,7 @@ let do_command command =
then begin
remove_execnow_results execnow;
let cmd =
- if !use_byte || execnow_needs_byte execnow.ex_cmd then
+ if !use_byte then
execnow_opt_to_byte execnow.ex_cmd
else
execnow.ex_cmd
diff --git a/share/Makefile.config.in b/share/Makefile.config.in
index afac49c37413cca4feb149e058a187c02620fbe1..536b4b06e74d1b0c6ecd635dfe0689a336d9d8b1 100644
--- a/share/Makefile.config.in
+++ b/share/Makefile.config.in
@@ -76,8 +76,6 @@ OCAMLLIB ?=@OCAMLLIB@
# either opt or byte
OCAMLBEST ?=@OCAMLBEST@
OCAMLVERSION ?=@OCAMLVERSION@
-NATIVE_DYNLINK ?=@HAS_NATIVE_DYNLINK@
-USABLE_NATIVE_DYNLINK ?=@HAS_USABLE_NATIVE_DYNLINK@
NATIVE_THREADS ?=@HAS_NATIVE_THREADS@
OCAMLWIN32 ?=@OCAMLWIN32@
PTESTSBEST ?=@PTESTSBEST@
diff --git a/share/Makefile.dynamic b/share/Makefile.dynamic
index 96552203d29dffda6bbc379c237b01acbf72c34f..f051c02f2d1ef1e5a9a77e205368aebce4a4f20b 100644
--- a/share/Makefile.dynamic
+++ b/share/Makefile.dynamic
@@ -37,10 +37,6 @@ ifndef PLUGIN_DYNAMIC
PLUGIN_DYNAMIC :=yes
endif
-ifeq ($(NATIVE_DYNLINK),no)
-USABLE_NATIVE_DYNLINK ?=no
-endif
-
#Do not generate documentation for this.
PLUGIN_UNDOC:=$(PLUGIN_UNDOC)
@@ -135,12 +131,7 @@ $(PLUGIN_DIR)/tests/ptests_config: $(PTESTS_DEP)
$(MKDIR) tests
$(RM) $$@
$(ECHO) "DEFAULT_SUITES=" $(PLUGIN_TESTS_DIRS) > $$@
- if test "$(USABLE_NATIVE_DYNLINK)" = "yes" \
- -o "$(FRAMAC_INTERNAL)" = "yes"; then \
- $(ECHO) "TOPLEVEL_PATH=$(FRAMAC_OPT)" >> $$@; \
- else \
- $(ECHO) "TOPLEVEL_PATH=./frama-c-$(PLUGIN_NAME).$(OCAMLBEST)$(EXE)\";;" >> $$@; \
- fi
+ $(ECHO) "TOPLEVEL_PATH=$(FRAMAC_OPT)" >> $$@;
$(ECHO) "FRAMAC_SHARE=$(FRAMAC_SHARE)" >> $$@
$(ECHO) "FRAMAC_LIB=$(FRAMAC_LIB)" >> $$@
if test "$(FRAMAC_INTERNAL)" = "no"; then \
@@ -251,11 +242,7 @@ $(PLUGIN_NAME)_CLEAN_DYNAMIC:
dist-clean distclean: $(PLUGIN_DIR)/$(PLUGIN_NAME)_DIST_CLEAN
-ifeq ($(USABLE_NATIVE_DYNLINK),no)
-STATIC=static
-else
STATIC=
-endif
all:: $(PLUGIN_DIR)/.depend byte $(OCAMLBEST) gui $(STATIC) plugins_ptests_config
diff --git a/share/Makefile.plugin.template b/share/Makefile.plugin.template
index c1517f8ff86c630182a71b3658713fdaf5fea74f..093fd027ea2ea40df7bee84d2962f15affd29d30 100644
--- a/share/Makefile.plugin.template
+++ b/share/Makefile.plugin.template
@@ -318,7 +318,7 @@ else
TARGET_TOP_CMXA:=
endif
-ifeq ("$(USABLE_NATIVE_DYNLINK) $(PLUGIN_DYNAMIC)","yes yes")
+ifeq ("$(PLUGIN_DYNAMIC)","yes")
TARGET_TOP_CMXS:= $(TARGET_TOP_CMX:.cmx=.cmxs)
else
TARGET_TOP_CMXS:=
@@ -332,7 +332,7 @@ TARGET_GUI_CMI:= $(TARGET_GUI_CMO:.cmo=.cmi)
TARGET_GUI_CMX:= $(TARGET_GUI_CMO:.cmo=.cmx)
TARGET_GUI_CMA:= $(TARGET_GUI_CMO:.cmo=.cma)
TARGET_GUI_CMXA:= $(TARGET_GUI_CMX:.cmx=.cmxa)
-ifeq ("$(USABLE_NATIVE_DYNLINK) $(PLUGIN_DYNAMIC)","yes yes")
+ifeq ("$(PLUGIN_DYNAMIC)","yes")
TARGET_GUI_CMXS:= $(TARGET_GUI_CMO:.cmo=.cmxs)
else
TARGET_GUI_CMXS:=
@@ -467,7 +467,7 @@ META.$(PLUGIN_PKG).NATIVE :=@PLUGIN_NAME@.cmxa
else
META.$(PLUGIN_PKG).NATIVE :=@PLUGIN_NAME@.cmx
endif
-ifeq ("$(USABLE_NATIVE_DYNLINK) $(PLUGIN_DYNAMIC)","yes yes")
+ifeq ("$(PLUGIN_DYNAMIC)","yes")
META.$(PLUGIN_PKG).PLUGIN :=@PLUGIN_NAME@.cmxs
endif
@@ -573,7 +573,7 @@ $(TARGET_TOP_CMX): $(PLUGIN_CMX) \
$(@PLUGIN_NAME@_TARGET_OFLAGS) \
$(@PLUGIN_NAME@_CMI_ONLY) $(@PLUGIN_NAME@_CMX)
-ifeq ("$(USABLE_NATIVE_DYNLINK) $(PLUGIN_DYNAMIC)","yes yes")
+ifeq ("$(PLUGIN_DYNAMIC)","yes")
$(TARGET_TOP_CMXS): $(TARGET_TOP_CMX) $(PLUGIN_EXTRA_OPT)
$(PRINT_PACKING) $@
$(OCAMLOPT) -o $(call winpath,$@) -shared \
@@ -631,7 +631,7 @@ $(TARGET_GUI_CMX): $(PLUGIN_GUI_CMX) $(TARGET_CMI) $(TARGET_GUI_CMI)
$(@PLUGIN_NAME@_GUI_CMI_ONLY) \
$(@PLUGIN_NAME@_GUI_CMX)
-ifeq ("$(USABLE_NATIVE_DYNLINK) $(PLUGIN_DYNAMIC)","yes yes")
+ifeq ("$(PLUGIN_DYNAMIC)","yes")
$(TARGET_GUI_CMXS): $(TARGET_GUI_CMX)
$(PRINT_PACKING) $@
$(MKDIR) $(PLUGIN_LIB_DIR)/gui
@@ -980,7 +980,6 @@ PLUGIN_DYN_GUI_CMO_LIST += $(TARGET_GUI_CMO)
endif #EXTRA_BYTE
endif #HAS_GUI
-ifeq ($(USABLE_NATIVE_DYNLINK),yes)
PLUGIN_DYN_DEP_GUI_CMX_LIST += $(PLUGIN_GUI_CMX)
PLUGIN_DYN_CMX_LIST += $(TARGET_TOP_CMXS) $(TARGET_TOP_CMX)
# If P1 depends on P2, then dynamically link P1.cmxs requires to have
@@ -990,16 +989,7 @@ PLUGIN_DYN_CMX_LIST += $(TARGET_TOP_CMXA)
endif #EXTRA_OPT
ifeq ($(HAS_GUI),yes)
PLUGIN_DYN_GUI_CMX_LIST += $(TARGET_GUI_CMXS)
-endif
-else # No native dynlink: use a static version
-PLUGIN_CMX_LIST += $(TARGET_TOP_CMX)
-ifdef PLUGIN_EXTRA_OPT
-EXTRA_OPT_LIBS+= $(PLUGIN_EXTRA_OPT)
-endif
-ifeq ($(HAS_GUI),yes)
-PLUGIN_GUI_CMX_LIST += $(TARGET_GUI_CMX)
endif # HAS_GUI
-endif # USABLE_NATIVE_DYNLINK
else # Normal plugin
PLUGIN_LIST += $(PLUGIN_DIR)/@PLUGIN_NAME@
diff --git a/src/libraries/stdlib/dynlink_native_ok.ml b/src/libraries/stdlib/FCDynlink.ml
similarity index 100%
rename from src/libraries/stdlib/dynlink_native_ok.ml
rename to src/libraries/stdlib/FCDynlink.ml
diff --git a/src/libraries/stdlib/dynlink_native_ko.ml b/src/libraries/stdlib/dynlink_native_ko.ml
deleted file mode 100644
index 2e5f1990ade7dcf2cf75bac01d23a0bb8dec7a00..0000000000000000000000000000000000000000
--- a/src/libraries/stdlib/dynlink_native_ko.ml
+++ /dev/null
@@ -1,98 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2016 *)
-(* CEA (Commissariat à l'énergie atomique et aux énergies *)
-(* alternatives) *)
-(* *)
-(* 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). *)
-(* *)
-(**************************************************************************)
-
-(* Implementation of [FCDynlink] compatible with OCaml >=3.11
- whenever [Dynlink] **does not** correctly work. *)
-
-module type OldDynlink = sig
- val loadfile : string -> unit
- val allow_unsafe_modules : bool -> unit
- val init : unit -> unit
- val add_interfaces: string list -> string list -> unit
- val digest_interface : string -> string list -> Digest.t
-end
-
-exception Unsupported_Feature of string
-let fail s = fun _ -> raise (Unsupported_Feature s)
-
-let is_native = Dynlink.is_native
-
-let adapt_filename =
- if is_native then fail "adapt_filename" else Dynlink.adapt_filename
-
-let loadfile = if is_native then fail "loadfile" else Dynlink.loadfile
-
-let loadfile_private =
- if is_native then fail "loadfile_private" else Dynlink.loadfile_private
-
-let allow_unsafe_modules =
- if is_native then fail "allow_unsafe_modules"
- else Dynlink.allow_unsafe_modules
-
-let init = if is_native then fail "init" else Dynlink.init
-
-let clear_available_units =
- if is_native then fail "clear_available_units"
- else Dynlink.clear_available_units
-
-let add_available_units =
- if is_native then fail "add_available_units" else Dynlink.add_available_units
-
-let add_interfaces =
- if is_native then fail "add_interfaces" else Dynlink.add_interfaces
-
-let default_available_units =
- if is_native then fail "default_available_units"
- else Dynlink.default_available_units
-
-let prohibit = if is_native then fail "prohibit" else Dynlink.prohibit
-let allow_only = if is_native then fail "allow_only" else Dynlink.allow_only
-
-type linking_error = Dynlink.linking_error =
- Undefined_global of string
- | Unavailable_primitive of string
- | Uninitialized_global of string
-
-type error = Dynlink.error =
- Not_a_bytecode_file of string
- | Inconsistent_import of string
- | Unavailable_unit of string
- | Unsafe_file
- | Linking_error of string * linking_error
- | Corrupted_interface of string
- | File_not_found of string
- | Cannot_open_dll of string
- | Inconsistent_implementation of string
-
-exception Error = Dynlink.Error
-
-let error_message =
- if is_native then fail "error_message" else Dynlink.error_message
-
-let digest_interface =
- if is_native then fail "digest_interface" else Dynlink.digest_interface
-
-(*
-Local Variables:
-compile-command: "make -C ../../.."
-End:
-*)
diff --git a/src/libraries/stdlib/dynlink_no_native.ml b/src/libraries/stdlib/dynlink_no_native.ml
deleted file mode 100644
index f4b9a3a3b0964a59a83e4b00aedc6fa9b3c2e0f8..0000000000000000000000000000000000000000
--- a/src/libraries/stdlib/dynlink_no_native.ml
+++ /dev/null
@@ -1,69 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2016 *)
-(* CEA (Commissariat à l'énergie atomique et aux énergies *)
-(* alternatives) *)
-(* *)
-(* 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). *)
-(* *)
-(**************************************************************************)
-
-(* Implementation of [FCDynlink] when no dynlink is available *)
-
-module type OldDynlink = sig
- val loadfile : string -> unit
- val allow_unsafe_modules : bool -> unit
- val init : unit -> unit
- val add_interfaces: string list -> string list -> unit
- val digest_interface : string -> string list -> Digest.t
-end
-
-exception Unsupported_Feature of string
-let fail s = fun _ -> raise (Unsupported_Feature s)
-
-let is_native = true
-let adapt_filename = fail "adapt_filename"
-
-let loadfile = fail "loadfile"
-let allow_unsafe_modules = fail "allow_unsafe_modules"
-let init = fail "init"
-let add_interfaces = fail "add_interfaces"
-
-type linking_error =
- Undefined_global of string
- | Unavailable_primitive of string
- | Uninitialized_global of string
-
-type error =
- Not_a_bytecode_file of string
- | Inconsistent_import of string
- | Unavailable_unit of string
- | Unsafe_file
- | Linking_error of string * linking_error
- | Corrupted_interface of string
- | File_not_found of string
- | Cannot_open_dll of string
- | Inconsistent_implementation of string
-
-exception Error of error
-
-let error_message = fail "error_message"
-let digest_interface = fail "digest_interface"
-
-(*
-Local Variables:
-compile-command: "make -C ../../.."
-End:
-*)
diff --git a/tests/misc/bts1347.i b/tests/misc/bts1347.i
index 40212b1183e559d0f5e2f584e113151507eea5e1..15a08daaf6e9f4b2225655aa490fa21b09688c8f 100644
--- a/tests/misc/bts1347.i
+++ b/tests/misc/bts1347.i
@@ -1,7 +1,3 @@
-/* run.config_no_native_dynlink
- CMD: bin/toplevel.byte
- OPT: -load-script tests/misc/bts1347.ml -val-show-progress -then -report
-*/
/* run.config
OPT: -load-script tests/misc/bts1347.ml -val-show-progress -then -report
*/
diff --git a/tests/misc/ensures.i b/tests/misc/ensures.i
index 4ec057666a52cb05ee91e1d6d92ee5d25e48106c..140bf8122f031aa574e460218275fceb1fb3112b 100644
--- a/tests/misc/ensures.i
+++ b/tests/misc/ensures.i
@@ -1,7 +1,3 @@
-/* run.config_no_native_dynlink
- CMD: bin/toplevel.byte
- OPT: -load-script tests/misc/ensures.ml
-*/
/* run.config
OPT: -load-script tests/misc/ensures.ml
*/
diff --git a/tests/misc/oracle/bts1347.res.oracle b/tests/misc/oracle/bts1347.res.oracle
index e0adc1c1a24d3e9a8632ba96810ea7d96d49ff26..fdc4af8be891f0b086b32f84931bd9383c90b51b 100644
--- a/tests/misc/oracle/bts1347.res.oracle
+++ b/tests/misc/oracle/bts1347.res.oracle
@@ -5,7 +5,7 @@
[value] Initial state computed
[value:initial-state] Values of globals at initialization
-tests/misc/bts1347.i:9:[value] warning: out of bounds read. assert \valid_read(x);
+tests/misc/bts1347.i:5:[value] warning: out of bounds read. assert \valid_read(x);
[value] Recording results for f
[value] done for function f
[value] Analyzing an incomplete application starting at g
@@ -13,7 +13,7 @@ tests/misc/bts1347.i:9:[value] warning: out of bounds read. assert \valid_read(x
[value] Initial state computed
[value:initial-state] Values of globals at initialization
-tests/misc/bts1347.i:10:[value] warning: out of bounds read. assert \valid_read(tmp);
+tests/misc/bts1347.i:6:[value] warning: out of bounds read. assert \valid_read(tmp);
(tmp from x++)
[value] Recording results for g
[value] done for function g
@@ -23,22 +23,22 @@ tests/misc/bts1347.i:10:[value] warning: out of bounds read. assert \valid_read(
--- Properties of Function 'f'
--------------------------------------------------------------------------------
-[ Dead ] Assertion 'emitter' (file tests/misc/bts1347.i, line 9)
+[ Dead ] Assertion 'emitter' (file tests/misc/bts1347.i, line 5)
Locally valid, but unreachable.
By Value because:
- - Unreachable return (file tests/misc/bts1347.i, line 9)
-[Unreachable] Unreachable return (file tests/misc/bts1347.i, line 9)
+ - Unreachable return (file tests/misc/bts1347.i, line 5)
+[Unreachable] Unreachable return (file tests/misc/bts1347.i, line 5)
by Value.
--------------------------------------------------------------------------------
--- Properties of Function 'g'
--------------------------------------------------------------------------------
-[ - ] Assertion 'Value,mem_access' (file tests/misc/bts1347.i, line 10)
+[ - ] Assertion 'Value,mem_access' (file tests/misc/bts1347.i, line 6)
tried with Value.
-[ Partial ] Assertion 'emitter' (file tests/misc/bts1347.i, line 10)
+[ Partial ] Assertion 'emitter' (file tests/misc/bts1347.i, line 6)
By emitter, with pending:
- - Assertion 'Value,mem_access' (file tests/misc/bts1347.i, line 10)
+ - Assertion 'Value,mem_access' (file tests/misc/bts1347.i, line 6)
--------------------------------------------------------------------------------
--- Status Report Summary
@@ -54,8 +54,8 @@ tests/misc/bts1347.i:10:[value] warning: out of bounds read. assert \valid_read(
[value] Initial state computed
[value:initial-state] Values of globals at initialization
-tests/misc/bts1347.i:9:[value] warning: out of bounds read. assert \valid_read(x);
-tests/misc/bts1347.i:9:[value] assertion 'emitter' got status valid.
+tests/misc/bts1347.i:5:[value] warning: out of bounds read. assert \valid_read(x);
+tests/misc/bts1347.i:5:[value] assertion 'emitter' got status valid.
[value] Recording results for f
[value] done for function f
[value] Analyzing an incomplete application starting at g
@@ -63,8 +63,8 @@ tests/misc/bts1347.i:9:[value] assertion 'emitter' got status valid.
[value] Initial state computed
[value:initial-state] Values of globals at initialization
-tests/misc/bts1347.i:10:[value] warning: out of bounds read. assert \valid_read(tmp);
+tests/misc/bts1347.i:6:[value] warning: out of bounds read. assert \valid_read(tmp);
(tmp from x++)
-tests/misc/bts1347.i:10:[value] assertion 'emitter' got status valid.
+tests/misc/bts1347.i:6:[value] assertion 'emitter' got status valid.
[value] Recording results for g
[value] done for function g
diff --git a/tests/misc/oracle/ensures.res.oracle b/tests/misc/oracle/ensures.res.oracle
index 9390ae5f9942b793cdb345a1ef59a313fea90bcf..411f00dd006d5ada62aafc58389aa740e0ed9a69 100644
--- a/tests/misc/oracle/ensures.res.oracle
+++ b/tests/misc/oracle/ensures.res.oracle
@@ -5,7 +5,7 @@
[value] Initial state computed
[value:initial-state] Values of globals at initialization
-tests/misc/ensures.i:8:[value] warning: function main: postcondition got status invalid.
+tests/misc/ensures.i:4:[value] warning: function main: postcondition got status invalid.
[value] done for function main
[kernel] Frama_C_bzero: behavior default!
VALID according to Frama-C kernel (under hypotheses)
diff --git a/tests/misc/remove_status_hyps.i b/tests/misc/remove_status_hyps.i
index 49b7c024a77ce9753b858a935d71157dbe4d553b..65348944a6d4a5ede92bee270d3aa2c8352a3070 100644
--- a/tests/misc/remove_status_hyps.i
+++ b/tests/misc/remove_status_hyps.i
@@ -1,7 +1,3 @@
-/* run.config_no_native_dynlink
- CMD: bin/toplevel.byte
- OPT: -load-script tests/misc/remove_status_hyps.ml
-*/
/* run.config
OPT: -load-script tests/misc/remove_status_hyps.ml
*/
diff --git a/tests/saveload/load_one.i b/tests/saveload/load_one.i
index 88f34ff79901f35b0d455e4981bd7a0f632ca6d9..7e7668faf7b8af9e3f035316291821284e65d018 100644
--- a/tests/saveload/load_one.i
+++ b/tests/saveload/load_one.i
@@ -1,7 +1,3 @@
-/* run.config_no_native_dynlink
- CMD: bin/toplevel.byte
- OPT: -load-script tests/saveload/load_one.ml -val-show-progress
-*/
/* run.config
OPT: -load-script tests/saveload/load_one.ml -val-show-progress
*/
diff --git a/tests/saveload/oracle/load_one.res.oracle b/tests/saveload/oracle/load_one.res.oracle
index c486c8b39c26cc8913370c15bf0fa531e6211e4b..6e0e457dd0ae8080bb184e16539f883dfac17f46 100644
--- a/tests/saveload/oracle/load_one.res.oracle
+++ b/tests/saveload/oracle/load_one.res.oracle
@@ -6,17 +6,17 @@
[value] Initial state computed
[value:initial-state] Values of globals at initialization
G ∈ {0}
-tests/saveload/load_one.i:20:[value] assertion got status valid.
+tests/saveload/load_one.i:16:[value] assertion got status valid.
[value] computing for function f <- main.
- Called from tests/saveload/load_one.i:22.
+ Called from tests/saveload/load_one.i:18.
[value] Recording results for f
[value] Done for function f
[value] computing for function f <- main.
- Called from tests/saveload/load_one.i:23.
+ Called from tests/saveload/load_one.i:19.
[value] Recording results for f
[value] Done for function f
[value] computing for function f <- main.
- Called from tests/saveload/load_one.i:24.
+ Called from tests/saveload/load_one.i:20.
[value] Recording results for f
[value] Done for function f
[value] Recording results for main