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

@@ -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)
 

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;
 }

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";

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,

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());
+}

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 <iosfwd>
 #include <fstream>
+#include <error.h>
 
 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_;

bin/genltl.cc

@@ -119,6 +119,7 @@
 #include "common_setup.hh"
 #include "common_output.hh"
 #include "common_range.hh"
+#include "common_cout.hh"
 
 #include <cassert>
 #include <iostream>
@@ -1111,5 +1112,6 @@ main(int argc, char** argv)
       error(2, 0, "%s", e.what());
     }
 
+  flush_cout();
   return 0;
 }

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

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;
 }

bin/ltlgrind.cc

@@ -26,6 +26,7 @@
 #include "common_finput.hh"
 #include "common_output.hh"
 #include "common_conv.hh"
+#include "common_cout.hh"
 
 #include <spot/tl/mutation.hh>
 
@@ -194,5 +195,6 @@ main(int argc, char* argv[])
   mutate_processor processor;
   if (processor.run())
     return 2;
+  flush_cout();
   return 0;
 }

bin/randltl.cc

@@ -31,6 +31,7 @@
 #include "common_range.hh"
 #include "common_r.hh"
 #include "common_conv.hh"
+#include "common_cout.hh"
 
 #include <sstream>
 #include <spot/tl/randomltl.hh>
@@ -327,5 +328,6 @@ main(int argc, char** argv)
       error(2, 0, "%s", e.what());
     }
 
+  flush_cout();
   return 0;
 }

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 = \

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 <http://www.gnu.org/licenses/>.
+
+
+. ./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
+
+: