Style: use NOLINTNEXTLINE to avoid cpplint errors on long links

Author: romainbrenguier

src/solvers/refinement/string_constraint_generator_indexof.cpp

@@ -244,6 +244,7 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of_string(
 /// Index of the first occurence of a target inside the string
 ///
 /// If the target is a character:
+// NOLINTNEXTLINE
 /// \copybrief add_axioms_for_index_of(const array_string_exprt&,const exprt&,const exprt&)
 /// \link
 /// add_axioms_for_index_of(const array_string_exprt&,const exprt&,const exprt&)
@@ -357,9 +358,10 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of(
 /// Index of the last occurence of a target inside the string
 ///
 /// If the target is a character:
+// NOLINTNEXTLINE
 /// \copybrief add_axioms_for_last_index_of(const array_string_exprt&,const exprt&,const exprt&)
-/// \link
-/// add_axioms_for_last_index_of(const array_string_exprt&,const exprt&,const exprt&)
+// NOLINTNEXTLINE
+/// \link add_axioms_for_last_index_of(const array_string_exprt&,const exprt&,const exprt&)
 ///   (More...) \endlink
 ///
 /// If the target is a refined_string:

src/solvers/refinement/string_constraint_generator_insert.cpp

@@ -56,8 +56,8 @@ exprt string_constraint_generatort::add_axioms_for_insert(
 /// \copybrief string_constraint_generatort::add_axioms_for_insert(
 /// const array_string_exprt &, const array_string_exprt &,
 /// const array_string_exprt &, const exprt &)
-/// \link
-/// add_axioms_for_insert(const array_string_exprt&,const array_string_exprt&,const array_string_exprt&,const exprt&)
+// NOLINTNEXTLINE
+/// \link add_axioms_for_insert(const array_string_exprt&,const array_string_exprt&,const array_string_exprt&,const exprt&)
 ///   (More...) \endlink
 ///
 /// If `start` and `end` arguments are given then `substring(s2, start, end)`

src/solvers/refinement/string_constraint_generator_testing.cpp

@@ -70,6 +70,7 @@ exprt string_constraint_generatort::add_axioms_for_is_prefix(
 /// Add axioms ensuring the return value is true when the string starts with the
 /// given target.
 /// These axioms are detailed here:
+// NOLINTNEXTLINE
 /// string_constraint_generatort::add_axioms_for_is_prefix(const array_string_exprt &prefix, const array_string_exprt &str, const exprt &offset)
 /// \todo The primitive should be renamed to `starts_with`.
 /// \todo Get rid of the boolean flag.

src/solvers/refinement/string_constraint_generator_transformation.cpp

@@ -76,6 +76,7 @@ exprt string_constraint_generatort::add_axioms_for_set_length(
 ///   const array_string_exprt &str,
 ///   const exprt &start,
 ///   const exprt &end)
+// NOLINTNEXTLINE
 /// \link string_constraint_generatort::add_axioms_for_substring(const array_string_exprt &res, const array_string_exprt &str, const exprt &start, const exprt &end)
 ///   (More...) \endlink
 /// \warning The specification may not be correct for the case where the string
@@ -367,8 +368,9 @@ exprt string_constraint_generatort::add_axioms_for_to_upper_case(
 
 /// Conversion of a string to upper case
 ///
-/// \copybrief string_constraint_generatort::add_axioms_for_to_upper_case(
-/// const array_string_exprt &res, const array_string_exprt &str)
+// NOLINTNEXTLINE
+/// \copybrief string_constraint_generatort::add_axioms_for_to_upper_case(const array_string_exprt&, const array_string_exprt&)
+// NOLINTNEXTLINE
 /// \link string_constraint_generatort::add_axioms_for_to_upper_case(const array_string_exprt &res, const array_string_exprt &str)
 ///   (More...) \endlink
 /// \param f: function application with arguments integer `|res|`, character
@@ -551,7 +553,9 @@ exprt string_constraint_generatort::add_axioms_for_delete(
 
 /// Remove a portion of a string
 ///
+// NOLINTNEXTLINE
 /// \copybrief string_constraint_generatort::add_axioms_for_delete(const array_string_exprt &res, const array_string_exprt &str, const exprt &start, const exprt &end)
+// NOLINTNEXTLINE
 /// \link string_constraint_generatort::add_axioms_for_delete(const array_string_exprt &res, const array_string_exprt &str, const exprt &start, const exprt &end)
 ///   (More...) \endlink
 /// \param f: function application with arguments integer `|res|`, character

src/solvers/refinement/string_constraint_generator_valueof.cpp

@@ -269,6 +269,7 @@ exprt string_constraint_generatort::add_axioms_from_int_hex(
 ///
 /// \copybrief  string_constraint_generatort::add_axioms_from_char(
 ///   const array_string_exprt &res, const exprt &c)
+// NOLINTNEXTLINE
 /// \link string_constraint_generatort::add_axioms_from_char(const array_string_exprt &res, const exprt &c)
 ///    (More...) \endlink
 /// \param f: function application with arguments integer `|res|`, character

src/solvers/refinement/string_refinement.cpp

@@ -215,6 +215,7 @@ static void display_index_set(
 ///     the index set of `str` we find `y` such that `f(y)=val` and
 ///     add lemma `P(y)`.
 ///     (See
+// NOLINTNEXTLINE
 ///     `instantiate(messaget::mstreamt&,const string_constraintt&,const exprt &,const exprt&)`
 ///      for details)
 ///   * For formulas of the form
@@ -467,12 +468,15 @@ void output_equations(
 /// Pointer symbols which are set to be equal by constraints, are replaced by
 /// an single symbol in the solver. The `symbol_solvert` object used for this
 /// substitution is constructed by
+// NOLINTNEXTLINE
 /// `generate_symbol_resolution_from_equations(const std::vector<equal_exprt>&,const namespacet&,messaget::mstreamt&)`.
 /// All these symbols are then replaced using
+// NOLINTNEXTLINE
 /// `replace_symbols_in_equations(const union_find_replacet &, std::vector<equal_exprt> &)`.
 ///
 /// ## Conversion to first order formulas:
 /// Each string primitive is converted to a list of first order formulas by the
+// NOLINTNEXTLINE
 /// function `substitute_function_applications_in_equations(std::vector<equal_exprt>&,string_constraint_generatort&)`.
 /// These formulas should be unquantified or be either a `string_constraintt`
 /// or a `string_not_contains_constraintt`.