From e97ea5fa746e3fcee78249a47951777f1e40cb91 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 14 Aug 2016 18:18:20 +0200 Subject: [PATCH] bin: diagnose more write errors * tests/core/full.test: New file. * tests/Makefile.am: Add it. * bin/autfilt.cc, bin/common_aoutput.cc, bin/common_aoutput.hh, bin/common_file.cc, bin/common_file.hh, bin/genltl.cc, bin/ltlcross.cc, bin/ltlfilt.cc, bin/ltlgrind.cc, bin/randltl.cc: Add diagnostics. * NEWS: Mention the fix. --- NEWS | 5 +++- bin/autfilt.cc | 1 + bin/common_aoutput.cc | 7 ++++++ bin/common_aoutput.hh | 1 + bin/common_file.cc | 15 +++++++++++- bin/common_file.hh | 5 +++- bin/genltl.cc | 2 ++ bin/ltlcross.cc | 2 ++ bin/ltlfilt.cc | 1 + bin/ltlgrind.cc | 2 ++ bin/randltl.cc | 2 ++ tests/Makefile.am | 1 + tests/core/full.test | 55 +++++++++++++++++++++++++++++++++++++++++++ 13 files changed, 96 insertions(+), 3 deletions(-) create mode 100644 tests/core/full.test diff --git a/NEWS b/NEWS index 59fe85c8b..f082b5087 100644 --- a/NEWS +++ b/NEWS @@ -1,6 +1,9 @@ New in spot 2.1.0a (not yet released) - Nothing yet. + Bugs fixed: + + * Fix several cases where command-line tools would fail to diagnose + write errors (e.g. when writing to filesystem that is full). New in spot 2.1 (2016-08-08) diff --git a/bin/autfilt.cc b/bin/autfilt.cc index 8cc2e7ce4..f2fdc796b 100644 --- a/bin/autfilt.cc +++ b/bin/autfilt.cc @@ -1272,5 +1272,6 @@ main(int argc, char** argv) if (automaton_format == Count) std::cout << match_count << std::endl; + check_cout(); return !match_count; } diff --git a/bin/common_aoutput.cc b/bin/common_aoutput.cc index e4682aeb8..fdc288920 100644 --- a/bin/common_aoutput.cc +++ b/bin/common_aoutput.cc @@ -409,6 +409,13 @@ void automaton_printer::add_stat(char c, const spot::printable* p) outputnamer.declare(c, p); } +automaton_printer::~automaton_printer() +{ + for (auto& p : outputfiles) + p.second->close(p.first); +} + + void printable_automaton::print(std::ostream& os, const char* pos) const { std::string options = "l"; diff --git a/bin/common_aoutput.hh b/bin/common_aoutput.hh index de078dab9..4508b8f69 100644 --- a/bin/common_aoutput.hh +++ b/bin/common_aoutput.hh @@ -242,6 +242,7 @@ class automaton_printer public: automaton_printer(stat_style input = no_input); + ~automaton_printer(); void print(const spot::twa_graph_ptr& aut, diff --git a/bin/common_file.cc b/bin/common_file.cc index 56e5dbeb6..ab89fbfe4 100644 --- a/bin/common_file.cc +++ b/bin/common_file.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015 Laboratoire de Recherche et Développement de +// Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement de // l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -41,3 +41,16 @@ output_file::output_file(const char* name) error(2, errno, "cannot open '%s'", name); os_ = of_; } + + +void output_file::close(const std::string& name) +{ + // We close of_, not os_, so that we never close std::cout. + if (os_) + os_->flush(); + if (of_) + of_->close(); + if (os_ && !*os_) + error(2, 0, "error writing to %s", + (name == "-") ? "standard output" : name.c_str()); +} diff --git a/bin/common_file.hh b/bin/common_file.hh index 8a80bc189..fba62dec0 100644 --- a/bin/common_file.hh +++ b/bin/common_file.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015 Laboratoire de Recherche et Développement de +// Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement de // l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -22,6 +22,7 @@ #include "common_sys.hh" #include #include +#include class output_file { @@ -34,6 +35,8 @@ public: // The function calls error() on... error. output_file(const char* name); + void close(const std::string& name); + ~output_file() { delete of_; diff --git a/bin/genltl.cc b/bin/genltl.cc index 4448787d5..e0c6ccb8f 100644 --- a/bin/genltl.cc +++ b/bin/genltl.cc @@ -119,6 +119,7 @@ #include "common_setup.hh" #include "common_output.hh" #include "common_range.hh" +#include "common_cout.hh" #include #include @@ -1111,5 +1112,6 @@ main(int argc, char** argv) error(2, 0, "%s", e.what()); } + flush_cout(); return 0; } diff --git a/bin/ltlcross.cc b/bin/ltlcross.cc index 51806777f..55bfdcda9 100644 --- a/bin/ltlcross.cc +++ b/bin/ltlcross.cc @@ -1396,6 +1396,7 @@ print_stats_csv(const char* filename) vstats[r][t].to_csv(out, !opt_omit); out << '\n'; } + outf.close(filename); } static void @@ -1442,6 +1443,7 @@ print_stats_json(const char* filename) out << " ]"; } out << "\n ]\n}\n"; + outf.close(filename); } int diff --git a/bin/ltlfilt.cc b/bin/ltlfilt.cc index 18682b9a1..e0e5d3534 100644 --- a/bin/ltlfilt.cc +++ b/bin/ltlfilt.cc @@ -753,6 +753,7 @@ main(int argc, char** argv) if (output_format == count_output) std::cout << match_count << std::endl; + flush_cout(); return one_match ? 0 : 1; } diff --git a/bin/ltlgrind.cc b/bin/ltlgrind.cc index 76dac8373..a67d52a36 100644 --- a/bin/ltlgrind.cc +++ b/bin/ltlgrind.cc @@ -26,6 +26,7 @@ #include "common_finput.hh" #include "common_output.hh" #include "common_conv.hh" +#include "common_cout.hh" #include @@ -194,5 +195,6 @@ main(int argc, char* argv[]) mutate_processor processor; if (processor.run()) return 2; + flush_cout(); return 0; } diff --git a/bin/randltl.cc b/bin/randltl.cc index 45cf6c507..db183d3d4 100644 --- a/bin/randltl.cc +++ b/bin/randltl.cc @@ -31,6 +31,7 @@ #include "common_range.hh" #include "common_r.hh" #include "common_conv.hh" +#include "common_cout.hh" #include #include @@ -327,5 +328,6 @@ main(int argc, char** argv) error(2, 0, "%s", e.what()); } + flush_cout(); return 0; } diff --git a/tests/Makefile.am b/tests/Makefile.am index b90f719c6..7cad228c9 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -191,6 +191,7 @@ TESTS_misc = \ core/bitvect.test \ core/intvcomp.test \ core/minusx.test \ + core/full.test \ core/trival.test TESTS_twa = \ diff --git a/tests/core/full.test b/tests/core/full.test new file mode 100644 index 000000000..3f25c60f2 --- /dev/null +++ b/tests/core/full.test @@ -0,0 +1,55 @@ +#! /bin/sh +# -*- coding: utf-8 -*- +# Copyright (C) 2016 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 || exit 1 + +set -e +test -w /dev/full || exit 77 + +# Make sure we diagnose write errors. As we use streams, the error +# usually has to be detected when closing the file. + +genltl --dac >/dev/full && exit 1 +genltl --dac | ltlfilt >/dev/full && exit 1 +genltl --dac | ltlfilt -c >/dev/full && exit 1 +genltl --eh | ltl2tgba --stats=%s >/dev/full && exit 1 +genltl --eh | ltl2tgba >/dev/full && exit 1 +randltl -n5 2 >/dev/full && exit 1 +randaut 2 >/dev/full && exit +randaut 2 --stats=%s >/dev/full && exit 1 +randaut 2 | autfilt >/dev/full && exit 1 +randaut 2 | autfilt -c >/dev/full && exit 1 +randaut 2 | autfilt --stats=%s >/dev/full && exit 1 +randaut 2 | autfilt --output=/dev/full && exit 1 +randaut 2 | autfilt --output=- >/dev/full && exit 1 +randaut 2 | dstar2tgba >/dev/full && exit 1 +randaut 2 | dstar2tgba --stats=%s >/dev/full && exit 1 +ltlgrind -f GFa >/dev/full && exit 1 +ltlcross -f GFa ltl2tgba --csv=/dev/full && exit 1 +ltlcross -f GFa ltl2tgba --csv >/dev/full && exit 1 +ltlcross -f GFa ltl2tgba --json=/dev/full && exit 1 +ltlcross -f GFa ltl2tgba --json >/dev/full && exit 1 +ltldo ltl2tgba -f GFa >/dev/full && exit 1 +ltldo ltl2tgba -f GFa --output=- >/dev/full && exit 1 +ltldo ltl2tgba -f GFa --output=/dev/full && exit 1 +ltldo ltl2tgba -f GFa --stats=%s >/dev/full && exit 1 + +: