diff --git a/NEWS b/NEWS index feb630320..220947d3a 100644 --- a/NEWS +++ b/NEWS @@ -35,6 +35,9 @@ New in spot 2.11.5.dev (not yet released) where thousands of different filenames can be created failed with "Too many open files". (Issue #534) + - Using --format=... on a tool that output formulas would force + the output on standard output, even when --output was given. + New in spot 2.11.5 (2023-04-20) diff --git a/bin/common_output.cc b/bin/common_output.cc index 2f851f109..16beca34d 100644 --- a/bin/common_output.cc +++ b/bin/common_output.cc @@ -225,7 +225,7 @@ namespace } }; - class formula_printer final: protected spot::formater + class formula_printer final: public spot::formater { public: formula_printer(std::ostream& os, const char* format) @@ -399,6 +399,7 @@ output_formula(std::ostream& out, { formula_with_location fl = { f, filename, linenum, index, prefix, suffix }; + format->set_output(out); format->print(fl, ptimer); } } diff --git a/tests/core/serial.test b/tests/core/serial.test index 6f4c48c6a..7914316c8 100755 --- a/tests/core/serial.test +++ b/tests/core/serial.test @@ -78,3 +78,16 @@ test 2000 = `ls -l randaut-*.hoa | wc -l` # likewise for LTL formulas randltl 2 -n 2000 -o randltl-%l.ltl test 2000 = `ls -l randltl-*.ltl | wc -l` + + +# Test the code path that works that has to reopen files +randltl -n100 --tree-size 1 26 --allow-dups -o '%f'.ltl --format=pass1 +randltl -n100 --tree-size 1 26 --allow-dups -o '>>%f'.ltl --format=pass2 +(uniq -c p1.ltl; uniq -c p20.ltl) | sed 's/^ *\([0-9][0-9]*\) */\1 /g' >out +cat >expected <