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

Fix column in LTL error messages, it was off by one.

Browse source 
* src/ltlparse/fmterror.cc (format_parse_errors): Count columns
starting at 1.  Older Bison used to start at 0 but changed to
match the GNU Coding Standards.
* src/ltltest/parseerr.test: Add a test case.
This commit is contained in:
Alexandre Duret-Lutz 2010-03-10 15:17:05 +01:00
parent 3cf2ddbcb0
commit d71ceb3b04
3 changed files with 39 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

9
ChangeLog
View file

@ -1,3 +1,12 @@
2010-03-10 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Fix column in LTL error messages, it was off by one.
* src/ltlparse/fmterror.cc (format_parse_errors): Count columns
starting at 1. Older Bison used to start at 0 but changed to
match the GNU Coding Standards.
* src/ltltest/parseerr.test: Add a test case.
2010-03-07 Alexandre Duret-Lutz <adl@lrde.epita.fr> 2010-03-07 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Do not rewrite F(a & GF(b)) = F(a) & GF(b), this can be harmful. Do not rewrite F(a & GF(b)) = F(a) & GF(b), this can be harmful.

10
src/ltlparse/fmterror.cc
View file

@ -1,6 +1,8 @@
// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // Copyright (C) 2010 Laboratoire de Recherche et Développement de
// département Systèmes Répartis Coopératifs (SRC), Université Pierre // l'Epita (LRDE).
// et Marie Curie. // Copyright (C) 2003, 2004, 2005 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. // This file is part of Spot, a model checking library.
// //
@ -39,7 +41,7 @@ namespace spot
os << ">>> " << ltl_string << std::endl; os << ">>> " << ltl_string << std::endl;
ltlyy::location& l = it->first; ltlyy::location& l = it->first;
unsigned n = 0; unsigned n = 1;
for (; n < 4 + l.begin.column; ++n) for (; n < 4 + l.begin.column; ++n)
os << ' '; os << ' ';
// Write at least one '^', even if begin==end. // Write at least one '^', even if begin==end.

27
src/ltltest/parseerr.test
View file

@ -1,5 +1,5 @@
#! /bin/sh #! /bin/sh
# Copyright (C) 2009 Laboratoire de Recherche et Développement # Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement
# de l'Epita (LRDE). # de l'Epita (LRDE).
# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), # 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
@ -30,7 +30,7 @@
check() check()
{ {
run 1 ../ltl2text "$1" >stdout set +x; run 1 ../ltl2text "$1" >stdout 2>stderr; set -x
if test -n "$2"; then if test -n "$2"; then
echo "$2" >expect echo "$2" >expect
else else
@ -43,9 +43,21 @@ check()
cat stdout cat stdout
echo "instead of" echo "instead of"
cat expect cat expect
rm -f stdout expect
exit 1 exit 1
fi fi
if test -n "$3"; then
echo "$3" >expect
if cmp stderr expect; then
:
else
echo "==== Error output was ===="
cat stderr
echo "==== instead of ===="
cat expect
exit 1
fi
fi
} }
# Empty or unparsable strings # Empty or unparsable strings
@ -72,3 +84,12 @@ run 0 ../equals -E 'a & (a + b' 'a & (a + b)'
run 0 ../equals -E 'a & (a + b c' 'a & (0)' run 0 ../equals -E 'a & (a + b c' 'a & (0)'
run 0 ../equals -E 'a & (+' 'a & (0)' run 0 ../equals -E 'a & (+' 'a & (0)'
run 0 ../equals -E 'a & (' 'a & (0)' run 0 ../equals -E 'a & (' 'a & (0)'
check 'a - b' 'AP(a)' '>>> a - b
^
syntax error, unexpected $undefined
>>> a - b
^^^
ignoring trailing garbage
'