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

skip divine tests when divine does not understand compile --help

Browse source 
Fixes #235, reported by Henrich Lauko.

* python/spot/ltsmin.i: Catch CalledProcessError.
* NEWS: Mention the bug.
* THANKS: Add Henrich.
This commit is contained in:
Alexandre Duret-Lutz 2017-02-28 16:05:59 +01:00
parent 6c218e4828
commit 905af90459
3 changed files with 14 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

11
python/spot/ltsmin.i
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2016 Laboratoire de Recherche et Développement de
// Copyright (C) 2016, 2017 Laboratoire de Recherche et Développement de
// l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@ -120,8 +120,13 @@ def require(*tools):
if shutil.which("divine") == None:
print("divine not available", file=sys.stderr)
sys.exit(77)
out = subprocess.check_output(['divine', 'compile', '--help'],
stderr=subprocess.STDOUT)
try:
out = subprocess.check_output(['divine', 'compile', '--help'],
stderr=subprocess.STDOUT)
except (subprocess.CalledProcessError):
print("divine does not understand 'compile --help'",
file=sys.stderr)
sys.exit(77)
if b'LTSmin' not in out:
print("divine available but no support for LTSmin",
file=sys.stderr)