Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
58 changes: 29 additions & 29 deletions jbmc/src/java_bytecode/character_refine_preprocess.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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(
Expand Down Expand Up @@ -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(
Expand Down Expand Up @@ -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(
Expand All @@ -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(
Expand All @@ -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(
Expand All @@ -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(
Expand All @@ -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(
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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(
Expand All @@ -539,11 +539,11 @@ 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 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(
Expand Down Expand Up @@ -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(
Expand Down Expand Up @@ -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(
Expand Down Expand Up @@ -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(
Expand All @@ -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(
Expand Down Expand Up @@ -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(
Expand Down Expand Up @@ -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(
Expand All @@ -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(
Expand Down Expand Up @@ -1074,9 +1074,9 @@ 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 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(
Expand Down Expand Up @@ -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(
Expand All @@ -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(
Expand All @@ -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(
Expand Down
2 changes: 1 addition & 1 deletion jbmc/src/java_bytecode/java_bytecode_convert_class.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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_annotationt> &java_annotations)
Expand Down
2 changes: 0 additions & 2 deletions src/analyses/local_safe_pointers.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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)
{
Expand Down Expand Up @@ -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)
{
Expand Down
2 changes: 1 addition & 1 deletion src/goto-instrument/wmm/goto2graph.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
2 changes: 1 addition & 1 deletion src/solvers/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -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`:
Expand Down
4 changes: 0 additions & 4 deletions src/solvers/refinement/string_constraint.h
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down Expand Up @@ -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)
Expand Down
4 changes: 2 additions & 2 deletions src/util/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -89,8 +89,8 @@ 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
\ref irep_idt for the string “#source_location” can be referred to as
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
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Maybe this change doesn't actually achieve what it is supposed to do? Doxygen now appears to be complaining that the link request could not be satisfied.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This changed worked. The problem is the other #source_location on the previous line. (I'm not sure how I missed this earlier!)

This has turned out to be much more tricky to fix - adding a \ doesn't work in this case (as explained in https://stackoverflow.com/a/36750674 ). I haven't found a perfect solution to this, but have now committed something that works with slightly different double quotes.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think this is good, especially with the elaborate commit message. It's not beautiful, but anyone can easily figure out what's going on here.

`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`
Expand Down
3 changes: 2 additions & 1 deletion src/util/expr_iterator.h
Original file line number Diff line number Diff line change
Expand Up @@ -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
///
Expand Down
3 changes: 2 additions & 1 deletion src/util/irep_ids.h
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,8 @@ Author: Reuben Thomas, reuben.thomas@me.com
#include <string>
#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`.
Expand Down