From 37934548643a054a96d618f2b44c2d7063f72b93 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 27 Jun 2012 18:07:42 +0200 Subject: [PATCH] [lbtt] Fix issues reported by Clang++ 3.1. * src/Graph.h.in (PathElement::hasEdge): Check the correct pointer, not the address of some member function. * src/BuchiAutomaton.cc, src/Configuration.cc, src/TestOperations.cc, src/TestOperations.h: Recode these files in utf-8. --- lbtt/ChangeLog | 10 +++++++++ lbtt/NEWS | 2 +- lbtt/src/BuchiAutomaton.cc | 23 +++++++++---------- lbtt/src/Configuration.cc | 7 +++--- lbtt/src/Graph.h.in | 36 +++++++++++++++--------------- lbtt/src/TestOperations.cc | 45 +++++++++++++++++++------------------- lbtt/src/TestOperations.h | 15 +++++++------ 7 files changed, 76 insertions(+), 62 deletions(-) diff --git a/lbtt/ChangeLog b/lbtt/ChangeLog index ca669bdb5..edd44909f 100644 --- a/lbtt/ChangeLog +++ b/lbtt/ChangeLog @@ -1,3 +1,13 @@ +2012-06-27 Alexandre Duret-Lutz + + Fix issues reported by Clang++ 3.1. + + * src/Graph.h.in (PathElement::hasEdge): Check the correct + pointer, not the address of some member function. + * src/BuchiAutomaton.cc, src/Configuration.cc, + src/TestOperations.cc, src/TestOperations.hh: Recode these files in + utf-8. + 2012-06-19 Alexandre Duret-Lutz Adjust parsers to accommodate old and new versions of Automake. diff --git a/lbtt/NEWS b/lbtt/NEWS index 4ea8422ee..1a707cec7 100644 --- a/lbtt/NEWS +++ b/lbtt/NEWS @@ -22,7 +22,7 @@ Copyright (C) 2008 Heikki Tauriainen Version 1.2.1a * Fix compilation with newer versions of Bison. -* Fix compilation on Intel's icpc, and with recent version of G++. +* Fix compilation on Intel's icpc, and recent version of G++ and Clang++. * Fix compilation with newer versions of Automake. * Fix construction of manual ("make dvi" and "make pdf") for recent version of texinfo. diff --git a/lbtt/src/BuchiAutomaton.cc b/lbtt/src/BuchiAutomaton.cc index 7a77dd383..ab5d206ed 100644 --- a/lbtt/src/BuchiAutomaton.cc +++ b/lbtt/src/BuchiAutomaton.cc @@ -1,4 +1,5 @@ -/* +/* -*- coding: utf-8 -*- + * * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005 * Heikki Tauriainen * @@ -199,7 +200,7 @@ void BuchiAutomaton::read(istream& input_stream) /* ---------------------------------------------------------------------------- * * Description: Reads an automaton description (which may represent a - * generalized Büchi automaton) from a stream and stores it + * generalized Büchi automaton) from a stream and stores it * into the automaton object. * * Argument: input_stream -- A reference to an input stream. @@ -216,7 +217,7 @@ void BuchiAutomaton::read(istream& input_stream) try { - /* Read the number of states in the generalized Büchi automaton. */ + /* Read the number of states in the generalized Büchi automaton. */ einput_stream >> number_of_states; @@ -275,8 +276,8 @@ void BuchiAutomaton::read(istream& input_stream) BitArray acc_sets(number_of_acceptance_sets); /* - * Allocate space for the regular Büchi automaton that will be constructed - * from the generalized Büchi automaton. + * Allocate space for the regular Büchi automaton that will be constructed + * from the generalized Büchi automaton. */ nodes.reserve(number_of_states); @@ -352,7 +353,7 @@ void BuchiAutomaton::read(istream& input_stream) if (state_mapping.second >= number_of_states) throw AutomatonParseException("number of different state " "identifiers does not match the size" - " of the Büchi automaton"); + " of the Büchi automaton"); current_state = state_mapping.second; state_mapping.second++; @@ -440,7 +441,7 @@ void BuchiAutomaton::read(istream& input_stream) if (state_mapping.second >= number_of_states) throw AutomatonParseException("number of different state " "identifiers does not match the size" - " of the Büchi automaton"); + " of the Büchi automaton"); neighbor_state = state_mapping.second; state_mapping.second++; @@ -548,7 +549,7 @@ void BuchiAutomaton::print if (nodes.empty()) { if (fmt == NORMAL) - estream << string(indent, ' ') + "The Büchi automaton is empty.\n"; + estream << string(indent, ' ') + "The Büchi automaton is empty.\n"; } else { @@ -558,7 +559,7 @@ void BuchiAutomaton::print pair reachable_part_statistics = subgraphStats(initial_state); - estream << string(indent, ' ') + "The Büchi automaton consists of\n" + estream << string(indent, ' ') + "The Büchi automaton consists of\n" + string(indent + 4, ' ') << statistics.first << " states and\n" + string(indent + 4, ' ') @@ -734,7 +735,7 @@ void BuchiAutomaton::BuchiTransition::print /* ---------------------------------------------------------------------------- * * Description: Writes information about a transition between two states of - * a Büchi automaton. + * a Büchi automaton. * * Arguments: stream -- A reference to an output * stream. @@ -820,7 +821,7 @@ void BuchiAutomaton::BuchiState::print const unsigned long int number_of_acceptance_sets) const /* ---------------------------------------------------------------------------- * - * Description: Writes information about a state of a Büchi automaton. + * Description: Writes information about a state of a Büchi automaton. * * Arguments: stream -- A reference to an output * stream. diff --git a/lbtt/src/Configuration.cc b/lbtt/src/Configuration.cc index 8a7092781..b01687f3f 100644 --- a/lbtt/src/Configuration.cc +++ b/lbtt/src/Configuration.cc @@ -1,4 +1,5 @@ -/* +/* -*- coding: utf-8 -*- + * * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005 * Heikki Tauriainen * @@ -1048,7 +1049,7 @@ void Configuration::print(ostream& stream, int indent) const "Model checking result consistency check\n"; if (global_options.do_intr_test) estream << string(indent + 4, ' ') + - "Büchi automata intersection emptiness check\n"; + "Büchi automata intersection emptiness check\n"; } else estream << "All automata correctness tests disabled.\n"; @@ -1396,7 +1397,7 @@ void Configuration::showCommandLineHelp(const char* program_name) "(`always', `onerror', \n" " `never', `onbreak')\n" " --intersectiontest[=VALUE], --nointersectiontest\n" - " Enable or disable the Büchi " + " Enable or disable the Büchi " "automata\n" " intersection emptiness test\n" " --localmodelcheck Use local model checking in tests" diff --git a/lbtt/src/Graph.h.in b/lbtt/src/Graph.h.in index ec484f01f..01028c3a6 100644 --- a/lbtt/src/Graph.h.in +++ b/lbtt/src/Graph.h.in @@ -43,7 +43,7 @@ using namespace std; namespace Graph { -/* +/* * Output formats for printing a graph, its edges or nodes. All output * functions for these objects will accept a parameter `fmt' which can be * either of these constants (and defaults to NORMAL). @@ -53,7 +53,7 @@ namespace Graph * for generating input files for the tool. */ -enum GraphOutputFormat {NORMAL, DOT}; +enum GraphOutputFormat {NORMAL, DOT}; @@ -95,7 +95,7 @@ class ProductAutomaton; * interface: * * Default constructor which can be called without arguments. - * + * * EdgeContainer::size_type * Data type able to represent the maximum number of elements * that can be stored in the container. @@ -110,8 +110,8 @@ class ProductAutomaton; * void clear() * Makes the container empty. * - * EdgeContainer::iterator - * EdgeContainer::const_iterator + * EdgeContainer::iterator + * EdgeContainer::const_iterator * Input iterators that can be used to traverse through the * elements of the container. The iterators must support * increment and dereferencing operations. However, support for @@ -278,7 +278,7 @@ public: stats() const; /* nodes and edges in * the graph. */ - + virtual pair /* Returns the number of */ subgraphStats(const size_type index) const; /* nodes and edges in a * connected subgraph of @@ -335,7 +335,7 @@ public: virtual ~Edge(); /* Destructor. */ /* default assignment operator */ - + size_type targetNode() const; /* Returns the index of */ /* the target node of * the directed edge. @@ -364,7 +364,7 @@ protected: * for sorting Edges in an * STL container. */ - + private: size_type target_node; /* Identifier of the edge's * target node. @@ -388,9 +388,9 @@ public: Node(const Node& node); /* Copy constructor. */ virtual ~Node(); /* Destructor. */ - + Node& operator=(const Node& node); /* Assignment operator. */ - + const EdgeContainer& edges() const; /* Returns the container of * edges beginning at the * node. @@ -481,9 +481,9 @@ private: class NodeIndexException : public Exception { -public: +public: NodeIndexException(); /* Default constructor. */ - + /* default copy constructor */ ~NodeIndexException() throw(); /* Destructor. */ @@ -1233,7 +1233,7 @@ inline ostream& operator<< * * Arguments: stream -- A reference to an output stream. * edge -- A reference to a constant edge to be printed. - * + * * Returns: A reference to the output stream. * * ------------------------------------------------------------------------- */ @@ -1371,11 +1371,11 @@ inline const EdgeContainer& Graph::Node::edges() const * * Arguments: None. * - * Returns: A reference to the constant container of pointers to the + * Returns: A reference to the constant container of pointers to the * edges starting from the node. * * ------------------------------------------------------------------------- */ -{ +{ return outgoing_edges; } @@ -1412,7 +1412,7 @@ template Graph::Node::Node(const Node& node) /* ---------------------------------------------------------------------------- * - * Description: Copy constructor for Graph::Node. Initializes + * Description: Copy constructor for Graph::Node. Initializes * a copy of a Node. * * Argument: node -- A reference to a constant node to be copied. @@ -1616,7 +1616,7 @@ inline bool Graph::PathElement::hasEdge() const * * ------------------------------------------------------------------------- */ { - return (edge != 0); + return edge_pointer != 0; } /* ========================================================================= */ @@ -1871,7 +1871,7 @@ EdgeSlist::find(const Graph::Edge* edge) const * * Returns: A slist::Edge*>::const_iterator * pointing to the edge in the list or - * slist::Edge*>::end() if the edge + * slist::Edge*>::end() if the edge * is not found in the list. * * ------------------------------------------------------------------------- */ diff --git a/lbtt/src/TestOperations.cc b/lbtt/src/TestOperations.cc index a2c461d53..c20277c68 100644 --- a/lbtt/src/TestOperations.cc +++ b/lbtt/src/TestOperations.cc @@ -1,4 +1,5 @@ -/* +/* -*- coding: utf-8 -*- + * * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005 * Heikki Tauriainen * @@ -830,12 +831,12 @@ void generateBuchiAutomaton * * Description: Constructs a BuchiAutomaton by invoking an external program * that will perform the conversion of a LTL formula (stored - * into a file) into a Büchi automaton. + * into a file) into a Büchi automaton. * * Arguments: f -- Indicates the formula to be converted into * an automaton. 0 corresponds to the positive * and 1 to the negated formula. - * algorithm_id -- Identifier of the LTL-to-Büchi translator + * algorithm_id -- Identifier of the LTL-to-Büchi translator * to use. * * Returns: Nothing. The result is stored in @@ -850,10 +851,10 @@ void generateBuchiAutomaton = test_results[algorithm_id].automaton_stats[f]; if (automaton_stats.buchiAutomatonComputed()) - printText("Büchi automaton (cached):\n", 3, 8); + printText("Büchi automaton (cached):\n", 3, 8); else { - printText("Büchi automaton:\n", 3, 8); + printText("Büchi automaton:\n", 3, 8); const Configuration::AlgorithmInformation& algorithm = configuration.algorithms[algorithm_id]; @@ -910,7 +911,7 @@ void generateBuchiAutomaton /* Execute the external program. */ if (!printText("", 5, 10)) - printText("", 4, 10); + printText("", 4, 10); int error_number; int error_pipe[2]; /* used for communicating errors in exec() */ @@ -1201,7 +1202,7 @@ void generateBuchiAutomaton printText("\n\n", 1); if (round_info.transcript_file.is_open()) - writeToTranscript("User break while generating Büchi automaton (" + writeToTranscript("User break while generating Büchi automaton (" + configuration.algorithmString(algorithm_id) + ", " + (f == 0 ? "posi" : "nega") + "tive formula)\n"); @@ -1210,7 +1211,7 @@ void generateBuchiAutomaton } if (round_info.transcript_file.is_open()) - writeToTranscript("Büchi automaton generation failed (" + writeToTranscript("Büchi automaton generation failed (" + configuration.algorithmString(algorithm_id) + ", " + (f == 0 ? "posi" : "nega") @@ -1308,7 +1309,7 @@ void generateBuchiAutomaton if (translator_process != 0) /* fatal error, lbtt should be terminated */ throw Exception - ("fatal internal error while generating Büchi automaton"); + ("fatal internal error while generating Büchi automaton"); throw BuchiAutomatonGenerationException(); } @@ -1342,7 +1343,7 @@ void generateBuchiAutomaton = automaton_stats.buchi_automaton->isDeterministic(); /* - * Update Büchi automaton statistics for the given algorithm. + * Update Büchi automaton statistics for the given algorithm. */ final_statistics[algorithm_id].total_number_of_buchi_states[f] @@ -1378,14 +1379,14 @@ void performEmptinessCheck * * Description: Performs the emptiness check on a ProductAutomaton, i.e., * finds the states of the original state space from which an - * accepting cycle of the Büchi automaton can be reached. + * accepting cycle of the Büchi automaton can be reached. * * Arguments: f -- Indicates the formula originally used for * constructing the given product automaton. * 0 corresponds to the automaton obtained * from the positive, 1 to the one obtained * from the negated formula. - * algorithm_id -- Identifier of the LTL-to-Büchi translator + * algorithm_id -- Identifier of the LTL-to-Büchi translator * originally used for generating the given * product automaton. * @@ -1503,7 +1504,7 @@ void performConsistencyCheck /* ---------------------------------------------------------------------------- * * Description: Checks the model checking results for consistency for a - * particular LTL-to-Büchi conversion algorithm implementation, + * particular LTL-to-Büchi conversion algorithm implementation, * i.e., verifies that the model checking results for a formula * and its negation are not contradictory. * @@ -1576,7 +1577,7 @@ void compareResults() /* ---------------------------------------------------------------------------- * * Description: Compares the model checking results obtained using different - * LTL->Büchi conversion algorithm implementations with each + * LTL->Büchi conversion algorithm implementations with each * other. * * Arguments: None. @@ -1685,7 +1686,7 @@ void compareResults() void performBuchiIntersectionCheck() /* ---------------------------------------------------------------------------- * - * Description: Tests the intersection of the Büchi automata constructed for + * Description: Tests the intersection of the Büchi automata constructed for * the formula and its negation for emptiness. * * Arguments: None. @@ -1694,10 +1695,10 @@ void performBuchiIntersectionCheck() * * ------------------------------------------------------------------------- */ { - if (printText("Büchi automata intersection emptiness check:\n", 3, 4)) - printText("\n", 4, 6); + if (printText("Büchi automata intersection emptiness check:\n", 3, 4)) + printText("\n", 4, 6); else - printText("Checking Büchi automata intersections for emptiness", 2, 4); + printText("Checking Büchi automata intersections for emptiness", 2, 4); bool result = true; @@ -1726,7 +1727,7 @@ void performBuchiIntersectionCheck() 8); /* - * Compute the intersection of two Büchi automata constructed for + * Compute the intersection of two Büchi automata constructed for * the positive and the negative formula, respectively. */ @@ -1802,7 +1803,7 @@ void performBuchiIntersectionCheck() if (round_info.transcript_file.is_open()) { - writeToTranscript("User break during Büchi automata intersection " + writeToTranscript("User break during Büchi automata intersection " "emptiness check"); round_info.transcript_file << string(8, ' ') + "(+) " + configuration.algorithmString(alg_1) @@ -1850,7 +1851,7 @@ void performBuchiIntersectionCheck() if (round_info.transcript_file.is_open()) { - writeToTranscript("Out of memory during Büchi automata " + writeToTranscript("Out of memory during Büchi automata " "intersection emptiness check"); round_info.transcript_file << string(8, ' ') + "(+) " + configuration.algorithmString(alg_1) @@ -1871,7 +1872,7 @@ void performBuchiIntersectionCheck() if (round_info.transcript_file.is_open()) { - writeToTranscript("Büchi automata intersection emptiness check failed"); + writeToTranscript("Büchi automata intersection emptiness check failed"); printBuchiIntersectionCheckStats (round_info.transcript_file, 8, algorithms); round_info.transcript_file << '\n'; diff --git a/lbtt/src/TestOperations.h b/lbtt/src/TestOperations.h index 74b9cdfd1..a7a6ed0bc 100644 --- a/lbtt/src/TestOperations.h +++ b/lbtt/src/TestOperations.h @@ -1,4 +1,5 @@ -/* +/* -*- coding: utf-8 -*- + * * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005 * Heikki Tauriainen * @@ -93,11 +94,11 @@ void verifyFormulaOnPath(); /* Evaluates the LTL void writeFormulaeToFiles(); /* Writes LTL formulas */ /* into a file. */ -void generateBuchiAutomaton /* Generates a Büchi */ +void generateBuchiAutomaton /* Generates a Büchi */ (int f, /* automaton from a LTL */ vector /* formula stored in a */ ::size_type /* given file, using a */ - algorithm_id); /* given LTL-to-Büchi + algorithm_id); /* given LTL-to-Büchi * translation algorithm * for the conversion. */ @@ -118,7 +119,7 @@ void performConsistencyCheck /* Performs a */ void compareResults(); /* Compares the model * checking results * obtained using some - * LTL-to-Büchi conversion + * LTL-to-Büchi conversion * algorithm with the * results given by the * other algorithms. @@ -126,7 +127,7 @@ void compareResults(); /* Compares the model void performBuchiIntersectionCheck(); /* Performs pairwise * emptiness checks on the - * Büchi automata + * Büchi automata * constructed by the * different algorithms * from a formula and its @@ -179,7 +180,7 @@ public: /****************************************************************************** * - * A class for reporting Büchi automaton generation errors. + * A class for reporting Büchi automaton generation errors. * *****************************************************************************/ @@ -361,7 +362,7 @@ FormulaGenerationException::operator=(const FormulaGenerationException& e) /* ========================================================================= */ inline BuchiAutomatonGenerationException::BuchiAutomatonGenerationException() : - Exception("Büchi automaton generation failed") + Exception("Büchi automaton generation failed") /* ---------------------------------------------------------------------------- * * Description: Constructor for class BuchiAutomatonGenerationException.