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

* src/main.cc: Include <climits> for LONG_MAX. lbtt won't

Browse source 
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.
This commit is contained in:
Alexandre Duret-Lutz 2008-03-13 11:28:18 +01:00
parent 5ef7084b61
commit ab1a2ae5d7
4 changed files with 38 additions and 28 deletions
Download patch file Download diff file Expand all files Collapse all files

35
lbtt/ChangeLog
View file

@ -1,3 +1,12 @@
2008-03-13 Alexandre Duret-Lutz <adl@lrde.epita.fr>
* src/main.cc: Include <climits> 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 <heikki.tauriainen@tkk.fi> 2005-08-30 Heikki Tauriainen <heikki.tauriainen@tkk.fi>
* src/main.cc: [HAVE_ISATTY && HAVE_UNISTD_H]: Include the * src/main.cc: [HAVE_ISATTY && HAVE_UNISTD_H]: Include the
@ -16,13 +25,13 @@
Update description of the --formulafile command line option. Update description of the --formulafile command line option.
(Configuration::print): Do not display a file name when reading (Configuration::print): Do not display a file name when reading
formulas from standard input. formulas from standard input.
* src/SpotWrapper.h, src/SpotWrapper.cc: Merge files from * src/SpotWrapper.h, src/SpotWrapper.cc: Merge files from
Spot 0.2 (contributed by Alexandre Duret-Lutz); remove #pragma Spot 0.2 (contributed by Alexandre Duret-Lutz); remove #pragma
definitions. definitions.
* src/ExternalTranslator.h, src/Makefile.in, src/translate.cc: * src/ExternalTranslator.h, src/Makefile.in, src/translate.cc:
Merge changes from Spot 0.2 (contributed by Alexandre Duret-Lutz). Merge changes from Spot 0.2 (contributed by Alexandre Duret-Lutz).
* doc/lbtt.texi: Fix typo in URL of the FormulaOptions block * doc/lbtt.texi: Fix typo in URL of the FormulaOptions block
generator. Update version, add documentation and references about generator. Update version, add documentation and references about
support for Spot. Describe the new semantics of the --formulafile support for Spot. Describe the new semantics of the --formulafile
@ -124,7 +133,7 @@
log file. log file.
* configure.ac: Add test for the setsid library function. * configure.ac: Add test for the setsid library function.
2004-07-31 Heikki Tauriainen <heikki.tauriainen@hut.fi> 2004-07-31 Heikki Tauriainen <heikki.tauriainen@hut.fi>
* src/Product.h (ProductEdge::edge_1, ProductEdge::edge_2): * src/Product.h (ProductEdge::edge_1, ProductEdge::edge_2):
@ -178,7 +187,7 @@
* doc/texinfo.tex: New upstream version. * doc/texinfo.tex: New upstream version.
* doc/lbtt.texi: Update to edition 1.1.0. * doc/lbtt.texi: Update to edition 1.1.0.
* NEWS: Update. * NEWS: Update.
2004-07-02 Heikki Tauriainen <heikki.tauriainen@hut.fi> 2004-07-02 Heikki Tauriainen <heikki.tauriainen@hut.fi>
* src/UserCommandReader.cc (parseCommand): Recognize * src/UserCommandReader.cc (parseCommand): Recognize
@ -257,13 +266,13 @@
New files for providing specializations of the general product New files for providing specializations of the general product
computation operation applicable to Büchi automata and state computation operation applicable to Büchi automata and state
spaces. spaces.
* src/Makefile.am: Add BuchiProduct.h, BuchiProduct.cc, * src/Makefile.am: Add BuchiProduct.h, BuchiProduct.cc,
Product.h, SccCollection.h and StateSpaceProduct.h to Product.h, SccCollection.h and StateSpaceProduct.h to
lbtt_SOURCES. lbtt_SOURCES.
Remove ProductAutomaton.h, ProductAutomaton.cc and Remove ProductAutomaton.h, ProductAutomaton.cc and
SccIterator.h from lbtt_SOURCES. SccIterator.h from lbtt_SOURCES.
* src/Graph.h.in (Graph::EdgeContainerType, Graph::Path): New * src/Graph.h.in (Graph::EdgeContainerType, Graph::Path): New
type definitions. type definitions.
(Graph::PathElement): New class. (Graph::PathElement): New class.
@ -337,7 +346,7 @@
(printAcceptingCycle): Update parameter list and documentation. (printAcceptingCycle): Update parameter list and documentation.
Display all relevant information about an accepting execution Display all relevant information about an accepting execution
of a Büchi automaton. of a Büchi automaton.
2004-05-18 Heikki Tauriainen <heikki.tauriainen@hut.fi> 2004-05-18 Heikki Tauriainen <heikki.tauriainen@hut.fi>
* configure.ac (YACC): Do not add `-d' here. * configure.ac (YACC): Do not add `-d' here.
@ -365,7 +374,7 @@
* src/NeverClaim-lex.ll: Add %option nounput to avoid a * src/NeverClaim-lex.ll: Add %option nounput to avoid a
compiler warning. compiler warning.
* src/ExternalTranslator.h: Include the TempFsysName.h header. * src/ExternalTranslator.h: Include the TempFsysName.h header.
(ExternalTranslator::TempFileObject): Remove. (ExternalTranslator::TempFileObject): Remove.
(ExternalTranslator::registerTempFileObject): Change (ExternalTranslator::registerTempFileObject): Change
@ -475,7 +484,7 @@
command line option. command line option.
(printCommandHelp): Update the description of the `formula' (printCommandHelp): Update the description of the `formula'
command. command.
* src/UserCommandReader.cc (executeUserCommands): Accept one * src/UserCommandReader.cc (executeUserCommands): Accept one
optional parameter for the `formula' command. Pass the input optional parameter for the `formula' command. Pass the input
tokens as an additional parameter in the printFormula call. tokens as an additional parameter in the printFormula call.
@ -505,7 +514,7 @@
* src/TempFsysName.h, src/TempFsysName.cc New files. * src/TempFsysName.h, src/TempFsysName.cc New files.
* src/Makefile.am: Add TempFsysName.h and TempFsysName.cc to * src/Makefile.am: Add TempFsysName.h and TempFsysName.cc to
lbtt_SOURCES. lbtt_SOURCES.
* src/TestRoundInfo.h: Include the TempFsysName.h header. * src/TestRoundInfo.h: Include the TempFsysName.h header.
(TestRoundInfo::formula_file_name[]) (TestRoundInfo::formula_file_name[])
(TestRoundInfo::automaton_file_name) (TestRoundInfo::automaton_file_name)
@ -513,7 +522,7 @@
TempFsysName*. TempFsysName*.
(TestRoundInfo::TestRoundInfo): Initialize temporary file (TestRoundInfo::TestRoundInfo): Initialize temporary file
name pointers to 0. name pointers to 0.
* src/main.cc: Include the TempFsysName.h header. * src/main.cc: Include the TempFsysName.h header.
(allocateTempFilenames, deallocateTempFilenames): New functions. (allocateTempFilenames, deallocateTempFilenames): New functions.
(abortHandler): New signal handler. (abortHandler): New signal handler.
@ -858,7 +867,7 @@
after colon in output. Return 3 if an unexpected exception after colon in output. Return 3 if an unexpected exception
occurred. In this case print an additional newline before the occurred. In this case print an additional newline before the
error message. error message.
2004-02-19 Heikki Tauriainen <heikki.tauriainen@hut.fi> 2004-02-19 Heikki Tauriainen <heikki.tauriainen@hut.fi>
* src/StringUtil.h: Include the IntervalList.h header. * src/StringUtil.h: Include the IntervalList.h header.
@ -926,7 +935,7 @@
Reformat the automata file format section to avoid overfull lines Reformat the automata file format section to avoid overfull lines
in dvi generation. in dvi generation.
Fix description of the Algorithm block used with lbtt-translate. Fix description of the Algorithm block used with lbtt-translate.
* doc/testprocedure.txt, doc/intersectioncheck.txt: Add initial * doc/testprocedure.txt, doc/intersectioncheck.txt: Add initial
newlines. newlines.

4
lbtt/src/Ltl-parse.yy
View file

@ -1,5 +1,5 @@
/* /*
* Copyright (C) 2004, 2005 * Copyright (C) 2004, 2005, 2008
* Heikki Tauriainen <Heikki.Tauriainen@tkk.fi> * Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
* *
* This program is free software; you can redistribute it and/or * 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 static inline size_t matchCharactersFromStream
(istream& stream, char* chars) (istream& stream, const char* chars)
{ {
size_t num_matched; size_t num_matched;
for (num_matched = 0; *chars != '\0' && stream.peek() == *chars; ++chars) for (num_matched = 0; *chars != '\0' && stream.peek() == *chars; ++chars)

14
lbtt/src/NeverClaim-parse.yy
View file

@ -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 <Heikki.Tauriainen@tkk.fi> * Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
* *
* This program is free software; you can redistribute it and/or * 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. * 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 formula: NC_PROPOSITION
{ {
$$ = $1; $$ = $1;
} }
| NC_TRUE | NC_TRUE
{ {
$$ = $1; $$ = $1;
} }
| NC_FALSE | NC_FALSE
{ {
@ -290,7 +290,7 @@ int parseNeverClaim(FILE* stream, NeverClaimAutomaton& a)
* a -- A reference to a NeverClaimAutomaton object in * a -- A reference to a NeverClaimAutomaton object in
* which the results should be stored. * which the results should be stored.
* *
* Returns: * Returns:
* *
* ------------------------------------------------------------------------- */ * ------------------------------------------------------------------------- */
{ {

13
lbtt/src/main.cc
View file

@ -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 <Heikki.Tauriainen@tkk.fi> * Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or
@ -21,6 +21,7 @@
#include <csignal> #include <csignal>
#include <cstdlib> #include <cstdlib>
#include <ctime> #include <ctime>
#include <climits>
#ifdef HAVE_SYS_TYPES_H #ifdef HAVE_SYS_TYPES_H
#include <sys/types.h> #include <sys/types.h>
#endif /* HAVE_SYS_TYPES_H */ #endif /* HAVE_SYS_TYPES_H */
@ -366,7 +367,7 @@ bool testLoop()
round_info.error = false; round_info.error = false;
round_info.skip round_info.skip
= (round_info.current_round < round_info.next_round_to_run); = (round_info.current_round < round_info.next_round_to_run);
if (!round_info.skip) if (!round_info.skip)
printText(string("Round ") + toString(round_info.current_round) printText(string("Round ") + toString(round_info.current_round)
+ " of " + toString(global_options.number_of_rounds) + "\n\n", + " of " + toString(global_options.number_of_rounds) + "\n\n",
@ -395,7 +396,7 @@ bool testLoop()
configuration.global_options.statespace_random_seed configuration.global_options.statespace_random_seed
= LRAND(0, RAND_MAX); = LRAND(0, RAND_MAX);
#endif /* HAVE_RAND48 */ #endif /* HAVE_RAND48 */
if (global_options.statespace_change_interval == 0) if (global_options.statespace_change_interval == 0)
round_info.next_round_to_change_statespace round_info.next_round_to_change_statespace
= global_options.number_of_rounds + 1; = global_options.number_of_rounds + 1;
@ -433,7 +434,7 @@ bool testLoop()
*/ */
round_info.fresh_formula round_info.fresh_formula
= (round_info.next_round_to_change_formula = (round_info.next_round_to_change_formula
== round_info.current_round); == round_info.current_round);
if (round_info.fresh_formula) if (round_info.fresh_formula)
@ -742,7 +743,7 @@ bool testLoop()
int main(int argc, char* argv[]) int main(int argc, char* argv[])
{ {
try try
{ {
configuration.read(argc, argv); configuration.read(argc, argv);
} }
@ -791,7 +792,7 @@ int main(int argc, char* argv[])
using_history(); using_history();
#endif /* HAVE_READLINE */ #endif /* HAVE_READLINE */
try try
{ {
allocateTempFilenames(); allocateTempFilenames();
if (!testLoop()) if (!testLoop())