diff --git a/NEWS b/NEWS
index 05b277967..44a51e5e1 100644
--- a/NEWS
+++ b/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)
diff --git a/src/dstarparse/dstarscan.ll b/src/dstarparse/dstarscan.ll
index 431da852e..25e83dd26 100644
--- a/src/dstarparse/dstarscan.ll
+++ b/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();
diff --git a/src/kripkeparse/kripkescan.ll b/src/kripkeparse/kripkescan.ll
index 37df81ae3..fff7e65ad 100644
--- a/src/kripkeparse/kripkescan.ll
+++ b/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();
\" {
diff --git a/src/kripkeparse/scankripke.ll b/src/kripkeparse/scankripke.ll
deleted file mode 100644
index a3b4a2983..000000000
--- a/src/kripkeparse/scankripke.ll
+++ /dev/null
@@ -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 .
-*/
-%option noyywrap
- //%option prefix="tgbayy"
-%option prefix="kripkeyy"
-%option outfile="lex.yy.c"
-%x STATE_STRING
-
-%{
-#include
-#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. */
-{
- \" {
- BEGIN(INITIAL);
- return token::STRING;
- }
- \\["\\] yylval->str->append(1, yytext[1]);
- [^"\\]+ yylval->str->append(yytext, yyleng);
- <> {
- 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);
- }
-//}
diff --git a/src/kripketest/bad_parsing.test b/src/kripketest/bad_parsing.test
index ae5fdca7a..1e5ca5541 100755
--- a/src/kripketest/bad_parsing.test
+++ b/src/kripketest/bad_parsing.test
@@ -1,6 +1,6 @@
#! /bin/sh
-
-# Copyright (C) 2011 Laboratoire de Recherche et Developpement
+# -*- coding: utf-8 -*-
+# 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
-
diff --git a/src/neverparse/neverclaimscan.ll b/src/neverparse/neverclaimscan.ll
index 998c379c4..50ad283f3 100644
--- a/src/neverparse/neverclaimscan.ll
+++ b/src/neverparse/neverclaimscan.ll
@@ -1,5 +1,6 @@
-/* Copyright (C) 2010, 2011, 2013 Laboratoire de Recherche et
-** Développement de l'Epita (LRDE).
+/* -*- coding: utf-8 -*-
+** 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();
diff --git a/src/tgbaparse/tgbascan.ll b/src/tgbaparse/tgbascan.ll
index 83c055e4d..edc613b14 100644
--- a/src/tgbaparse/tgbascan.ll
+++ b/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();
\" {
diff --git a/src/tgbatest/neverclaimread.test b/src/tgbatest/neverclaimread.test
index baf92ab9e..a8f74c924 100755
--- a/src/tgbatest/neverclaimread.test
+++ b/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< input.dos
+mv input.dos input
+run 2 ../ltl2tgba -b -X input > stdout 2>stderr
+cat stderr
+grep input: stderr > stderrfilt
+diff stderrfilt expected