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.
This commit is contained in:
Alexandre Duret-Lutz
parent
becfcbcf79
commit
f8cf2aa9b3
9 changed files with 48 additions and 128 deletions
2
NEWS
2
NEWS
|
|
@ -29,6 +29,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)
|
||||
|
||||
|
|
|
|||
|
|
@ -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();
|
||||
|
|
|
|||
|
|
@ -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();
|
||||
|
||||
\" {
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
}
|
||||
//}
|
||||
|
|
@ -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
|
||||
|
||||
|
|
|
|||
|
|
@ -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();
|
||||
|
||||
|
|
|
|||
|
|
@ -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();
|
||||
|
||||
\" {
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -114,3 +114,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
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue