From addaf7f5b05d2874ea85cb816346826f174072fe Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Sat, 7 Mar 2020 21:33:01 +0100
Subject: [PATCH] ltlcross: detect write errors for --save-bogus, --grind, etc

* bin/ltlcross.cc: Explicitly close those file to check for
error conditions.
* tests/core/full.test: Add one test.
---
 bin/ltlcross.cc      | 23 +++++++++++++++++------
 tests/core/full.test |  6 ++++--
 2 files changed, 21 insertions(+), 8 deletions(-)

diff --git a/bin/ltlcross.cc b/bin/ltlcross.cc
index e4482aa87..4526d90cd 100644
--- a/bin/ltlcross.cc
+++ b/bin/ltlcross.cc
@@ -224,6 +224,7 @@ static bool products_avg = true;
 static bool opt_omit = false;
 static const char* bogus_output_filename = nullptr;
 static output_file* bogus_output = nullptr;
+static const char* grind_output_filename = nullptr;
 static output_file* grind_output = nullptr;
 static const char* saved_inclusion_products_filename = nullptr;
 static output_file* saved_inclusion_products = nullptr;
@@ -513,6 +514,7 @@ parse_opt(int key, char* arg, struct argp_state*)
       fail_on_timeout = true;
       break;
     case OPT_GRIND:
+      grind_output_filename = arg;
       grind_output = new output_file(arg);
       break;
     case OPT_IGNORE_EXEC_FAIL:
@@ -1819,12 +1821,21 @@ main(int argc, char** argv)
             }
         }
 
-      // FIXME: I think we should call close() on all these files
-      // before deleting them.  Otherwise we fail to report write
-      // errors.
-      delete bogus_output;
-      delete grind_output;
-      delete saved_inclusion_products;
+      if (bogus_output)
+        {
+          bogus_output->close(bogus_output_filename);
+          delete bogus_output;
+        }
+      if (grind_output)
+        {
+          grind_output->close(grind_output_filename);
+          delete grind_output;
+        }
+      if (saved_inclusion_products)
+        {
+          saved_inclusion_products->close(saved_inclusion_products_filename);
+          delete saved_inclusion_products;
+        }
 
       if (json_output)
         print_stats_json(json_output);
diff --git a/tests/core/full.test b/tests/core/full.test
index 3f25c60f2..a1df7b83d 100644
--- a/tests/core/full.test
+++ b/tests/core/full.test
@@ -1,7 +1,7 @@
 #! /bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2016 Laboratoire de Recherche et Développement de
-# l'Epita (LRDE).
+# Copyright (C) 2016, 2020 Laboratoire de Recherche et Développement
+# de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
 #
@@ -47,6 +47,8 @@ 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
+ltlcross -f GFa ltl2tgba --save-inclusion-products=/dev/full && exit 1
+ltlcross -f GFa ltl2tgba --save-inclusion-products=- >/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