Commit f5dce597 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

switch to C++14 compilation

* configure.ac: Compile in C++14 by default and rename
--enable-c++14 as c++17.
* doc/org/compile.org, doc/org/concepts.org, doc/org/index.org,
doc/org/install.org, doc/org/tut.org, doc/org/upgrade2.org, HACKING,
NEWS, README: Adjust all mentions of C++11.
* spot/twaalgos/stats.hh: Use std::make_unique.
parent 7f427827
...@@ -28,7 +28,7 @@ since the generated files they produce are distributed.) ...@@ -28,7 +28,7 @@ since the generated files they produce are distributed.)
GNU Bison >= 3.0 GNU Bison >= 3.0
GNU Emacs (preferably >= 24 but it may work with older versions) GNU Emacs (preferably >= 24 but it may work with older versions)
Groff (a.k.a. GNU troff) >= 1.20 Groff (a.k.a. GNU troff) >= 1.20
SWIG >= 3.0 (for its better C++11 support) SWIG >= 3.0 (for its better C++11/C++14 support)
Doxygen >= 1.4.0 Doxygen >= 1.4.0
Perl, with its Gettext module (it might be called something like Perl, with its Gettext module (it might be called something like
liblocale-gettext-perl or p5-locale-gettext in your distribution) liblocale-gettext-perl or p5-locale-gettext in your distribution)
...@@ -300,16 +300,14 @@ forget guards, and we do not forget to rename them when a file is ...@@ -300,16 +300,14 @@ forget guards, and we do not forget to rename them when a file is
copied into another one. copied into another one.
C++11 C++14
----- -----
Spot uses some C++11 features, and therefore requires a C++11 Spot uses some C++14 features, and therefore requires a C++14
compiler. The code relies on features that are not available in compiler. g++ 5.x or clang++ 3.4 should be enough.
version of g++ older than 4.8, so this is our minimum requirement
for now. Avoid features that require 4.9.
Reasonably recent versions of clang should work as well. Our We currently avoid C++17 features until C++17 compiler are widely
build farm has clang++ 3.5. available.
Encoding Encoding
-------- --------
......
New in spot 2.3.5.dev (not yet released) New in spot 2.3.5.dev (not yet released)
Build:
- Spot is now built in C++14 mode, so you need at least GCC 5 or
clang 3.4. The current version of all major linux distributions
ship with at least GCC 6, which defaults to C++14, so this should
not be a problem. In *this* release of Spot, most of the header
files are still C++11 compatible, so you should be able to include
Spot in a C++11 project in case you do not yet want to upgrade.
There is also an --enable-c++17 option to configure in case you
want to force a build of Spot in C++17 mode.
Tools: Tools:
- genaut is a new binary that produces families of automata defined - genaut is a new binary that produces families of automata defined
......
...@@ -2,7 +2,7 @@ Overview ...@@ -2,7 +2,7 @@ Overview
======== ========
Spot is a model-checking toolkit comprising: Spot is a model-checking toolkit comprising:
- a C++11 library with data-structures and algorithms for working - a C++14 library with data-structures and algorithms for working
with linear-time temporal logical formulas and ω-automata with with linear-time temporal logical formulas and ω-automata with
any acceptance condition. any acceptance condition.
- a set of command-line tools for easy access to those algorithms, - a set of command-line tools for easy access to those algorithms,
...@@ -73,8 +73,8 @@ Installation ...@@ -73,8 +73,8 @@ Installation
Requirements Requirements
------------ ------------
Spot requires a C++11-compliant compiler. Spot requires a C++14-compliant compiler. G++ 5.x or later, as well
G++ 4.8 or later, as well as Clang++ 3.5 or later should work. as Clang++ 3.5 or later should work.
Spot expects a complete installation of Python (version 3.3 or later). Spot expects a complete installation of Python (version 3.3 or later).
Especially, Python's headers files should be installed. If you don't Especially, Python's headers files should be installed. If you don't
...@@ -141,6 +141,10 @@ flags specific to Spot: ...@@ -141,6 +141,10 @@ flags specific to Spot:
client code should be compiled with -D_GLIBCXX_DEBUG as well. This client code should be compiled with -D_GLIBCXX_DEBUG as well. This
options should normally only be useful to run Spot's test-suite. options should normally only be useful to run Spot's test-suite.
--enable-c++17
Build everything in C++17 mode. We use that in our build farm to
ensure that Spot can be used in C++17 projects as well.
Here are the meaning of the fine-tuning options, in case Here are the meaning of the fine-tuning options, in case
--enable/disable-devel is not enough. --enable/disable-devel is not enough.
......
...@@ -47,18 +47,14 @@ adl_CHECK_BISON ...@@ -47,18 +47,14 @@ adl_CHECK_BISON
# Decrease verbosity when passing argument V=0 # Decrease verbosity when passing argument V=0
AM_SILENT_RULES([no]) AM_SILENT_RULES([no])
# Option to activate C/C++14 # Option to activate C++17
AC_ARG_ENABLE([c++14], AC_ARG_ENABLE([c++17],
[AC_HELP_STRING([--enable-c++14], [AC_HELP_STRING([--enable-c++17],
[Use C++14.])], [Compile in C++17 mode.])],
[enable_14=yes], [enable_14=no]) [enable_17=yes], [enable_17=no])
# Activate at C11 for gnulib tests # Activate C11 for gnulib tests
if test x"${enable_14}" = xyes; then AX_CHECK_COMPILE_FLAG([-std=c11], [CFLAGS="$CFLAGS -std=c11"])
AX_CHECK_COMPILE_FLAG([-std=c14], [CFLAGS="$CFLAGS -std=c14"])
else
AX_CHECK_COMPILE_FLAG([-std=c11], [CFLAGS="$CFLAGS -std=c11"])
fi
gl_INIT gl_INIT
...@@ -73,46 +69,11 @@ AX_CHECK_COMPILE_FLAG([-Werror -fvisibility=hidden], ...@@ -73,46 +69,11 @@ AX_CHECK_COMPILE_FLAG([-Werror -fvisibility=hidden],
[CXXFLAGS="$CXXFLAGS -fvisibility-inlines-hidden"])]) [CXXFLAGS="$CXXFLAGS -fvisibility-inlines-hidden"])])
CXXFLAGS="$CXXFLAGS -DSPOT_BUILD" CXXFLAGS="$CXXFLAGS -DSPOT_BUILD"
# Turn on C++11 support
m4_define([_AX_CXX_COMPILE_STDCXX_11_testbody],
[AC_LANG_SOURCE([#include <memory>
#include <string>
#include <chrono> // fails with some installation of clang
#include <map>
template <typename T>
struct check
{
static_assert(sizeof(int) <= sizeof(T), "not big enough");
};
typedef check<check<bool>> right_angle_brackets;
auto f = std::make_shared<std::string>("shared_ptr");
int a;
decltype(a) b;
typedef check<int> check_type;
check_type c;
check_type&& cr = static_cast<check_type&&>(c);
auto d = a;
void test_emplace()
{
std::map<int, int> m;
m.emplace(1, 2); // fails with g++ 4.6
}
])])
# Turn on C++14 support # Turn on C++14 support
# This is currently a copy of the above code for C++11, feel free to add
# further tests here when necessary.
m4_define([_AX_CXX_COMPILE_STDCXX_14_testbody], m4_define([_AX_CXX_COMPILE_STDCXX_14_testbody],
[AC_LANG_SOURCE([#include <memory> [AC_LANG_SOURCE([#include <memory>
#include <string> #include <string>
#include <chrono> // fails with some installation of clang #include <chrono> // used to fail in C++11 with some installation of clang
#include <map> #include <map>
template <typename T> template <typename T>
...@@ -123,7 +84,7 @@ m4_define([_AX_CXX_COMPILE_STDCXX_14_testbody], ...@@ -123,7 +84,7 @@ m4_define([_AX_CXX_COMPILE_STDCXX_14_testbody],
typedef check<check<bool>> right_angle_brackets; typedef check<check<bool>> right_angle_brackets;
auto f = std::make_shared<std::string>("shared_ptr"); auto f = std::make_unique<std::string>("uniq_ptr");
int a; int a;
decltype(a) b; decltype(a) b;
...@@ -133,33 +94,27 @@ m4_define([_AX_CXX_COMPILE_STDCXX_14_testbody], ...@@ -133,33 +94,27 @@ m4_define([_AX_CXX_COMPILE_STDCXX_14_testbody],
check_type&& cr = static_cast<check_type&&>(c); check_type&& cr = static_cast<check_type&&>(c);
auto d = a; auto d = a;
void test_emplace()
{
std::map<int, int> m;
m.emplace(1, 2); // fails with g++ 4.6
}
])]) ])])
if test x"${enable_14}" = xyes; then if test x"${enable_17}" = xyes; then
for f in -std=c++14 '-std=c++14 -stdlib=libc++' -std=c++1y for f in -std=c++17 '-std=c++17 -stdlib=libc++' -std=c++1z
do do
AX_CHECK_COMPILE_FLAG([$f], [CXXFLAGS="$CXXFLAGS $f" stdpass=true], [], [], AX_CHECK_COMPILE_FLAG([$f], [CXXFLAGS="$CXXFLAGS $f" stdpass=true], [], [],
[_AX_CXX_COMPILE_STDCXX_14_testbody]) [_AX_CXX_COMPILE_STDCXX_14_testbody])
${stdpass-false} && break ${stdpass-false} && break
done done
if ! "${stdpass-false}"; then if ! "${stdpass-false}"; then
AC_ERROR([unable to turn on C++14 mode with this compiler]) AC_ERROR([unable to turn on C++17 mode with this compiler])
fi fi
else else
for f in -std=c++11 '-std=c++11 -stdlib=libc++' -std=c++0x for f in -std=c++14 '-std=c++14 -stdlib=libc++' -std=c++1y
do do
AX_CHECK_COMPILE_FLAG([$f], [CXXFLAGS="$CXXFLAGS $f" stdpass=true], [], [], AX_CHECK_COMPILE_FLAG([$f], [CXXFLAGS="$CXXFLAGS $f" stdpass=true], [], [],
[_AX_CXX_COMPILE_STDCXX_11_testbody]) [_AX_CXX_COMPILE_STDCXX_14_testbody])
${stdpass-false} && break ${stdpass-false} && break
done done
if ! "${stdpass-false}"; then if ! "${stdpass-false}"; then
AC_ERROR([unable to turn on C++11 mode with this compiler]) AC_ERROR([unable to turn on C++14 mode with this compiler])
fi fi
fi fi
......
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
#+TITLE: Compiling against Spot #+TITLE: Compiling against Spot
#+DESCRIPTION: How to compile C++11 programs using Spot #+DESCRIPTION: How to compile C++14 programs using Spot
#+SETUPFILE: setup.org #+SETUPFILE: setup.org
#+HTML_LINK_UP: tut.html #+HTML_LINK_UP: tut.html
...@@ -39,10 +39,10 @@ obvisously. On this page, we are going to assume that you use =g++= ...@@ -39,10 +39,10 @@ obvisously. On this page, we are going to assume that you use =g++=
same user interface. To successfully build the =hello= program, we same user interface. To successfully build the =hello= program, we
might need to tell the compiler several things: might need to tell the compiler several things:
1. The language that we use is C++11 (or C++14). This usually 1. The language that we use is C++14 (or optionally C++17). This
requires passing an option like =-std=c++11=. Note that with usually requires passing an option like =-std=c++14=. Note that
version 6 of =g++= the default is now to compile C++14, so this with version 6 of =g++= the default is now to compile C++14, so
option is not necessary. this option is not necessary.
2. The C++ preprocessor should be able to find =spot/misc/version.hh=. 2. The C++ preprocessor should be able to find =spot/misc/version.hh=.
This might require appending another directory to the include This might require appending another directory to the include
search path with =-I location=. search path with =-I location=.
...@@ -78,7 +78,7 @@ be able to find everything by default, and you should be able to ...@@ -78,7 +78,7 @@ be able to find everything by default, and you should be able to
compile =hello.cc= and then execute =hello= with compile =hello.cc= and then execute =hello= with
#+BEGIN_SRC sh #+BEGIN_SRC sh
g++ -std=c++11 hello.cc -lspot -o hello g++ -std=c++14 hello.cc -lspot -o hello
./hello ./hello
#+END_SRC #+END_SRC
...@@ -101,11 +101,11 @@ This means that all spot headers have been installed in ...@@ -101,11 +101,11 @@ This means that all spot headers have been installed in
Usually, these directories are searched by default, so Usually, these directories are searched by default, so
#+BEGIN_SRC sh #+BEGIN_SRC sh
g++ -std=c++11 hello.cc -lspot -o hello g++ -std=c++14 hello.cc -lspot -o hello
#+END_SRC #+END_SRC
should still work. But if that is not the case, add should still work. But if that is not the case, add
#+BEGIN_SRC sh #+BEGIN_SRC sh
g++ -std=c++11 -I/usr/local/include hello.cc -L/usr/local/lib -lspot -o hello g++ -std=c++14 -I/usr/local/include hello.cc -L/usr/local/lib -lspot -o hello
#+END_SRC #+END_SRC
If running =./hello= fails with a message about not finding =libspot.so=, If running =./hello= fails with a message about not finding =libspot.so=,
...@@ -131,7 +131,7 @@ libraries in =$HOME/usr/lib=. ...@@ -131,7 +131,7 @@ libraries in =$HOME/usr/lib=.
You would compile =hello.cc= with You would compile =hello.cc= with
#+BEGIN_SRC sh #+BEGIN_SRC sh
g++ -std=c++11 -I$HOME/usr/include hello.cc -L$HOME/usr/lib -lspot -o hello g++ -std=c++14 -I$HOME/usr/include hello.cc -L$HOME/usr/lib -lspot -o hello
#+END_SRC #+END_SRC
and execute with and execute with
#+BEGIN_SRC sh #+BEGIN_SRC sh
...@@ -184,7 +184,7 @@ There are at least two traps with this scenario: ...@@ -184,7 +184,7 @@ There are at least two traps with this scenario:
So compiling against a non-installed Spot would look like this: So compiling against a non-installed Spot would look like this:
#+BEGIN_SRC sh #+BEGIN_SRC sh
/dir/spot-X.Y/libtool link g++ -std=c++11 -I/dir/spot-X.Y -I/dir/spot-X.Y/buddy/src hello.cc /dir/spot-X.Y/spot/libspot.la -o hello /dir/spot-X.Y/libtool link g++ -std=c++14 -I/dir/spot-X.Y -I/dir/spot-X.Y/buddy/src hello.cc /dir/spot-X.Y/spot/libspot.la -o hello
#+END_SRC #+END_SRC
Using =libtool link g++= instead of =g++= will cause =libtool= to Using =libtool link g++= instead of =g++= will cause =libtool= to
......
...@@ -1022,7 +1022,7 @@ components that are distributed and installed by Spot. ...@@ -1022,7 +1022,7 @@ components that are distributed and installed by Spot.
- =libbddx= is a customized version of [[https://sourceforge.net/projects/buddy/][the BuDDy library]], for - =libbddx= is a customized version of [[https://sourceforge.net/projects/buddy/][the BuDDy library]], for
manipulating [[#bdd][BDDs]]. manipulating [[#bdd][BDDs]].
- =libspot= is the main library, containing a C++11 implementation of all the - =libspot= is the main library, containing a C++14 implementation of all the
data structures and algorithms. This depends on =libddx=. data structures and algorithms. This depends on =libddx=.
- =libspotgen= is an auxiliary library that contains functions to - =libspotgen= is an auxiliary library that contains functions to
generate families of automata, useful for benchmarking and testing generate families of automata, useful for benchmarking and testing
...@@ -1034,7 +1034,7 @@ components that are distributed and installed by Spot. ...@@ -1034,7 +1034,7 @@ components that are distributed and installed by Spot.
SpinS or a patched version of DiVinE, but you have to install SpinS or a patched version of DiVinE, but you have to install
those third-party tools first. See [[https://gitlab.lrde.epita.fr/spot/spot/blob/next/tests/ltsmin/README][=tests/ltsmin/README=]] those third-party tools first. See [[https://gitlab.lrde.epita.fr/spot/spot/blob/next/tests/ltsmin/README][=tests/ltsmin/README=]]
for details. for details.
- In addition to the C++11 API, we also provide Python bindings for - In addition to the C++14 API, we also provide Python bindings for
=libspotgen=, =libspotltsmin=, =libbddx=, and most of =libspot=. =libspotgen=, =libspotltsmin=, =libbddx=, and most of =libspot=.
These are available by importing =spot.gen=, =spot.ltsmin=, =bdd=, These are available by importing =spot.gen=, =spot.ltsmin=, =bdd=,
and =spot=. Those Python bindings also includes some additional and =spot=. Those Python bindings also includes some additional
......
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
#+TITLE: Spot: a platform for LTL and ω-automata manipulation #+TITLE: Spot: a platform for LTL and ω-automata manipulation
#+DESCRIPTION: Spot is a library and tool suite for LTL and ω-automata #+DESCRIPTION: Spot is a library and tool suite for LTL and ω-automata
#+KEYWORDS: Spot,C++11,library,platform,framework,tool-suite,LTL,PSL,omega-automata #+KEYWORDS: Spot,C++14,library,platform,framework,tool-suite,LTL,PSL,omega-automata
#+SETUPFILE: setup.org #+SETUPFILE: setup.org
#+HTML_HEAD_EXTRA: <style>#org-div-home-and-up { display: none; }</style> #+HTML_HEAD_EXTRA: <style>#org-div-home-and-up { display: none; }</style>
Spot is a C++11 library for LTL, ω-automata manipulation and model Spot is a C++14 library for LTL, ω-automata manipulation and model
checking. It has the following notable features: checking. It has the following notable features:
- Support for [[file:concepts.org::#ltl][LTL]] (several syntaxes supported) and - Support for [[file:concepts.org::#ltl][LTL]] (several syntaxes supported) and
......
...@@ -16,7 +16,7 @@ successful development build]]. ...@@ -16,7 +16,7 @@ successful development build]].
** Requirements ** Requirements
Spot requires a C++11-compliant compiler. =g++= 4.8 or later, as well Spot requires a C++14-compliant compiler. =g++= 5.0 or later, as well
as =clang++= 3.5 or later should work. as =clang++= 3.5 or later should work.
Spot expects a complete installation of Python (version 3.3 or later). Spot expects a complete installation of Python (version 3.3 or later).
...@@ -75,7 +75,7 @@ apt-get install spot libspot-dev spot-doc python3-spot # Or a subset of those ...@@ -75,7 +75,7 @@ apt-get install spot libspot-dev spot-doc python3-spot # Or a subset of those
#+END_SRC #+END_SRC
The package =spot= contains the [[file:tools.org][command-line tools]]. =libspot-dev= The package =spot= contains the [[file:tools.org][command-line tools]]. =libspot-dev=
contains the header files if you plan to use Spot in a C++11 contains the header files if you plan to use Spot in a C++14
program. =spot-doc= contains some html (including these pages) and pdf program. =spot-doc= contains some html (including these pages) and pdf
documentation. Finally =python3-spot= contains some Python bindings documentation. Finally =python3-spot= contains some Python bindings
(this package also installs some ipython notebooks that you can use as (this package also installs some ipython notebooks that you can use as
......
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
#+TITLE: Code Examples #+TITLE: Code Examples
#+DESCRIPTION: Directory of code examples for using Spot in C++11, Python, and shell. #+DESCRIPTION: Directory of code examples for using Spot in C++14, Python, and shell.
#+SETUPFILE: setup.org #+SETUPFILE: setup.org
#+HTML_LINK_UP: index.html #+HTML_LINK_UP: index.html
......
...@@ -20,7 +20,7 @@ experience of updating a couple of projects that are using Spot. ...@@ -20,7 +20,7 @@ experience of updating a couple of projects that are using Spot.
Spot 1.2.6 and Spot 2.0, just to get an idea of what will need to be Spot 1.2.6 and Spot 2.0, just to get an idea of what will need to be
updated. updated.
1. [[#cpp11][Spot now compiles using the C++11 standard]]. Compliant compiler 1. [[#cpp14][Spot now compiles using the C++14 standard]]. Compliant compiler
are sufficiently widespread now that this should not be an issue. are sufficiently widespread now that this should not be an issue.
2. The layout of the source-tree and the layout of the installed 2. The layout of the source-tree and the layout of the installed
...@@ -83,23 +83,22 @@ experience of updating a couple of projects that are using Spot. ...@@ -83,23 +83,22 @@ experience of updating a couple of projects that are using Spot.
numbered. Many algorithms have been rewritten on top of this numbered. Many algorithms have been rewritten on top of this
=twa_graph= class, and this simplified them a lot. =twa_graph= class, and this simplified them a lot.
* Upgrading to C++11 * Upgrading to C++14
:PROPERTIES: :PROPERTIES:
:CUSTOM_ID: cpp11 :CUSTOM_ID: cpp11
:END: :END:
Because Spot now relies on C++11 features, programs that use Spot Because Spot now relies on C++14 features, programs that use Spot
should at least be compiled using this version (or a later one) of should at least be compiled using this version (or a later one) of
the language. the language.
Before the =g++= 6.0, the default C++ standard used was C++98, and Before the =g++= 6.0, the default C++ standard used was C++98, and
enabling C++11 is usually done by passing the option =-std=c++11=. enabling C++14 is usually done by passing the option =-std=c++14=.
In =g++= 6.0 the default C++ standard used is C++14, so passing In =g++= 6.0 the default C++ standard used is C++14, so passing
=-std=c++11= is only necessary in projects that are incompatible =-std=c++14= is not necessary.
with C++14.
Upgrading from C++98 or C++03 to C++11 should be relatively smooth Upgrading from C++98, C++03 or C++11 to C++14 should be relatively
as the language is /mostly/ backward compatible. smooth as the language is /mostly/ backward compatible.
* Upgrading =#include= directives * Upgrading =#include= directives
:PROPERTIES: :PROPERTIES:
...@@ -600,7 +599,6 @@ for (auto i: aut->succ(s)) ...@@ -600,7 +599,6 @@ for (auto i: aut->succ(s))
automatically unregistered when the automaton is destroyed. automatically unregistered when the automaton is destroyed.
* Various renamings * Various renamings
:PROPERTIES: :PROPERTIES:
......
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2008, 2011, 2012, 2013, 2014, 2015, 2016 Laboratoire de // Copyright (C) 2008, 2011-2017 Laboratoire de Recherche et
// Recherche et Développement de l'Epita (LRDE). // Développement de l'Epita (LRDE).
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre // département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie. // et Marie Curie.
...@@ -77,7 +77,7 @@ namespace spot ...@@ -77,7 +77,7 @@ namespace spot
public: public:
void automaton(const const_twa_graph_ptr& aut) void automaton(const const_twa_graph_ptr& aut)
{ {
val_ = std::unique_ptr<scc_info>(new scc_info(aut)); val_ = std::make_unique<scc_info>(aut);
} }
void reset() void reset()
......
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