From 5cd58f9aafdc1887fce164a8c6de6ec81c0116a9 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 1 Feb 2005 18:03:00 +0000 Subject: [PATCH] * src/evtgbaparse/evtgbaparse.yy, src/evtgbaparse/evtgbascan.ll, src/evtgbaparse/fmterror.cc, src/evtgbaparse/parsedecl.hh, src/evtgbaparse/public.hh, src/evtgbatest/product.cc, src/evtgbatest/readsave.cc, src/ltlparse/fmterror.cc, src/ltlparse/ltlparse.yy, src/ltlparse/parsedecl.hh, src/ltlparse/public.hh, src/tgbaparse/parsedecl.hh, src/tgbaparse/public.hh, src/tgbaparse/tgbaparse.yy: Update to Bison 2.0. --- ChangeLog | 9 +++++++++ HACKING | 2 +- src/evtgbaparse/evtgbaparse.yy | 22 +++++++++++----------- src/evtgbaparse/evtgbascan.ll | 12 +----------- src/evtgbaparse/fmterror.cc | 8 +++++--- src/evtgbaparse/parsedecl.hh | 4 ++-- src/evtgbaparse/public.hh | 6 ++++-- src/evtgbatest/product.cc | 6 ++++-- src/evtgbatest/readsave.cc | 5 +++-- src/ltlparse/fmterror.cc | 4 ++-- src/ltlparse/ltlparse.yy | 16 ++++++---------- src/ltlparse/parsedecl.hh | 4 ++-- src/ltlparse/public.hh | 4 ++-- src/tgbaparse/parsedecl.hh | 4 ++-- src/tgbaparse/public.hh | 2 +- src/tgbaparse/tgbaparse.yy | 22 +++++++++------------- 16 files changed, 64 insertions(+), 66 deletions(-) diff --git a/ChangeLog b/ChangeLog index 404045b24..fcce0f7e2 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,14 @@ 2005-02-01 Alexandre Duret-Lutz + * src/evtgbaparse/evtgbaparse.yy, src/evtgbaparse/evtgbascan.ll, + src/evtgbaparse/fmterror.cc, src/evtgbaparse/parsedecl.hh, + src/evtgbaparse/public.hh, src/evtgbatest/product.cc, + src/evtgbatest/readsave.cc, src/ltlparse/fmterror.cc, + src/ltlparse/ltlparse.yy, src/ltlparse/parsedecl.hh, + src/ltlparse/public.hh, src/tgbaparse/parsedecl.hh, + src/tgbaparse/public.hh, src/tgbaparse/tgbaparse.yy: Update + to Bison 2.0. + * bench/emptchk/pml2tgba.pl (usage): Correct description. From Denis. * bench/emptchk/README: Timing info from Denis. diff --git a/HACKING b/HACKING index 747e73678..7455491df 100644 --- a/HACKING +++ b/HACKING @@ -13,7 +13,7 @@ generally if you plan to regenerate some of the generated files. GNU Automake >= 1.9 GNU Libtool >= 1.4 GNU Flex (the version probably doesn't matter much, we used 2.5.31) - The CVS version of GNU Bison (called 1.875c at the time of writing) + GNU Bison >= 2.0 SWIG >= 1.3.23 Doxygen >= 1.4.0 diff --git a/src/evtgbaparse/evtgbaparse.yy b/src/evtgbaparse/evtgbaparse.yy index a5a24abbc..889e1a705 100644 --- a/src/evtgbaparse/evtgbaparse.yy +++ b/src/evtgbaparse/evtgbaparse.yy @@ -1,4 +1,4 @@ -/* Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +/* Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), ** département Systèmes Répartis Coopératifs (SRC), Université Pierre ** et Marie Curie. ** @@ -55,6 +55,12 @@ %token ACC_DEF %token INIT_DEF +%destructor { delete $$; } STRING UNTERMINATED_STRING IDENT + strident string acc_list + +%printer { debug_stream() << *$$; } STRING UNTERMINATED_STRING IDENT + strident string + %% evtgba: lines @@ -114,14 +120,7 @@ init_decl: %% void -yy::Parser::print_() -{ - if (looka_ == STRING || looka_ == IDENT) - YYCDEBUG << " '" << *value.str << "'"; -} - -void -yy::Parser::error_() +yy::parser::error(const location_type& location, const std::string& message) { error_list.push_back(spot::evtgba_parse_error(location, message)); } @@ -136,12 +135,13 @@ namespace spot if (evtgbayyopen(name)) { error_list.push_back - (evtgba_parse_error(yy::Location(), + (evtgba_parse_error(yy::location(), std::string("Cannot open file ") + name)); return 0; } evtgba_explicit* result = new evtgba_explicit(); - evtgbayy::Parser parser(debug, yy::Location(), error_list, result); + evtgbayy::parser parser(error_list, result); + parser.set_debug_level(debug); parser.parse(); evtgbayyclose(); return result; diff --git a/src/evtgbaparse/evtgbascan.ll b/src/evtgbaparse/evtgbascan.ll index a25dd3e64..2302569f2 100644 --- a/src/evtgbaparse/evtgbascan.ll +++ b/src/evtgbaparse/evtgbascan.ll @@ -1,4 +1,4 @@ -/* Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +/* Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), ** département Systèmes Répartis Coopératifs (SRC), Université Pierre ** et Marie Curie. ** @@ -31,16 +31,8 @@ #define YY_USER_ACTION \ yylloc->columns(yyleng); -#define YY_USER_INIT \ - do { \ - yylloc->begin.filename = current_file; \ - yylloc->end.filename = current_file; \ - } while (0) - #define YY_NEVER_INTERACTIVE 1 -static std::string current_file; - %} eol \n|\r|\n\r|\r\n @@ -99,12 +91,10 @@ namespace spot if (name == "-") { yyin = stdin; - current_file = "standard input"; } else { yyin = fopen (name.c_str (), "r"); - current_file = name; if (!yyin) return 1; } diff --git a/src/evtgbaparse/fmterror.cc b/src/evtgbaparse/fmterror.cc index 2469a47dd..d6fda032d 100644 --- a/src/evtgbaparse/fmterror.cc +++ b/src/evtgbaparse/fmterror.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// 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. // @@ -26,14 +26,16 @@ namespace spot { bool format_evtgba_parse_errors(std::ostream& os, + const std::string& filename, evtgba_parse_error_list& error_list) { bool printed = false; spot::evtgba_parse_error_list::iterator it; for (it = error_list.begin(); it != error_list.end(); ++it) { - if (it->first.begin.filename != "") - os << it->first << ": "; + if (filename != "-") + os << filename << ":"; + os << it->first << ": "; os << it->second << std::endl; printed = true; } diff --git a/src/evtgbaparse/parsedecl.hh b/src/evtgbaparse/parsedecl.hh index 8843c1f8d..a41c585f7 100644 --- a/src/evtgbaparse/parsedecl.hh +++ b/src/evtgbaparse/parsedecl.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// 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. // @@ -27,7 +27,7 @@ #include "location.hh" # define YY_DECL \ - int evtgbayylex (yystype *yylval, yy::Location *yylloc) + int evtgbayylex (yystype *yylval, yy::location *yylloc) YY_DECL; namespace spot diff --git a/src/evtgbaparse/public.hh b/src/evtgbaparse/public.hh index e1851de9f..5f8824058 100644 --- a/src/evtgbaparse/public.hh +++ b/src/evtgbaparse/public.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// 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. // @@ -32,7 +32,7 @@ namespace spot { /// \brief A parse diagnostic with its location. - typedef std::pair evtgba_parse_error; + typedef std::pair evtgba_parse_error; /// \brief A list of parser diagnostics, as filled by parse. typedef std::list evtgba_parse_error_list; @@ -56,10 +56,12 @@ namespace spot /// \brief Format diagnostics produced by spot::evtgba_parse. /// \param os Where diagnostics should be output. + /// \param filename The filename that should appear in the diagnostics. /// \param error_list The error list filled by spot::ltl::parse while /// parsing \a ltl_string. /// \return \c true iff any diagnostic was output. bool format_evtgba_parse_errors(std::ostream& os, + const std::string& filename, evtgba_parse_error_list& error_list); } diff --git a/src/evtgbatest/product.cc b/src/evtgbatest/product.cc index 2e3d1524c..49250bde5 100644 --- a/src/evtgbatest/product.cc +++ b/src/evtgbatest/product.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -67,7 +67,9 @@ main(int argc, char** argv) spot::evtgba_explicit* a = spot::evtgba_parse(argv[filename_index], pel, debug); - exit_code = spot::format_evtgba_parse_errors(std::cerr, pel); + exit_code = spot::format_evtgba_parse_errors(std::cerr, + argv[filename_index], + pel); if (a) { diff --git a/src/evtgbatest/readsave.cc b/src/evtgbatest/readsave.cc index 1b8bb0ac6..755677270 100644 --- a/src/evtgbatest/readsave.cc +++ b/src/evtgbatest/readsave.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -54,7 +54,8 @@ main(int argc, char** argv) spot::evtgba_explicit* a = spot::evtgba_parse(argv[filename_index], pel, debug); - exit_code = spot::format_evtgba_parse_errors(std::cerr, pel); + exit_code = spot::format_evtgba_parse_errors(std::cerr, argv[filename_index], + pel); if (a) { diff --git a/src/ltlparse/fmterror.cc b/src/ltlparse/fmterror.cc index bf4b396d8..7e2765d92 100644 --- a/src/ltlparse/fmterror.cc +++ b/src/ltlparse/fmterror.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// 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. // @@ -37,7 +37,7 @@ namespace spot for (it = error_list.begin(); it != error_list.end(); ++it) { os << ">>> " << ltl_string << std::endl; - yy::Location& l = it->first; + yy::location& l = it->first; unsigned n = 0; for (; n < 4 + l.begin.column; ++n) diff --git a/src/ltlparse/ltlparse.yy b/src/ltlparse/ltlparse.yy index 9a1f89d5a..f487834f4 100644 --- a/src/ltlparse/ltlparse.yy +++ b/src/ltlparse/ltlparse.yy @@ -1,4 +1,4 @@ -/* Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +/* 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. ** @@ -111,6 +111,8 @@ using namespace spot::ltl; %destructor { delete $$; } "atomic proposition" %destructor { spot::ltl::destroy($$); } result subformula +%printer { debug_stream() << *$$; } "atomic proposition" + %% result: subformula END_OF_INPUT { result = $$ = $1; @@ -260,14 +262,7 @@ subformula: ATOMIC_PROP %% void -yy::Parser::print_() -{ - if (looka_ == ATOMIC_PROP) - YYCDEBUG << " '" << *value.str << "'"; -} - -void -yy::Parser::error_() +yy::parser::error(const location_type& location, const std::string& message) { error_list.push_back(parse_error(location, message)); } @@ -284,7 +279,8 @@ namespace spot { formula* result = 0; flex_set_buffer(ltl_string.c_str()); - yy::Parser parser(debug, yy::Location(), error_list, env, result); + yy::parser parser(error_list, env, result); + parser.set_debug_level(debug); parser.parse(); return result; } diff --git a/src/ltlparse/parsedecl.hh b/src/ltlparse/parsedecl.hh index cf5f7f2e4..f6c1217cc 100644 --- a/src/ltlparse/parsedecl.hh +++ b/src/ltlparse/parsedecl.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2003, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -26,7 +26,7 @@ #include "location.hh" # define YY_DECL \ - int ltlyylex (yystype *yylval, yy::Location *yylloc) + int ltlyylex (yystype *yylval, yy::location *yylloc) YY_DECL; void flex_set_buffer(const char *buf); diff --git a/src/ltlparse/public.hh b/src/ltlparse/public.hh index 33b37f7b5..a4297452c 100644 --- a/src/ltlparse/public.hh +++ b/src/ltlparse/public.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// 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. // @@ -38,7 +38,7 @@ namespace spot /// @{ /// \brief A parse diagnostic with its location. - typedef std::pair parse_error; + typedef std::pair parse_error; /// \brief A list of parser diagnostics, as filled by parse. typedef std::list parse_error_list; diff --git a/src/tgbaparse/parsedecl.hh b/src/tgbaparse/parsedecl.hh index 65c48b399..27a9fc2ac 100644 --- a/src/tgbaparse/parsedecl.hh +++ b/src/tgbaparse/parsedecl.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2003, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -27,7 +27,7 @@ #include "location.hh" # define YY_DECL \ - int tgbayylex (yystype *yylval, yy::Location *yylloc) + int tgbayylex (yystype *yylval, yy::location *yylloc) YY_DECL; namespace spot diff --git a/src/tgbaparse/public.hh b/src/tgbaparse/public.hh index b9970abb2..0c79c16ce 100644 --- a/src/tgbaparse/public.hh +++ b/src/tgbaparse/public.hh @@ -36,7 +36,7 @@ namespace spot /// @{ /// \brief A parse diagnostic with its location. - typedef std::pair tgba_parse_error; + typedef std::pair tgba_parse_error; /// \brief A list of parser diagnostics, as filled by parse. typedef std::list tgba_parse_error_list; diff --git a/src/tgbaparse/tgbaparse.yy b/src/tgbaparse/tgbaparse.yy index 2740137f9..e027e9144 100644 --- a/src/tgbaparse/tgbaparse.yy +++ b/src/tgbaparse/tgbaparse.yy @@ -1,4 +1,4 @@ -/* Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +/* 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. ** @@ -80,6 +80,9 @@ typedef std::map formula_cache; delete $$; } acc_list +%printer { debug_stream() << *$$; } STRING UNTERMINATED_STRING IDENT + strident string condition + %% tgba: acceptance_decl lines | acceptance_decl @@ -110,7 +113,7 @@ line: strident ',' strident ',' condition ',' acc_list ';' i != pel.end(); ++i) { // Adjust the diagnostic to the current position. - Location here = @1; + location here = @1; here.begin.line += i->first.begin.line; here.begin.column += i->first.begin.column; here.end.line = @@ -201,14 +204,7 @@ acc_decl: %% void -yy::Parser::print_() -{ - if (looka_ == STRING || looka_ == IDENT) - YYCDEBUG << " '" << *value.str << "'"; -} - -void -yy::Parser::error_() +yy::parser::error(const location_type& location, const std::string& message) { error_list.push_back(spot::tgba_parse_error(location, message)); } @@ -225,14 +221,14 @@ namespace spot if (tgbayyopen(name)) { error_list.push_back - (tgba_parse_error(yy::Location(), + (tgba_parse_error(yy::location(), std::string("Cannot open file ") + name)); return 0; } formula_cache fcache; tgba_explicit* result = new tgba_explicit(dict); - tgbayy::Parser parser(debug, yy::Location(), error_list, - env, result, fcache); + tgbayy::parser parser(error_list, env, result, fcache); + parser.set_debug_level(debug); parser.parse(); tgbayyclose(); return result;