From 4b4575eca3b111058b4cbf3a1bd80fbc7c809990 Mon Sep 17 00:00:00 2001 From: John Nonweiler Date: Tue, 2 Oct 2018 14:50:19 +0100 Subject: [PATCH 1/6] Add missing newlines after doxygen \file tags --- src/util/expr_iterator.h | 3 ++- src/util/irep_ids.h | 3 ++- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/src/util/expr_iterator.h b/src/util/expr_iterator.h index 132a1784d7b..05c63b24481 100644 --- a/src/util/expr_iterator.h +++ b/src/util/expr_iterator.h @@ -19,7 +19,8 @@ // Forward declarations - table of contents -/// \file Forward depth-first search iterators +/// \file +/// Forward depth-first search iterators /// These iterators' copy operations are expensive, so use auto&, and avoid /// std::next(), std::prev() and post-increment iterator /// diff --git a/src/util/irep_ids.h b/src/util/irep_ids.h index 7d946bed305..b96ff929f25 100644 --- a/src/util/irep_ids.h +++ b/src/util/irep_ids.h @@ -22,7 +22,8 @@ Author: Reuben Thomas, reuben.thomas@me.com #include #endif -/// \file The irep_ids are generated using a technique called +/// \file +/// The irep_ids are generated using a technique called /// [X-macros](https://en.wikipedia.org/wiki/X_Macro). /// The ids are defined in the file irep_ids.def, using a pair of macros /// `IREP_ID_ONE` and `IREP_ID_TWO`. From 9bd9b53147a1e4cf30d0e1132e8b227822cac1a3 Mon Sep 17 00:00:00 2001 From: John Nonweiler Date: Fri, 5 Oct 2018 15:34:33 +0100 Subject: [PATCH 2/6] Correct parameter names in doxygen comments --- .../character_refine_preprocess.cpp | 42 +++++++++---------- .../java_bytecode_convert_class.cpp | 2 +- 2 files changed, 22 insertions(+), 22 deletions(-) diff --git a/jbmc/src/java_bytecode/character_refine_preprocess.cpp b/jbmc/src/java_bytecode/character_refine_preprocess.cpp index e0f230384f9..a09966c0b05 100644 --- a/jbmc/src/java_bytecode/character_refine_preprocess.cpp +++ b/jbmc/src/java_bytecode/character_refine_preprocess.cpp @@ -35,7 +35,7 @@ codet character_refine_preprocesst::convert_char_function( /// The returned expression is true when the first argument is in the interval /// defined by the lower and upper bounds (included) -/// \param arg: Expression we want to bound +/// \param chr: Expression we want to bound /// \param lower_bound: Integer lower bound /// \param upper_bound: Integer upper bound /// \return A Boolean expression @@ -65,7 +65,7 @@ exprt character_refine_preprocesst::in_list_expr( /// Determines the number of char values needed to represent the specified /// character (Unicode code point). -/// \param expr: An expression of type character +/// \param chr: An expression of type character /// \param type: A type for the output /// \return A integer expression of the given type exprt character_refine_preprocesst::expr_of_char_count( @@ -308,7 +308,7 @@ codet character_refine_preprocesst::convert_hash_code(conversion_inputt &target) /// Returns the leading surrogate (a high surrogate code unit) of the surrogate /// pair representing the specified supplementary character (Unicode code point) /// in the UTF-16 encoding. -/// \param expr: An expression of type character +/// \param chr: An expression of type character /// \param type: A type for the output /// \return An expression of the given type exprt character_refine_preprocesst::expr_of_high_surrogate( @@ -342,7 +342,7 @@ exprt character_refine_preprocesst::expr_of_is_ascii_lower_case( } /// Determines if the specified character is an ASCII uppercase character. -/// \param expr: An expression of type character +/// \param chr: An expression of type character /// \param type: A type for the output /// \return A Boolean expression exprt character_refine_preprocesst::expr_of_is_ascii_upper_case( @@ -356,7 +356,7 @@ exprt character_refine_preprocesst::expr_of_is_ascii_upper_case( /// TODO: for now this is only for ASCII characters, the /// following unicode categories are not yet considered: /// TITLECASE_LETTER MODIFIER_LETTER OTHER_LETTER LETTER_NUMBER -/// \param expr: An expression of type character +/// \param chr: An expression of type character /// \param type: A type for the output /// \return An expression of the given type exprt character_refine_preprocesst::expr_of_is_letter( @@ -374,7 +374,7 @@ exprt character_refine_preprocesst::expr_of_is_letter( /// TITLECASE_LETTER MODIFIER_LETTER OTHER_LETTER LETTER_NUMBER /// and contributory property Other_Alphabetic as defined by the /// Unicode Standard. -/// \param expr: An expression of type character +/// \param chr: An expression of type character /// \param type: A type for the output /// \return An expression of the given type exprt character_refine_preprocesst::expr_of_is_alphabetic( @@ -396,7 +396,7 @@ codet character_refine_preprocesst::convert_is_alphabetic( /// Determines whether the specified character (Unicode code point) is in the /// Basic Multilingual Plane (BMP). Such code points can be represented using a /// single char. -/// \param expr: An expression of type character +/// \param chr: An expression of type character /// \param type: A type for the output /// \return A Boolean expression exprt character_refine_preprocesst::expr_of_is_bmp_code_point( @@ -417,7 +417,7 @@ codet character_refine_preprocesst::convert_is_bmp_code_point( } /// Determines if a character is defined in Unicode. -/// \param expr: An expression of type character +/// \param chr: An expression of type character /// \param type: A type for the output /// \return An expression of the given type exprt character_refine_preprocesst::expr_of_is_defined( @@ -519,7 +519,7 @@ codet character_refine_preprocesst::convert_is_digit_int( /// Determines if the given char value is a Unicode high-surrogate code unit /// (also known as leading-surrogate code unit). -/// \param expr: An expression of type character +/// \param chr: An expression of type character /// \param type: A type for the output /// \return A Boolean expression exprt character_refine_preprocesst::expr_of_is_high_surrogate( @@ -543,7 +543,7 @@ codet character_refine_preprocesst::convert_is_high_surrogate( /// '\u001B' '\u007F' through '\u009F' /// /// TODO: For now, we ignore the FORMAT general category value -/// \param expr: An expression of type character +/// \param chr: An expression of type character /// \param type: A type for the output /// \return A Boolean expression exprt character_refine_preprocesst::expr_of_is_identifier_ignorable( @@ -770,7 +770,7 @@ codet character_refine_preprocesst::convert_is_low_surrogate( /// specification. /// /// TODO: For now only ASCII characters are considered -/// \param expr: An expression of type character +/// \param chr: An expression of type character /// \param type: A type for the output /// \return An expression of the given type exprt character_refine_preprocesst::expr_of_is_mirrored( @@ -812,7 +812,7 @@ codet character_refine_preprocesst::convert_is_space(conversion_inputt &target) /// Determines if the specified character is white space according to Unicode /// (SPACE_SEPARATOR, LINE_SEPARATOR, or PARAGRAPH_SEPARATOR) -/// \param expr: An expression of type character +/// \param chr: An expression of type character /// \param type: A type for the output /// \return A Boolean expression exprt character_refine_preprocesst::expr_of_is_space_char( @@ -846,7 +846,7 @@ codet character_refine_preprocesst::convert_is_space_char_int( /// Determines whether the specified character (Unicode code point) is in the /// supplementary character range. -/// \param expr: An expression of type character +/// \param chr: An expression of type character /// \param type: A type for the output /// \return A Boolean expression exprt character_refine_preprocesst::expr_of_is_supplementary_code_point( @@ -866,7 +866,7 @@ codet character_refine_preprocesst::convert_is_supplementary_code_point( } /// Determines if the given char value is a Unicode surrogate code unit. -/// \param expr: An expression of type character +/// \param chr: An expression of type character /// \param type: A type for the output /// \return A Boolean expression exprt character_refine_preprocesst::expr_of_is_surrogate( @@ -902,7 +902,7 @@ codet character_refine_preprocesst::convert_is_surrogate_pair( } /// Determines if the specified character is a titlecase character. -/// \param expr: An expression of type character +/// \param chr: An expression of type character /// \param type: A type for the output /// \return A Boolean expression exprt character_refine_preprocesst::expr_of_is_title_case( @@ -939,7 +939,7 @@ codet character_refine_preprocesst::convert_is_title_case_int( /// Determines if the specified character is in the LETTER_NUMBER category of /// Unicode -/// \param expr: An expression of type character +/// \param chr: An expression of type character /// \param type: A type for the output /// \return A Boolean expression exprt character_refine_preprocesst::expr_of_is_letter_number( @@ -966,7 +966,7 @@ exprt character_refine_preprocesst::expr_of_is_letter_number( /// /// TODO: For now we do not allow connecting punctuation, combining mark, /// non-spacing mark -/// \param expr: An expression of type character +/// \param chr: An expression of type character /// \param type: A type for the output /// \return A Boolean expression exprt character_refine_preprocesst::expr_of_is_unicode_identifier_part( @@ -1076,7 +1076,7 @@ codet character_refine_preprocesst::convert_is_valid_code_point( /// (SPACE_SEPARATOR, LINE_SEPARATOR, or PARAGRAPH_SEPARATOR) but is not also a /// non-breaking space ('\u00A0', '\u2007', '\u202F'). * it is one of these: /// U+0009 U+000A U+000B U+000C U+000D U+001C U+001D U+001E U+001F -/// \param expr: An expression of type character +/// \param chr: An expression of type character /// \param type: A type for the output /// \return A Boolean expression exprt character_refine_preprocesst::expr_of_is_whitespace( @@ -1115,7 +1115,7 @@ codet character_refine_preprocesst::convert_is_whitespace_int( /// Returns the trailing surrogate (a low surrogate code unit) of the surrogate /// pair representing the specified supplementary character (Unicode code point) /// in the UTF-16 encoding. -/// \param expr: An expression of type character +/// \param chr: An expression of type character /// \param type: A type for the output /// \return A integer expression of the given type exprt character_refine_preprocesst::expr_of_low_surrogate( @@ -1138,7 +1138,7 @@ codet character_refine_preprocesst::convert_low_surrogate( /// Returns the value obtained by reversing the order of the bytes in the /// specified char value. -/// \param expr: An expression of type character +/// \param chr: An expression of type character /// \param type: A type for the output /// \return A character expression of the given type exprt character_refine_preprocesst::expr_of_reverse_bytes( @@ -1164,7 +1164,7 @@ codet character_refine_preprocesst::convert_reverse_bytes( /// (Basic Multilingual Plane or Plane 0) value, the resulting char array has /// the same value as codePoint. If the specified code point is a supplementary /// code point, the resulting char array has the corresponding surrogate pair. -/// \param expr: An expression of type character +/// \param chr: An expression of type character /// \param type: A type for the output /// \return A character array expression of the given type exprt character_refine_preprocesst::expr_of_to_chars( diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp index 01a082c217e..3c39562e477 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp @@ -1074,7 +1074,7 @@ static void find_and_replace_parameters( /// Convert parsed annotations into the symbol table /// \param parsed_annotations: The parsed annotations to convert -/// \param annotations: The java_annotationt collection to populate +/// \param java_annotations: The java_annotationt collection to populate void convert_annotations( const java_bytecode_parse_treet::annotationst &parsed_annotations, std::vector &java_annotations) From f83ddd22074df2f71a59504394569a1af1409fed Mon Sep 17 00:00:00 2001 From: John Nonweiler Date: Fri, 5 Oct 2018 15:36:56 +0100 Subject: [PATCH 3/6] Escape \ and # symbols in doxygen docs --- .../character_refine_preprocess.cpp | 16 ++++++++-------- src/goto-instrument/wmm/goto2graph.cpp | 2 +- src/util/README.md | 2 +- 3 files changed, 10 insertions(+), 10 deletions(-) diff --git a/jbmc/src/java_bytecode/character_refine_preprocess.cpp b/jbmc/src/java_bytecode/character_refine_preprocess.cpp index a09966c0b05..b4ae9886c7a 100644 --- a/jbmc/src/java_bytecode/character_refine_preprocess.cpp +++ b/jbmc/src/java_bytecode/character_refine_preprocess.cpp @@ -475,11 +475,11 @@ codet character_refine_preprocesst::convert_is_defined_int( /// DECIMAL_DIGIT_NUMBER. /// /// TODO: for now we only support these ranges of digits: -/// '\u0030' through '\u0039', ISO-LATIN-1 digits ('0' through '9') -/// '\u0660' through '\u0669', Arabic-Indic digits -/// '\u06F0' through '\u06F9', Extended Arabic-Indic digits -/// '\u0966' through '\u096F', Devanagari digits -/// '\uFF10' through '\uFF19', Fullwidth digits +/// '\\u0030' through '\\u0039', ISO-LATIN-1 digits ('0' through '9') +/// '\\u0660' through '\\u0669', Arabic-Indic digits +/// '\\u06F0' through '\\u06F9', Extended Arabic-Indic digits +/// '\\u0966' through '\\u096F', Devanagari digits +/// '\\uFF10' through '\\uFF19', Fullwidth digits /// Many other character ranges contain digits as well. /// \param chr: An expression of type character /// \param type: A type for the output @@ -539,8 +539,8 @@ codet character_refine_preprocesst::convert_is_high_surrogate( } /// Determines if the character is one of ignorable in a Java identifier, that -/// is, it is in one of these ranges: '\u0000' through '\u0008' '\u000E' through -/// '\u001B' '\u007F' through '\u009F' +/// is, it is in one of these ranges: '\\u0000' through '\\u0008' '\\u000E' +/// through '\\u001B' '\\u007F' through '\\u009F' /// /// TODO: For now, we ignore the FORMAT general category value /// \param chr: An expression of type character @@ -1074,7 +1074,7 @@ codet character_refine_preprocesst::convert_is_valid_code_point( /// Determines if the specified character is white space according to Java. It /// is the case when it one of the following: * a Unicode space character /// (SPACE_SEPARATOR, LINE_SEPARATOR, or PARAGRAPH_SEPARATOR) but is not also a -/// non-breaking space ('\u00A0', '\u2007', '\u202F'). * it is one of these: +/// non-breaking space ('\\u00A0', '\\u2007', '\\u202F'). * it is one of these: /// U+0009 U+000A U+000B U+000C U+000D U+001C U+001D U+001E U+001F /// \param chr: An expression of type character /// \param type: A type for the output diff --git a/src/goto-instrument/wmm/goto2graph.cpp b/src/goto-instrument/wmm/goto2graph.cpp index 9ced322139a..bd9e179ea42 100644 --- a/src/goto-instrument/wmm/goto2graph.cpp +++ b/src/goto-instrument/wmm/goto2graph.cpp @@ -1517,7 +1517,7 @@ void instrumentert::print_outputs(memory_modelt model, bool hide_internals) table.close(); } -/// Note: can be distributed (#define DISTRIBUTED) +/// Note: can be distributed (\#define DISTRIBUTED) #if 1 // #ifdef _WIN32 void instrumentert::collect_cycles_by_SCCs(memory_modelt model) diff --git a/src/util/README.md b/src/util/README.md index 1b444ca5643..b0f6d321769 100644 --- a/src/util/README.md +++ b/src/util/README.md @@ -90,7 +90,7 @@ is initially populated from `irep_ids.def`, so for example the fourth entry in `irep_ids.def` is `“IREP_ID_ONE(type)”`, so the string “type” has index 3. You can refer to this \ref irep_idt as `ID_type`. The other kind of line you see is `“IREP_ID_TWO(C_source_location, #source_location)”`, which means the -\ref irep_idt for the string “#source_location” can be referred to as +\ref irep_idt for the string “\#source_location” can be referred to as `ID_C_source_location`. The “C” is for comment, meaning that it should be stored in the [comments](\ref irept::dt::comments). Any strings that need to be stored as [irep_idt](\ref irep_idt)s which aren't in `irep_ids.def` From 6fe94f1bb1e8a4bc5da5bc291efd260f1bcceeaf Mon Sep 17 00:00:00 2001 From: John Nonweiler Date: Fri, 5 Oct 2018 15:53:05 +0100 Subject: [PATCH 4/6] Change doxygen subsection label Doxygen was giving a warning message about "multiple use of section label 'deprecated'", so this commit changes the section label. There are no references to this section, so the label is only changed in one place. (I can't find any other uses of this section label, so the warning message seems to be wrong, but it doesn't hurt to fix it.) --- src/solvers/README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/solvers/README.md b/src/solvers/README.md index a9a9a3639c9..ce1487e9682 100644 --- a/src/solvers/README.md +++ b/src/solvers/README.md @@ -308,7 +308,7 @@ allocates a new string before calling a primitive. \copybrief add_axioms_for_parse_int \link add_axioms_for_parse_int More... \endlink -\subsection deprecated Deprecated primitives: +\subsection solvers-deprecated Deprecated primitives: * `cprover_string_concat_code_point`, `cprover_string_code_point_at`, `cprover_string_code_point_before`, `cprover_string_code_point_count`: From ada175661f873d984ad318233e54616db3b38286 Mon Sep 17 00:00:00 2001 From: John Nonweiler Date: Fri, 5 Oct 2018 16:06:51 +0100 Subject: [PATCH 5/6] Update params in doxygen comments Delete documentation for parameters which no longer exist --- src/analyses/local_safe_pointers.cpp | 2 -- src/solvers/refinement/string_constraint.h | 4 ---- 2 files changed, 6 deletions(-) diff --git a/src/analyses/local_safe_pointers.cpp b/src/analyses/local_safe_pointers.cpp index 213bdecabc2..4b864adbb10 100644 --- a/src/analyses/local_safe_pointers.cpp +++ b/src/analyses/local_safe_pointers.cpp @@ -177,7 +177,6 @@ void local_safe_pointerst::operator()(const goto_programt &goto_program) /// \param out: stream to write output to /// \param goto_program: GOTO program analysed (the same one passed to /// operator()) -/// \param ns: global namespace void local_safe_pointerst::output( std::ostream &out, const goto_programt &goto_program) { @@ -219,7 +218,6 @@ void local_safe_pointerst::output( /// \param out: stream to write output to /// \param goto_program: GOTO program analysed (the same one passed to /// operator()) -/// \param ns: global namespace void local_safe_pointerst::output_safe_dereferences( std::ostream &out, const goto_programt &goto_program) { diff --git a/src/solvers/refinement/string_constraint.h b/src/solvers/refinement/string_constraint.h index f92bce2211d..2786f91e0e8 100644 --- a/src/solvers/refinement/string_constraint.h +++ b/src/solvers/refinement/string_constraint.h @@ -104,8 +104,6 @@ class string_constraintt final }; /// Used for debug printing. -/// \param [in] ns: namespace for `from_expr` -/// \param [in] identifier: identifier for `from_expr` /// \param [in] expr: constraint to render /// \return rendered string inline std::string to_string(const string_constraintt &expr) @@ -176,8 +174,6 @@ class string_not_contains_constraintt : public exprt }; /// Used for debug printing. -/// \param [in] ns: namespace for `from_expr` -/// \param [in] identifier: identifier for `from_expr` /// \param [in] expr: constraint to render /// \return rendered string inline std::string to_string(const string_not_contains_constraintt &expr) From eea5403d0a0f77b711bb1263dd937205b024a8ad Mon Sep 17 00:00:00 2001 From: John Nonweiler Date: Mon, 8 Oct 2018 14:48:17 +0100 Subject: [PATCH 6/6] Update comment to make doxygen happy Doxygen produced a warning about a reference it couldn't find, because of a '#' symbol used in the comment (which the author didn't intend to be a reference). Usually, '#' could be escaped '\#', but that doesn't work in this case, because it appears within quotes (as explained in https://stackoverflow.com/a/36750674 ). I couldn't find a way to get this to work with the quotes that had been used, so I have changed it to use different quotes. --- src/util/README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/util/README.md b/src/util/README.md index b0f6d321769..89b4850e4b7 100644 --- a/src/util/README.md +++ b/src/util/README.md @@ -89,7 +89,7 @@ efficient to store many copies of the same string. The static list of strings is initially populated from `irep_ids.def`, so for example the fourth entry in `irep_ids.def` is `“IREP_ID_ONE(type)”`, so the string “type” has index 3. You can refer to this \ref irep_idt as `ID_type`. The other kind of line you -see is `“IREP_ID_TWO(C_source_location, #source_location)”`, which means the +see is \c "IREP_ID_TWO(C_source_location, #source_location)", which means the \ref irep_idt for the string “\#source_location” can be referred to as `ID_C_source_location`. The “C” is for comment, meaning that it should be stored in the [comments](\ref irept::dt::comments). Any strings that need