diff --git a/lbtt/ChangeLog b/lbtt/ChangeLog index 3d865a4e8..49e4f8ce9 100644 --- a/lbtt/ChangeLog +++ b/lbtt/ChangeLog @@ -1,3 +1,12 @@ +2008-03-13 Alexandre Duret-Lutz + + * src/main.cc: Include for LONG_MAX. lbtt won't + compile with g++-4.3 otherwise. + * src/Ltl-parse.yy (matchCharactersFromStream): Declare the chars + as const to kill a g++ warning. + * src/NeverClaim-parse.yy (yyerror): Declare the error + message as const to kill a g++ warning. + 2005-08-30 Heikki Tauriainen * src/main.cc: [HAVE_ISATTY && HAVE_UNISTD_H]: Include the @@ -16,13 +25,13 @@ Update description of the --formulafile command line option. (Configuration::print): Do not display a file name when reading formulas from standard input. - + * src/SpotWrapper.h, src/SpotWrapper.cc: Merge files from Spot 0.2 (contributed by Alexandre Duret-Lutz); remove #pragma definitions. * src/ExternalTranslator.h, src/Makefile.in, src/translate.cc: Merge changes from Spot 0.2 (contributed by Alexandre Duret-Lutz). - + * doc/lbtt.texi: Fix typo in URL of the FormulaOptions block generator. Update version, add documentation and references about support for Spot. Describe the new semantics of the --formulafile @@ -124,7 +133,7 @@ log file. * configure.ac: Add test for the setsid library function. - + 2004-07-31 Heikki Tauriainen * src/Product.h (ProductEdge::edge_1, ProductEdge::edge_2): @@ -178,7 +187,7 @@ * doc/texinfo.tex: New upstream version. * doc/lbtt.texi: Update to edition 1.1.0. * NEWS: Update. - + 2004-07-02 Heikki Tauriainen * src/UserCommandReader.cc (parseCommand): Recognize @@ -257,13 +266,13 @@ New files for providing specializations of the general product computation operation applicable to Büchi automata and state spaces. - + * src/Makefile.am: Add BuchiProduct.h, BuchiProduct.cc, Product.h, SccCollection.h and StateSpaceProduct.h to lbtt_SOURCES. Remove ProductAutomaton.h, ProductAutomaton.cc and SccIterator.h from lbtt_SOURCES. - + * src/Graph.h.in (Graph::EdgeContainerType, Graph::Path): New type definitions. (Graph::PathElement): New class. @@ -337,7 +346,7 @@ (printAcceptingCycle): Update parameter list and documentation. Display all relevant information about an accepting execution of a Büchi automaton. - + 2004-05-18 Heikki Tauriainen * configure.ac (YACC): Do not add `-d' here. @@ -365,7 +374,7 @@ * src/NeverClaim-lex.ll: Add %option nounput to avoid a compiler warning. - + * src/ExternalTranslator.h: Include the TempFsysName.h header. (ExternalTranslator::TempFileObject): Remove. (ExternalTranslator::registerTempFileObject): Change @@ -475,7 +484,7 @@ command line option. (printCommandHelp): Update the description of the `formula' command. - + * src/UserCommandReader.cc (executeUserCommands): Accept one optional parameter for the `formula' command. Pass the input tokens as an additional parameter in the printFormula call. @@ -505,7 +514,7 @@ * src/TempFsysName.h, src/TempFsysName.cc New files. * src/Makefile.am: Add TempFsysName.h and TempFsysName.cc to lbtt_SOURCES. - + * src/TestRoundInfo.h: Include the TempFsysName.h header. (TestRoundInfo::formula_file_name[]) (TestRoundInfo::automaton_file_name) @@ -513,7 +522,7 @@ TempFsysName*. (TestRoundInfo::TestRoundInfo): Initialize temporary file name pointers to 0. - + * src/main.cc: Include the TempFsysName.h header. (allocateTempFilenames, deallocateTempFilenames): New functions. (abortHandler): New signal handler. @@ -858,7 +867,7 @@ after colon in output. Return 3 if an unexpected exception occurred. In this case print an additional newline before the error message. - + 2004-02-19 Heikki Tauriainen * src/StringUtil.h: Include the IntervalList.h header. @@ -926,7 +935,7 @@ Reformat the automata file format section to avoid overfull lines in dvi generation. Fix description of the Algorithm block used with lbtt-translate. - + * doc/testprocedure.txt, doc/intersectioncheck.txt: Add initial newlines. diff --git a/lbtt/src/Ltl-parse.yy b/lbtt/src/Ltl-parse.yy index 805d5965b..b308f7f30 100644 --- a/lbtt/src/Ltl-parse.yy +++ b/lbtt/src/Ltl-parse.yy @@ -1,5 +1,5 @@ /* - * Copyright (C) 2004, 2005 + * Copyright (C) 2004, 2005, 2008 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or @@ -372,7 +372,7 @@ infix_b_formula: formula LTLPARSE_AND formula *****************************************************************************/ static inline size_t matchCharactersFromStream - (istream& stream, char* chars) + (istream& stream, const char* chars) { size_t num_matched; for (num_matched = 0; *chars != '\0' && stream.peek() == *chars; ++chars) diff --git a/lbtt/src/NeverClaim-parse.yy b/lbtt/src/NeverClaim-parse.yy index bdbdfb4da..c25a1c6d3 100644 --- a/lbtt/src/NeverClaim-parse.yy +++ b/lbtt/src/NeverClaim-parse.yy @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005 + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005, 2008 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or @@ -83,7 +83,7 @@ extern int yyleng; /* Length of the last *****************************************************************************/ /* ========================================================================= */ -void yyerror(char*) +void yyerror(const char*) /* ---------------------------------------------------------------------------- * * Description: Function for reporting never claim parse errors. @@ -219,12 +219,12 @@ transition: NC_DOUBLE_COLON formula NC_RIGHT_ARROW NC_GOTO NC_LABEL ; formula: NC_PROPOSITION - { - $$ = $1; + { + $$ = $1; } | NC_TRUE - { - $$ = $1; + { + $$ = $1; } | NC_FALSE { @@ -290,7 +290,7 @@ int parseNeverClaim(FILE* stream, NeverClaimAutomaton& a) * a -- A reference to a NeverClaimAutomaton object in * which the results should be stored. * - * Returns: + * Returns: * * ------------------------------------------------------------------------- */ { diff --git a/lbtt/src/main.cc b/lbtt/src/main.cc index 4c4093da2..2aed90039 100644 --- a/lbtt/src/main.cc +++ b/lbtt/src/main.cc @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005 + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005, 2008 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or @@ -21,6 +21,7 @@ #include #include #include +#include #ifdef HAVE_SYS_TYPES_H #include #endif /* HAVE_SYS_TYPES_H */ @@ -366,7 +367,7 @@ bool testLoop() round_info.error = false; round_info.skip = (round_info.current_round < round_info.next_round_to_run); - + if (!round_info.skip) printText(string("Round ") + toString(round_info.current_round) + " of " + toString(global_options.number_of_rounds) + "\n\n", @@ -395,7 +396,7 @@ bool testLoop() configuration.global_options.statespace_random_seed = LRAND(0, RAND_MAX); #endif /* HAVE_RAND48 */ - + if (global_options.statespace_change_interval == 0) round_info.next_round_to_change_statespace = global_options.number_of_rounds + 1; @@ -433,7 +434,7 @@ bool testLoop() */ round_info.fresh_formula - = (round_info.next_round_to_change_formula + = (round_info.next_round_to_change_formula == round_info.current_round); if (round_info.fresh_formula) @@ -742,7 +743,7 @@ bool testLoop() int main(int argc, char* argv[]) { - try + try { configuration.read(argc, argv); } @@ -791,7 +792,7 @@ int main(int argc, char* argv[]) using_history(); #endif /* HAVE_READLINE */ - try + try { allocateTempFilenames(); if (!testLoop())