From 161bb0675fef81c908e2beb409edecf30ebb3f6e Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 2 Nov 2017 10:31:52 +0100 Subject: [PATCH] test the SPOT_BDD_TRACE envvar * tests/core/bdd.test: New file. * tests/Makefile.am: Add it. --- tests/Makefile.am | 1 + tests/core/bdd.test | 29 +++++++++++++++++++++++++++++ 2 files changed, 30 insertions(+) create mode 100755 tests/core/bdd.test diff --git a/tests/Makefile.am b/tests/Makefile.am index 7763accfa..afa1a3d6a 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -196,6 +196,7 @@ TESTS_kripke = \ core/kripke.test TESTS_misc = \ + core/bdd.test \ core/bitvect.test \ core/intvcomp.test \ core/minusx.test \ diff --git a/tests/core/bdd.test b/tests/core/bdd.test new file mode 100755 index 000000000..82c1bd912 --- /dev/null +++ b/tests/core/bdd.test @@ -0,0 +1,29 @@ +#!/bin/sh +# -*- coding: utf-8 -*- +# Copyright (C) 2017 Laboratoire de Recherche et Développement de +# l'Epita (LRDE). +# +# This file is part of Spot, a model checking library. +# +# Spot is free software; you can redistribute it and/or modify it +# under the terms of the GNU General Public License as published by +# the Free Software Foundation; either version 3 of the License, or +# (at your option) any later version. +# +# Spot is distributed in the hope that it will be useful, but WITHOUT +# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +# License for more details. +# +# You should have received a copy of the GNU General Public License +# along with this program. If not, see . + +. ./defs +set -e + +# Make sure that setting the SPOT_BDD_TRACE envvar actually does +# something. +SPOT_BDD_TRACE=1 ltl2tgba a >out 2>err +grep spot: out && exit 1 +grep 'spot: BDD package initialized' err +grep 'spot: BDD stats:' err -- GitLab