From 3a3913cf5080c844b34803bbe230dfc4c9a89a52 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Tue, 16 Feb 2016 17:22:36 +0100
Subject: [PATCH] otf_product: fix deletion of iter_cache_

Fixes #152, reported by Valentin Iovene.

* spot/twa/twaproduct.cc (~twa_product): Delete iter_cache_.
* tests/python/otfcrash.py: New file.
* tests/Makefile.am: Add it.
* NEWS: Mention the bug.
---
 NEWS                     |  2 ++
 spot/twa/twaproduct.cc   |  4 ++++
 tests/Makefile.am        |  1 +
 tests/python/otfcrash.py | 39 +++++++++++++++++++++++++++++++++++++++
 4 files changed, 46 insertions(+)
 create mode 100644 tests/python/otfcrash.py

diff --git a/NEWS b/NEWS
index dc49dad08..393b37e32 100644
--- a/NEWS
+++ b/NEWS
@@ -132,6 +132,8 @@ New in spot 1.99.7a (not yet released)
   * ltlfilt, autfilt, randltl, and randaut could easily crash when
     compiled statically (i.e., with configure --disable-shared).
   * "1 U (a | Fb)" was not always simplified to "F(a | b)".
+  * destroying the operands of an otf_product() before the product
+    itself could crash.
 
 New in spot 1.99.7 (2016-01-15)
 
diff --git a/spot/twa/twaproduct.cc b/spot/twa/twaproduct.cc
index 94af3c309..b382492e7 100644
--- a/spot/twa/twaproduct.cc
+++ b/spot/twa/twaproduct.cc
@@ -318,6 +318,10 @@ namespace spot
 
   twa_product::~twa_product()
   {
+    // Make sure we delete the iterator cache before erasing the two
+    // automata (by reference counting).
+    delete iter_cache_;
+    iter_cache_ = nullptr;
   }
 
   const state*
diff --git a/tests/Makefile.am b/tests/Makefile.am
index 93bd6a86a..bd0fb25b5 100644
--- a/tests/Makefile.am
+++ b/tests/Makefile.am
@@ -303,6 +303,7 @@ TESTS_python = \
   python/ltsmin.ipynb \
   python/minato.py \
   python/optionmap.py \
+  python/otfcrash.py \
   python/parsetgba.py \
   python/piperead.ipynb \
   python/prodexpt.py \
diff --git a/tests/python/otfcrash.py b/tests/python/otfcrash.py
new file mode 100644
index 000000000..a68e179fd
--- /dev/null
+++ b/tests/python/otfcrash.py
@@ -0,0 +1,39 @@
+import spot
+import spot.ltsmin
+import tempfile
+import shutil
+import sys
+
+# this test requires divine with --ltsmin support
+if shutil.which("divine") == None:
+    sys.exit(77)
+import subprocess
+out = subprocess.check_output(['divine', 'compile',
+                               '--help'], stderr=subprocess.STDOUT)
+if b'LTSmin' not in out:
+    sys.exit(77)
+
+# the test case actually starts here
+with tempfile.NamedTemporaryFile(dir='.', suffix='.dve') as fp:
+    fp.write(b"""int f = 3;
+process R {
+  int p = 1, found = 0;
+  state i, e;
+  init i;
+  trans
+    i -> i {guard p != f; effect p = p + 1;},
+    i -> e {guard p == f; effect found = 1;},
+    e -> e {};
+}
+system async;
+""")
+    fp.flush()
+    m = spot.ltsmin.load(fp.name)
+
+    def modelcheck(formula, model):
+        a = spot.translate(formula)
+        k = m.kripke([ap.ap_name() for ap in a.ap()])
+        p = spot.otf_product(k, a)
+        return p.is_empty()
+
+    assert(modelcheck('X "R.found"', m) == True)