Commit 1b09863b authored by Maximilien Colange's avatar Maximilien Colange

Merge branch 'master' into dynload

parents 36d8b097 f8e9bb82
......@@ -3,5 +3,5 @@ S uppaal_parser
B _build/src/
B _build/uppaal_parser/
PKG batteries udbml xml-light
PKG udbml xml-light
B @UDBML_ROOT@/udbml
......@@ -10,16 +10,20 @@ OCAMLBUILD=ocamlbuild -use-ocamlfind -classic-display -build-dir $(BUILDDIR) @OC
UTAP_INCLUDEDIR=@abs_top_srcdir@/utap/src
UTAP_LIB=@abs_top_srcdir@/utap/src/libutap.a
CXX_FLAGS=-xc++ -std=c++11 -fPIC -O3 -g -DNDEBUG @TIAMO_MACROS@ -I$(UTAP_INCLUDEDIR) -I@abs_top_srcdir@/src
OCAML_CXX_FLAGS=$(foreach i,$(CXX_FLAGS),-ccopt $i)
CXX_FLAGS=-std=c++11 @TIAMO_MACROS@ -I$(UTAP_INCLUDEDIR) -I@abs_top_srcdir@/src
XML_LINK_FLAGS=$(foreach i,$(XML_LIBS),-cclib $i)
all-local:
$(OCAMLBUILD) -cflags "-cc g++ $(OCAML_CXX_FLAGS)" timedAutomatonBuilder.o
$(OCAMLBUILD) -cflags "-g -noassert -I $(INCLUDEDIR)" -lflags "$(INCLUDEDIR)/udbml.cmxa src/timedAutomatonBuilder.o $(UTAP_LIB) $(XML_LINK_FLAGS) -cclib -L$(INCLUDEDIR)" src/main.native
cp `readlink -f $(BUILDDIR)/src/main.native` tiamo
SUFFIXES = .native .ml
all-local: tiamo
tiamo: src/main.native
cp `readlink -f $(BUILDDIR)/$<` tiamo
.ml.native:
CXX_FLAGS="$(CXX_FLAGS)" $(OCAMLBUILD) -cflags "-I $(INCLUDEDIR)" -lflags "$(INCLUDEDIR)/udbml.cmxa $(UTAP_LIB) $(XML_LINK_FLAGS) -cclib -L$(INCLUDEDIR)" $@
clean-local:
ocamlbuild -clean
$(OCAMLBUILD) -clean
rm -f tiamo
......@@ -2,14 +2,14 @@ TiAMo (Timed Automata Model-checker)
M. Colange
O. Sankur
This tools is also based on the DBM library from Uppaal and on the timed automata parser library from Uppaal.
This tool is also based on the DBM library from Uppaal and on the timed automata parser library from Uppaal.
The name of the authors and contributors of these libraries can be found in their respective folders.
Both libraries have been adapted by M. Colange (essentially to drop dependency on Boost, and to work with C++11).
INSTALLATION NOTES
Requires ocaml, batteries, ocamlbuild, camlp4 (you can obtain them through opam)
Requires ocaml, ocamlbuild, camlp4 (you can obtain them through opam).
Requires libxml2 (for the parser).
Requires a C++11-compatible compiler.
Tested (and works fine) with gcc-4.7, gcc-4.8, gcc-4.9 and gcc-5 (5.3.0).
......@@ -17,5 +17,5 @@ Requires a C++11-compatible compiler.
- install udbml (see github.com/osankur/udbml.git)
- install TiAMo
The script 'build.sh' retrieves udbml, compiles and installing it (locally), then compiles
The script 'build.sh' retrieves udbml, compiles and installs it (locally), then compiles
TiAMo. Simply run this script, or modify it if you want a custom installation.
......@@ -40,6 +40,51 @@ AC_SUBST(XML_CONFIG)
AC_SUBST(XML_CFLAGS)
AC_SUBST(XML_LIBS)
OCAMLTAGS=""
dnl Check for debug flags
enableval=no
AC_MSG_CHECKING([whether to compile with debug info])
AC_ARG_ENABLE(debugging,
AS_HELP_STRING([--enable-debugging], [compile with debugging information]))
case "${enableval}" in
yes)
AC_MSG_RESULT(yes)
OPT_FLAGS="$OPT_FLAGS -g"
OCAMLTAGS="$OCAMLTAGS, debug"
;;
no)
AC_MSG_RESULT(no)
OPT_FLAGS="$OPT_FLAGS -O3"
;;
*)
AC_MSG_ERROR([bad value ${enableval} for --enable-debugging, needs yes or no])
;;
esac
enableval=no
AC_MSG_CHECKING([whether to enable checking of run-time assertions])
AC_ARG_ENABLE(assertions,
AS_HELP_STRING([--enable-assertions], [check run-time assertions]))
case "${enableval}" in
yes)
AC_MSG_RESULT(yes)
;;
no)
AC_MSG_RESULT(no)
AC_DEFINE(NDEBUG, 1, [Assertions are disabled when this is defined])
OPT_FLAGS="$OPT_FLAGS -DNDEBUG"
OCAMLTAGS="$OCAMLTAGS, noassert"
;;
*)
AC_MSG_ERROR([bad value ${enableval} --enable-assertions, needs yes or no])
;;
esac
CFLAGS="$OPT_FLAGS"
CPPFLAGS="$OPT_FLAGS"
AC_SUBST(OCAMLTAGS)
AC_SUBST(OCAMLBUILDFLAGS)
AC_CONFIG_SUBDIRS([utap])
......
open Ocamlbuild_plugin (* open the main API module *)
open Command
(* TODO find a cleaner way to retrieve these informations from the environment
* maybe the CXX_FLAGS should be given as arguments to the 'c++' tag,
* thus allowing per-file CXX flags.
*)
let cxx = "g++"
(**
* Default CXX flags:
* -xc++ to be sure to compile .c files as c++
* -fPIC to ensure position-independent code
*)
let cxx_flags =
let env_cxx =
try Some (Sys.getenv "CXX_FLAGS")
with | Not_found -> None
in
match env_cxx with
| None -> ["-xc++"; "-fPIC"]
| Some x -> ["-xc++"; "-fPIC"; x]
(* a helper function *)
(* prefix every c++ flags with -ccopt *)
let ocaml_cxx_flags = fun flags ->
let camlflags = List.flatten (List.map (fun opt -> ["-ccopt"; opt]) flags) in
atomize camlflags
(* TODO add C options when seeing tags:
* noassert -> add '-DNDEBUG'
*
* This kind of tags (debug, noassert, optimization levels...) should be set
* by the configure script through the _tags.in file.
*)
let _ =
dispatch begin function
| After_rules ->
(* TODO declare the internal utap library here *)
(* a custom noassert flag, only for compilation, not preprocessing *)
flag ["compile";"noassert"] (A"-noassert");
(* set proper compilation flags for c++ *)
flag ["c++"] (S[A"-cc"; A cxx; ocaml_cxx_flags cxx_flags]);
flag ["c++";"debug"] (ocaml_cxx_flags ["-g"]);
flag ["c++";"noassert"] (ocaml_cxx_flags ["-DNDEBUG"]);
(* explicit link dependency for C-based object files *)
pdep ["link"] "linkdep" (fun param -> [param])
| _ -> ()
end
<*>: bin_annot
<*.cm{o,x}> or <main.native>: debug, custom
<main.native>: package(dynlink)
<*.c> or <*.cm{o,x}> or <main.native>: custom @OCAMLTAGS@
<main.native>: use_dynlink, linkdep(src/timedAutomatonBuilder.o)
<costs.ml>: pp(camlp4o pa_macro.cmo @TIAMO_MACROS@)
<timedAutomatonBuilder.c>: c++
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment