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

bitvect: fix block_count() on 0-sized bit-vectors

Browse source 
The bug was introduced by 522373984c.

* src/misc/bitvect.hh (block_count): Here.
* src/tgbatest/dstar.test: Add a test case.
This commit is contained in:
Alexandre Duret-Lutz 2014-01-23 23:09:28 +01:00
parent 91789b9b12
commit 4f31a9bbed
2 changed files with 32 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/misc/bitvect.hh
View file

@ -131,7 +131,7 @@ namespace spot
size_t used_blocks() const size_t used_blocks() const
{ {
const size_t bpb = 8 * sizeof(block_t); const size_t bpb = 8 * sizeof(block_t);
return (size_ - 1) / bpb + 1; return (size_ + bpb - 1) / bpb;
} }
/// Append one bit. /// Append one bit.

32
src/tgbatest/dstar.test
View file

@ -1,6 +1,6 @@
#!/bin/sh #!/bin/sh
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
# Copyright (C) 2013 Laboratoire de Recherche et # Copyright (C) 2013, 2014 Laboratoire de Recherche et
# Développement de l'Epita (LRDE). # Développement de l'Epita (LRDE).
# #
# This file is part of Spot, a model checking library. # This file is part of Spot, a model checking library.
@ -237,3 +237,33 @@ EOF
diff expected stdout diff expected stdout
test "`../../bin/dstar2tgba -D dra.dstar --stats '%s %t %p %d'`" = "3 12 1 1" 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