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

ltlcross: detect write errors for --save-bogus, --grind, etc

Browse source 
* bin/ltlcross.cc: Explicitly close those file to check for
error conditions.
* tests/core/full.test: Add one test.
This commit is contained in:
Alexandre Duret-Lutz 2020-03-07 21:33:01 +01:00
parent 3805b63e24
commit addaf7f5b0
2 changed files with 21 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

17
bin/ltlcross.cc
View file

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

6
tests/core/full.test
View file

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