diff --git a/NEWS b/NEWS
index 077ec6313..6d145160d 100644
--- a/NEWS
+++ b/NEWS
@@ -1,18 +1,4 @@
-New in spot 2.7.1.dev (not yet released)
-
- Documentation:
-
- - A new page shows how to create explicit Kripke structures in C++
- and Python. See https://spot.lrde.epita.fr/tut52.html
- - Another new page shows how to deal with LTLf formulas (i.e., LTL
- with finite semantics) and how to translate those.
- See https://spot.lrde.epita.fr/tut12.html
-
- Python:
-
- - Improved support for explicit Kripke structure. It is now
- possible to iterate over a kripke_graph object in a way similar to
- twa_graph.
+New in spot 2.7.2.dev (not yet released)
Library:
@@ -29,6 +15,27 @@ New in spot 2.7.1.dev (not yet released)
'ltldo ltl2dstar -f 'GFa -> GFb' | autfilt --small' produces 1
state instead of 4.)
+New in spot 2.7.2 (2019-03-17)
+
+ Python:
+
+ - Improved support for explicit Kripke structures. It is now
+ possible to iterate over a kripke_graph object in a way similar to
+ twa_graph.
+
+ Documentation:
+
+ - A new page shows how to create explicit Kripke structures in C++
+ and Python. See https://spot.lrde.epita.fr/tut52.html
+ - Another new page shows how to deal with LTLf formulas (i.e., LTL
+ with finite semantics) and how to translate those.
+ See https://spot.lrde.epita.fr/tut12.html
+
+ Build:
+
+ - Work around a spurious null dereference warning when compiling
+ with --coverage and g++ 8.3.0-3 from Debian unstable.
+
New in spot 2.7.1 (2019-02-14)
Build
diff --git a/configure.ac b/configure.ac
index ca222c678..0c87413bf 100644
--- a/configure.ac
+++ b/configure.ac
@@ -21,7 +21,7 @@
# along with this program. If not, see .
AC_PREREQ([2.61])
-AC_INIT([spot], [2.7.1.dev], [spot@lrde.epita.fr])
+AC_INIT([spot], [2.7.2.dev], [spot@lrde.epita.fr])
AC_CONFIG_AUX_DIR([tools])
AC_CONFIG_MACRO_DIR([m4])
AM_INIT_AUTOMAKE([1.11 gnu tar-ustar color-tests parallel-tests])
diff --git a/doc/org/setup.org b/doc/org/setup.org
index d03324286..d6ba75962 100644
--- a/doc/org/setup.org
+++ b/doc/org/setup.org
@@ -1,11 +1,11 @@
#+OPTIONS: H:2 num:nil toc:t html-postamble:nil
#+EMAIL: spot@lrde.epita.fr
#+HTML_LINK_HOME: index.html
-#+MACRO: SPOTVERSION 2.7.1
-#+MACRO: LASTRELEASE 2.7.1
-#+MACRO: LASTTARBALL [[http://www.lrde.epita.fr/dload/spot/spot-2.7.1.tar.gz][=spot-2.7.1.tar.gz=]]
-#+MACRO: LASTNEWS [[https://gitlab.lrde.epita.fr/spot/spot/blob/spot-2-7-1/NEWS][summary of the changes]]
-#+MACRO: LASTDATE 2019-02-14
+#+MACRO: SPOTVERSION 2.7.2
+#+MACRO: LASTRELEASE 2.7.2
+#+MACRO: LASTTARBALL [[http://www.lrde.epita.fr/dload/spot/spot-2.7.2.tar.gz][=spot-2.7.2.tar.gz=]]
+#+MACRO: LASTNEWS [[https://gitlab.lrde.epita.fr/spot/spot/blob/spot-2-7-2/NEWS][summary of the changes]]
+#+MACRO: LASTDATE 2019-03-17
#+ATTR_HTML: :id spotlogo
[[file:spot2.svg]]
diff --git a/doc/org/tut.org b/doc/org/tut.org
index 60b8f0344..d15063356 100644
--- a/doc/org/tut.org
+++ b/doc/org/tut.org
@@ -13,7 +13,7 @@ If you have difficulties compiling the C++ examples, check out [[file:compile.or
instructions]].
Reading the [[file:concepts.org][concepts page]] might help if you are not familiar with some
-of the objects manipulated here.
+of the objects or concepts used here.
* Examples with Shell, Python, and C++
@@ -25,7 +25,7 @@ three interfaces supported by Spot: shell commands, Python, or C++.
- [[file:tut04.org][Testing the equivalence of two LTL formulas]]
- [[file:tut10.org][Translating an LTL formula into a never claim]]
- [[file:tut11.org][Translating an LTL formula into a monitor]]
-- [[file:tut12.org][Working with LTL formula with finite semantics]]
+- [[file:tut12.org][Working with LTL formulas with finite semantics]]
- [[file:tut20.org][Converting a never claim into HOA]]
- [[file:tut30.org][Converting Rabin (or Other) to Büchi, and simplifying it]]
- [[file:tut31.org][Removing alternation]]
diff --git a/doc/org/tut12.org b/doc/org/tut12.org
index 10641558b..741053597 100644
--- a/doc/org/tut12.org
+++ b/doc/org/tut12.org
@@ -1,5 +1,5 @@
# -*- coding: utf-8 -*-
-#+TITLE: Working with LTL formula with finite semantics
+#+TITLE: Working with LTL formulas with finite semantics
#+DESCRIPTION: Code example for using Spot to translate LTLf formulas
#+INCLUDE: setup.org
#+HTML_LINK_UP: tut.html
diff --git a/spot/twaalgos/ltl2taa.cc b/spot/twaalgos/ltl2taa.cc
index 49c3880ee..6430f43cb 100644
--- a/spot/twaalgos/ltl2taa.cc
+++ b/spot/twaalgos/ltl2taa.cc
@@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
-// Copyright (C) 2009-2010, 2012-2016, 2018 Laboratoire de Recherche
-// et Développement de l'Epita (LRDE).
+// Copyright (C) 2009-2010, 2012-2016, 2018-2019 Laboratoire de
+// Recherche et Développement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
@@ -20,6 +20,7 @@
#include "config.h"
#include
#include
+#include
#include
#include
#include
@@ -340,6 +341,10 @@ namespace spot
for (unsigned i = 0; i < vs.size(); ++i)
pos[i] = vs[i].succ_.size();
+ // g++ (Debian 8.3.0-3) 8.3.0 in --coverage mode,
+ // reports a "potential null pointer dereference" on the next
+ // line without this assert...
+ assert(pos.size() > 0);
while (pos[0] != 0)
{
std::vector u; // Union