Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
38810ff7
Commit
38810ff7
authored
Mar 16, 2010
by
Francois Bobot
Browse files
dynlink_compat : en faisant un vrai test de ocaml 3.11 ou superieur
parent
2278ee78
Changes
5
Hide whitespace changes
Inline
Side-by-side
Makefile.in
View file @
38810ff7
...
...
@@ -52,12 +52,22 @@ OCAMLVERSION = @OCAMLVERSION@
CAMLP4
=
@CAMLP4O@
PSVIEWER
=
@PSVIEWER@
PDFVIEWER
=
@PDFVIEWER@
DYNLINK
=
@DYNLINK@
ifeq
($(DYNLINK),Dynlink)
DYNLINKBFLAGS
=
dynlink.cma
DYNLINKOFLAGS
=
dynlink.cmxa
else
DYNLINKBFLAGS
=
DYNLINKOFLAGS
=
endif
INCLUDES
=
-I
src/core
-I
src/util
-I
src/parser
-I
src/output
\
-I
src/transform
-I
src/programs
-I
src
BFLAGS
=
-w
Aelz
-dtypes
-g
$(INCLUDES)
@INCLUDEGTK2@
-I
+threads @OCAMLGRAPHLIB@ str.cma unix.cma
dynlink.cma
BFLAGS
=
-w
Aelz
-dtypes
-g
$(INCLUDES)
@INCLUDEGTK2@
-I
+threads @OCAMLGRAPHLIB@ str.cma unix.cma
$(DYNLINKBFLAGS)
# no -warn-error because some do not compile all files (e.g. those linked to APRON)
OFLAGS
=
-w
Aelz
-dtypes
$(INCLUDES)
@INCLUDEGTK2@
-I
+threads @OCAMLGRAPHLIB@ str.cmxa unix.cmxa
dynlink.cmxa
OFLAGS
=
-w
Aelz
-dtypes
$(INCLUDES)
@INCLUDEGTK2@
-I
+threads @OCAMLGRAPHLIB@ str.cmxa unix.cmxa
$(DYNLINKOFLAGS)
COQC7
=
@COQC7@
COQC8
=
@COQC8@
...
...
@@ -69,7 +79,7 @@ GENERATED = src/version.ml src/parser/parser.mli src/parser/parser.ml \
src/parser/lexer.ml src/output/driver_lexer.ml
\
src/output/driver_parser.mli src/output/driver_parser.ml
\
src/programs/pgm_lexer.ml src/programs/pgm_parser.mli
\
src/programs/pgm_parser.ml
src/programs/pgm_parser.ml
src/util/dynlink_compat.ml
# main targets
##############
...
...
@@ -110,7 +120,8 @@ doc/version.tex src/version.ml: Version version.sh config.status
CORE_CMO
:=
ident.cmo ty.cmo term.cmo theory.cmo pretty.cmo
CORE_CMO
:=
$(
addprefix
src/core/,
$(CORE_CMO)
)
UTIL_CMO
:=
pp.cmo loc.cmo util.cmo hashcons.cmo sysutil.cmo
UTIL_CMO
:=
pp.cmo loc.cmo util.cmo hashcons.cmo sysutil.cmo
\
dynlink_compat.cmo
UTIL_CMO
:=
$(
addprefix
src/util/,
$(UTIL_CMO)
)
PARSER_CMO
:=
parser.cmo lexer.cmo typing.cmo
...
...
@@ -590,6 +601,9 @@ config.status: configure
configure
:
configure.in
autoconf
src/util/dynlink_compat.ml
:
src/util/dynlink_compat.ml.in config.status
./config.status
# clean and depend
##################
...
...
configure.in
View file @
38810ff7
...
...
@@ -102,6 +102,18 @@ case $OCAMLVERSION in
FORPACK="-for-pack Graph";;
esac
#Dynlink is native?
case $OCAMLVERSION in
3.08*|3.09*|3.10*)
DYNLINK="Dynlink_"
enable_dynlink=no;;
#Dynlink_ is used for compatibility in /src/util/dynlink_compat.ml.in
*)
DYNLINK="Dynlink"
enable_dynlink=yes
esac
# Ocaml library path
# old way: OCAMLLIB=`$OCAMLC -v | tail -1 | cut -f 4 -d ' ' | tr -d '\\r'`
OCAMLLIB=`$OCAMLC -where | tr -d '\\r'`
...
...
@@ -446,6 +458,7 @@ AC_SUBST(OCAMLGRAPHLIB)
AC_SUBST(LABLGTK2)
AC_SUBST(INCLUDEGTK2)
AC_SUBST(OCAMLWEB)
AC_SUBST(DYNLINK)
# AC_SUBST(CAMLP4O)
# AC_SUBST(CAMLP4LIB)
...
...
@@ -481,7 +494,7 @@ AC_SUBST(PSVIEWER)
AC_SUBST(PDFVIEWER)
# Finally create the Makefile from Makefile.in
dnl AC_OUTPUT(Makefile)
AC_CONFIG_FILES(Makefile bench/bench)
AC_CONFIG_FILES(Makefile bench/bench
src/util/dynlink_compat.ml
)
AC_OUTPUT
chmod a-w Makefile
chmod a-w bench/bench
...
...
@@ -496,6 +509,7 @@ echo "OCaml version : $OCAMLVERSION"
echo "OCaml library path : $OCAMLLIB"
echo "OcamlGraph lib : $OCAMLGRAPHVER"
echo "Verbose make : $VERBOSEMAKE"
echo "Why plugin enabled : $enable_dynlink"
echo "Abstract interpretation : $enable_apron"
echo "Frama-C plugin : $FRAMAC"
if test "$enable_apron" = "yes" ; then
...
...
src/output/driver.ml
View file @
38810ff7
...
...
@@ -165,16 +165,7 @@ let () =
"Pervasives";"Format";"List";"Sys";"Unix"]
*)
module
Dynlink
=
struct
let
is_native
=
true
open
Dynlink
let
is_native1
=
is_native
let
is_native
=
false
include
Dynlink
let
is_native2
=
is_native
let
is_native_not_defined
=
is_native1
<>
is_native2
end
open
Dynlink_compat
let
load_plugin
dir
(
byte
,
nat
)
=
if
Dynlink
.
is_native_not_defined
then
...
...
src/util/dynlink_compat.ml.in
0 → 100644
View file @
38810ff7
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software 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. *)
(* *)
(**************************************************************************)
# 19 "src/util/dynlink_compat.ml.in"
module Dynlink_ =
struct
let is_native = true (* Dumb value *)
let loadfile_private _ = assert false (* Shouldn't be used *)
end
module Dynlink =
struct
let is_native_not_defined = "@DYNLINK@" = "_Dynlink"
include @DYNLINK@
end
src/util/dynlink_compat.mli
0 → 100644
View file @
38810ff7
module
Dynlink
:
sig
val
is_native_not_defined
:
bool
val
is_native
:
bool
val
loadfile_private
:
string
->
unit
end
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment