From 4f31a9bbed78cd3f019352202ddea4b2559436ca Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Thu, 23 Jan 2014 23:09:28 +0100
Subject: [PATCH] bitvect: fix block_count() on 0-sized bit-vectors

The bug was introduced by 522373984cd5100890b8fb641861fd1139b9e028.

* src/misc/bitvect.hh (block_count): Here.
* src/tgbatest/dstar.test: Add a test case.
---
 src/misc/bitvect.hh     |  2 +-
 src/tgbatest/dstar.test | 32 +++++++++++++++++++++++++++++++-
 2 files changed, 32 insertions(+), 2 deletions(-)

diff --git a/src/misc/bitvect.hh b/src/misc/bitvect.hh
index 474e96854..b641326d9 100644
--- a/src/misc/bitvect.hh
+++ b/src/misc/bitvect.hh
@@ -131,7 +131,7 @@ namespace spot
     size_t used_blocks() const
     {
       const size_t bpb = 8 * sizeof(block_t);
-      return (size_ - 1) / bpb + 1;
+      return (size_ + bpb - 1) / bpb;
     }
 
     /// Append one bit.
diff --git a/src/tgbatest/dstar.test b/src/tgbatest/dstar.test
index 826837ce0..499252d01 100755
--- a/src/tgbatest/dstar.test
+++ b/src/tgbatest/dstar.test
@@ -1,6 +1,6 @@
 #!/bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2013 Laboratoire de Recherche et
+# Copyright (C) 2013, 2014 Laboratoire de Recherche et
 # Développement de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -237,3 +237,33 @@ EOF
 diff expected stdout
 
 test "`../../bin/dstar2tgba -D dra.dstar --stats '%s %t %p %d'`" = "3 12 1 1"
+
+# This has caused a crash at some point when dealing with 0-sized
+# bitsets to represent acceptance sets.
+cat >aut.dsa <<EOF
+DSA v2 explicit
+Comment: "Streett{Safra[NBA=1]}"
+States: 1
+Acceptance-Pairs: 0
+Start: 0
+AP: 0
+---
+State: 0
+Acc-Sig:
+0
+EOF
+run 0 ../ltl2tgba -XDD aut.dsa | tee stdout
+
+cat >expected<<EOF
+digraph G {
+  0 [label="", style=invis, height=0]
+  0 -> 1
+  1 [label="0"]
+  1 -> 1 [label="1\n"]
+  1 -> 2 [label="1\n"]
+  2 [label="1"]
+  2 -> 2 [label="1\n"]
+}
+EOF
+
+diff expected stdout