fix line number tracking in files with DOS newlines

* src/dstarparse/dstarscan.ll, src/kripkeparse/kripkescan.ll,
src/neverparse/neverclaimscan.ll, src/tgbaparse/tgbascan.ll:
Distinguish between 1-sized EOL and 2-sized EOL.
* src/kripketest/bad_parsing.test, src/tgbatest/neverclaimread.test,
src/tgbatest/readsave.test: Add more tests.
* NEWS: Mention it.
* src/kripkeparse/scankripke.ll: Remove this unused file.

NEWS

@@ -170,6 +170,8 @@ New in spot 1.2.5a (not yet released)
       in Spot.  The workaround (not assigning sets) is actually more
       efficient, so we can consider it as a bug fix, even though
       libstd++ has also been fixed.
+    - all parsers would report wrong line numbers while processing
+      files with DOS style newlines.
 
 New in spot 1.2.5 (2014-08-21)
 

src/dstarparse/dstarscan.ll

@@ -1,4 +1,4 @@
-/* Copyright (C) 2013 Laboratoire de Recherche et Développement
+/* Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement
 ** de l'Epita (LRDE).
 **
 ** This file is part of Spot, a model checking library.
@@ -31,7 +31,8 @@
 typedef dstaryy::parser::token token;
 %}
 
-eol      \n|\r|\n\r|\r\n
+eol      \n+|\r+
+eol2     (\n\r)+|(\r\n)+
 %x in_COMMENT in_STRING
 
 %%
@@ -42,6 +43,7 @@ eol      \n|\r|\n\r|\r\n
 %}
 
 {eol}			yylloc->lines(yyleng); return token::EOL;
+{eol2}			yylloc->lines(yyleng / 2); return token::EOL;
 
                         /* skip blanks and comments */
 [ \t]+			yylloc->step();

src/kripkeparse/kripkescan.ll

@@ -1,4 +1,4 @@
-/* Copyright (C) 2011 Laboratoire de Recherche et Developpement
+/* Copyright (C) 2011, 2014 Laboratoire de Recherche et Developpement
 * de l'Epita (LRDE)
 *
 * This file is part of Spot, a model checking library.
@@ -36,7 +36,8 @@
 
 %}
 
-eol      \n|\r|\n\r|\r\n
+eol      \n+|\r+
+eol2     (\n\r)+|(\r\n)+
 
 %%
 
@@ -51,6 +52,7 @@ eol      \n|\r|\n\r|\r\n
 
 			/* discard whitespace */
 {eol}			yylloc->lines(yyleng); yylloc->step();
+{eol2}			yylloc->lines(yyleng / 2); yylloc->step();
 [ \t]+			yylloc->step();
 
 \"			{

src/kripkeparse/scankripke.ll

@@ -1,115 +0,0 @@
-/* Copyright (C) 2011  Laboratoire d'Informatique de Paris 6 (LIP6),
-** département Systèmes Répartis Coopératifs (SRC), Université Pierre
-** et Marie Curie.
-**
-** 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/>.
-*/
-%option noyywrap
- //%option prefix="tgbayy"
-%option prefix="kripkeyy"
-%option outfile="lex.yy.c"
-%x STATE_STRING
-
-%{
-#include <string>
-#include "parsekripke.tab.hh"
-
-
-#define YY_USER_ACTION \
-  yylloc->columns(yyleng);
-
-#define YY_NEVER_INTERACTIVE 1
-
-   typedef kripkeyy::parser::token token;
-
-
-%}
-
-eol      \n|\r|\n\r|\r\n
-
-%%
-
-%{
-  yylloc->step ();
-%}
-
-[a-zA-Z][a-zA-Z0-9_]*   {
-			  yylval->str = new std::string(yytext, yyleng);
-			  return token::IDENT;
-			}
-
-			/* discard whitespace */
-{eol}			yylloc->lines(yyleng); yylloc->step();
-[ \t]+			yylloc->step();
-
-\"			{
-			  yylval->str = new std::string;
-			  BEGIN(STATE_STRING);
-			}
-
-","                     {
-                           return token::COMA;
-                         }
-
-";"                     return token::SEMICOL;
-
-.			return *yytext;
-
-  /* Handle \" and \\ in strings.  */
-<STATE_STRING>{
-  \"                    {
-                          BEGIN(INITIAL);
-			  return token::STRING;
-                        }
-  \\["\\]               yylval->str->append(1, yytext[1]);
-  [^"\\]+               yylval->str->append(yytext, yyleng);
-  <<EOF>>		{
-  			  BEGIN(INITIAL);
-			  return token::UNTERMINATED_STRING;
-			}
-}
-
-%{
-  /* Dummy use of yyunput to shut up a gcc warning.  */
-  (void) &yyunput;
-%}
-
-%%
-
- //namespace spot
- //{
-  int
-  kripkeyyopen(const std::string &name)
-  {
-    if (name == "-")
-      {
-        yyin = stdin;
-      }
-    else
-      {
-        yyin = fopen(name.c_str(), "r");
-        if (!yyin)
-	  return 1;
-      }
-    return 0;
-  }
-
-  void
-  kripkeyyclose()
-  {
-    fclose(yyin);
-  }
-//}

src/kripketest/bad_parsing.test

@@ -1,6 +1,6 @@
 #! /bin/sh
-
+# -*- coding: utf-8 -*-
-# Copyright (C) 2011 Laboratoire de Recherche et Developpement
+# Copyright (C) 2011, 2014 Laboratoire de Recherche et Développement
 # de l'Epita (LRDE)
 #
 # This file is part of Spot, a model checking library.
@@ -67,6 +67,14 @@ run 1 ../parse_print input 2> output
 cat output | grep -v + > res
 diff expected res
 
+# The diagnostic should be the same with DOS return lines
+sed 's/$/\r/' input > input.dos
+mv input.dos input
+run 1 ../parse_print input 2> output
+cat output | grep -v + > res
+diff expected res
+
+
 rm -f output res expected
 
 cat >input <<\EOF
@@ -86,4 +94,3 @@ cat output | grep -v + > res
 diff expected res
 
 rm -f output res expected
-

src/neverparse/neverclaimscan.ll

@@ -1,5 +1,6 @@
-/* Copyright (C) 2010, 2011, 2013 Laboratoire de Recherche et
+/* -*- coding: utf-8 -*-
-** Développement de l'Epita (LRDE).
+** Copyright (C) 2010, 2011, 2013, 2014 Laboratoire de Recherche et
+** Développement de l'Epita (LRDE).
 **
 ** This file is part of Spot, a model checking library.
 **
@@ -38,7 +39,8 @@ static bool missing_parent = false;
 
 %x in_par
 
-eol      \n|\r|\n\r|\r\n
+eol      \n+|\r+
+eol2     (\n\r)+|(\r\n)+
 
 %%
 
@@ -48,6 +50,7 @@ eol      \n|\r|\n\r|\r\n
 
                         /* skip blanks */
 {eol}			yylloc->lines(yyleng); yylloc->step();
+{eol2}			yylloc->lines(yyleng / 2); yylloc->step();
 [ \t]+			yylloc->step();
 "/*".*"*/"		yylloc->step();
 

src/tgbaparse/tgbascan.ll

@@ -1,7 +1,8 @@
-/* Copyright (C) 2011, Laboratoire de Recherche et Développement de
+/* -*- coding: utf-8 -*-
+** Copyright (C) 2011, 2014, Laboratoire de Recherche et Développement de
 ** l'Epita (LRDE).
 ** Copyright (C) 2003, 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
-** département Systèmes Répartis Coopératifs (SRC), Université Pierre
+** département Systèmes Répartis Coopératifs (SRC), Université Pierre
 ** et Marie Curie.
 **
 ** This file is part of Spot, a model checking library.
@@ -37,7 +38,8 @@ typedef tgbayy::parser::token token;
 
 %}
 
-eol      \n|\r|\n\r|\r\n
+eol      \n+|\r+
+eol2     (\n\r)+|(\r\n)+
 
 %%
 
@@ -54,6 +56,7 @@ acc[ \t]*=		return token::ACC_DEF;
 
 			/* discard whitespace */
 {eol}			yylloc->lines(yyleng); yylloc->step();
+{eol2}			yylloc->lines(yyleng / 2); yylloc->step();
 [ \t]+			yylloc->step();
 
 \"			{

src/tgbatest/neverclaimread.test

@@ -287,6 +287,14 @@ EOF
 grep input: stderr > stderrfilt
 diff stderrfilt expected-err
 
+# DOS-style new lines should have the same output.
+sed 's/$/\r/g' input > input.dos
+mv input.dos input
+run 2 ../ltl2tgba -ks -XN input > stdout 2>stderr
+cat stderr
+grep input: stderr > stderrfilt
+diff stderrfilt expected-err
+
 cat >formulae<<EOF
 a
 FG a

src/tgbatest/readsave.test

@@ -120,3 +120,11 @@ input:4.20: ignoring trailing garbage
 EOF
 
 diff stderrfilt expected
+
+# The diagnostic should be the same with DOS input
+sed 's/$/\r/' input > input.dos
+mv input.dos input
+run 2 ../ltl2tgba -b -X input > stdout 2>stderr
+cat stderr
+grep input: stderr > stderrfilt
+diff stderrfilt expected