alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

Fix two spurious segfaults in test cases for the Python interface.

Browse source 
* wrap/python/tests/setxor.py, wrap/python/tests/bddnqueen.py:
Clean all used bdd variables before calling bdd_done(), so that
bdd_delref() is never called after bdd_done().  In NDEBUG builds,
bdd_delref() does not check whether the BuDDy is running or not,
and calling it after bdd_done() will crash.
This commit is contained in:
Alexandre Duret-Lutz 2011-04-09 17:33:42 +02:00
parent 0caf51abd8
commit 9ad062b247
3 changed files with 27 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

10
ChangeLog
View file

@ -1,3 +1,13 @@
2011-04-09 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Fix two spurious segfaults in test cases for the Python interface.
* wrap/python/tests/setxor.py, wrap/python/tests/bddnqueen.py:
Clean all used bdd variables before calling bdd_done(), so that
bdd_delref() is never called after bdd_done(). In NDEBUG builds,
bdd_delref() does not check whether the BuDDy is running or not,
and calling it after bdd_done() will crash.
2011-04-09 Alexandre Duret-Lutz <adl@lrde.epita.fr> 2011-04-09 Alexandre Duret-Lutz <adl@lrde.epita.fr>
* HACKING: Add an example for using callgrind. * HACKING: Add an example for using callgrind.

14
wrap/python/tests/bddnqueen.py
View file

@ -1,7 +1,9 @@
# -*- mode: python; coding: iso-8859-1 -*- # -*- mode: python; coding: utf-8 -*-
# Copyright (C) 2003, 2004, 2010 Laboratoire d'Informatique de Paris 6 (LIP6), # Copyright (C) 2010, 2011 Laboratoire de Recherche et Développement
# département Systèmes Répartis Coopératifs (SRC), Université Pierre # de l'EPITA.
# et Marie Curie. # Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6
# (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
# Pierre et Marie Curie.
# #
# This file is part of Spot, a model checking library. # This file is part of Spot, a model checking library.
# #
@ -97,4 +99,8 @@ solution = bdd_satone(queen)
bdd_printset(solution) bdd_printset(solution)
print print
# Cleanup all BDD variables before calling bdd_done(), otherwise
# bdd_delref will be called after bdd_done() and this is unsafe in
# optimized builds.
X = e = queen = solution = 0
bdd_done() bdd_done()

9
wrap/python/tests/setxor.py
View file

@ -1,5 +1,6 @@
# -*- mode: python; coding: iso-8859-1 -*- # -*- mode: python; coding: utf-8 -*-
# Copyright (C) 2010 Laboratoire de Recherche et Développement de l'EPITA. # Copyright (C) 2010, 2011 Laboratoire de Recherche et Développement
# de l'EPITA.
# #
# This file is part of Spot, a model checking library. # This file is part of Spot, a model checking library.
# #
@ -43,4 +44,8 @@ e = V[0] & V[1] & -V[2] & -V[3] & V[4]
assert(e == bdd_setxor(a,d)) assert(e == bdd_setxor(a,d))
assert(e == bdd_setxor(d,a)) assert(e == bdd_setxor(d,a))
# Cleanup all BDD variables before calling bdd_done(), otherwise
# bdd_delref will be called after bdd_done() and this is unsafe in
# optimized builds.
V = a = b = c = d = e = 0;
bdd_done() bdd_done()