Documentation fixes in stirng constraint generator

Updates in code point, add_axioms_for_constant, constraint for float
 add_axioms_from_float_scientific_notation,
 update add_axioms_for_empty_string.
Xemove <tt> tag (does not seem supported by doxygen).
Add documentation for associate_array_to_pointer, associate_length_to_array.

Author: romainbrenguier

src/solvers/refinement/string_constraint_generator_code_points.cpp

@@ -16,7 +16,7 @@ Author: Romain Brenguier, [email protected]
 /// code point to a utf-16 string
 /// \param res: array of characters corresponding to the result fo the function
 /// \param code_point: an expression representing a java code point
-/// \return an expression
+/// \return integer expression equal to zero
 exprt string_constraint_generatort::add_axioms_for_code_point(
   const array_string_exprt &res,
   const exprt &code_point)
@@ -113,7 +113,7 @@ exprt pair_value(exprt char1, exprt char2, typet return_type)
 }
 
 /// add axioms corresponding to the String.codePointAt java function
-/// \par parameters: function application with two arguments: a string and an
+/// \param f: function application with arguments a string and an
 ///   index
 /// \return a integer expression corresponding to a code point
 exprt string_constraint_generatort::add_axioms_for_code_point_at(
@@ -175,8 +175,8 @@ exprt string_constraint_generatort::add_axioms_for_code_point_before(
 
 /// add axioms giving approximate bounds on the result of the
 /// String.codePointCount java function
-/// \par parameters: function application with three arguments: a string and two
-///   indexes
+/// \param f: function application with three arguments string `str`, integer
+///           `begin` and integer `end`.
 /// \return an integer expression
 exprt string_constraint_generatort::add_axioms_for_code_point_count(
   const function_application_exprt &f)
@@ -198,8 +198,8 @@ exprt string_constraint_generatort::add_axioms_for_code_point_count(
 /// add axioms giving approximate bounds on the result of the
 /// String.offsetByCodePointCount java function. We approximate the result by
 /// saying the result is between index + offset and index + 2 * offset
-/// \par parameters: function application with three arguments: a string and two
-///   indexes
+/// \param f: function application with arguments string `str`, integer `index`
+///           and integer `offset`.
 /// \return a new string expression
 exprt string_constraint_generatort::add_axioms_for_offset_by_code_point(
   const function_application_exprt &f)

src/solvers/refinement/string_constraint_generator_constants.cpp

@@ -17,8 +17,9 @@ Author: Romain Brenguier, [email protected]
 
 /// add axioms saying the returned string expression should be equal to the
 /// string constant
-/// \par parameters: a string constant
-/// \return a string expression
+/// \param res: array of characters for the result
+/// \param sval: a string constant
+/// \return integer expression equal to zero
 exprt string_constraint_generatort::add_axioms_for_constant(
   const array_string_exprt &res,
   irep_idt sval)
@@ -52,8 +53,9 @@ exprt string_constraint_generatort::add_axioms_for_constant(
 }
 
 /// add axioms to say that the returned string expression is empty
-/// \par parameters: function application without argument
-/// \return string expression
+/// \param f: function application with arguments integer `length` and character
+///           pointer `ptr`.
+/// \return integer expression equal to zero
 exprt string_constraint_generatort::add_axioms_for_empty_string(
   const function_application_exprt &f)
 {

src/solvers/refinement/string_constraint_generator_float.cpp

@@ -149,7 +149,7 @@ exprt estimate_decimal_exponent(const exprt &f, const ieee_float_spect &spec)
 
 /// Add axioms corresponding to the String.valueOf(F) java function
 /// \param f: function application with one float argument
-/// \return a integer expression
+/// \return an integer expression
 exprt string_constraint_generatort::add_axioms_for_string_of_float(
   const function_application_exprt &f)
 {
@@ -169,12 +169,12 @@ exprt string_constraint_generatort::add_axioms_from_double(
 }
 
 /// Add axioms corresponding to the integer part of m, in decimal form with no
-/// leading zeroes, followed by `'.'` (`'\\u002E'`), followed by one or more
-/// decimal digits representing the fractional part of m. This specification is
-/// correct for inputs that do not exceed 100000 and the function is unspecified
-/// for other values.
+/// leading zeroes, followed by '.', followed by
+/// one or more decimal digits representing the fractional part of m.
+/// This specification is correct for inputs that do not exceed 100000 and the
+/// function is unspecified for other values.
 ///
-/// TODO: this specification is not correct for negative numbers and
+/// \todo: this specification is not correct for negative numbers and
 /// double precision
 /// \param res: string expression corresponding to the result
 /// \param f: expression representing a float
@@ -474,7 +474,7 @@ exprt string_constraint_generatort::add_axioms_from_float_scientific_notation(
 /// Add axioms corresponding to the scientific representation of floating point
 /// values
 /// \param f: a function application expression
-/// \return code 0 on succes
+/// \return code 0 on success
 exprt string_constraint_generatort::add_axioms_from_float_scientific_notation(
   const function_application_exprt &f)
 {

src/solvers/refinement/string_constraint_generator_insert.cpp

@@ -48,8 +48,9 @@ exprt string_constraint_generatort::add_axioms_for_insert(
 
 /// add axioms corresponding to the StringBuilder.insert(int, CharSequence) and
 /// StringBuilder.insert(int, CharSequence, int, int) java functions
-/// \par parameters: function application with three arguments: two strings and
-///   an index
+/// \param f: function application with arguments integer `|res|`, char pointer
+///           `&res[0]`, refined string `s1`, refined string `s2`,
+///           integer `offset`
 /// \return a new string expression
 exprt string_constraint_generatort::add_axioms_for_insert(
   const function_application_exprt &f)

src/solvers/refinement/string_constraint_generator_main.cpp

@@ -241,6 +241,13 @@ string_constraint_generatort::associate_char_array_to_char_pointer(
   return result;
 }
 
+/// Associate a char array to a char pointer.
+/// Insert in `arrays_of_pointers_` a binding from `ptr` to `arr`.
+/// If the length of `arr` is infinite, we create a new integer symbol and add
+/// a binding from `arr` to this length in `length_of_array_`.
+/// This also adds the default axioms for `arr`.
+/// \param f: a function application with argument a character array `arr` and
+/// a character pointer `ptr`.
 exprt string_constraint_generatort::associate_array_to_pointer(
   const function_application_exprt &f)
 {
@@ -263,6 +270,11 @@ exprt string_constraint_generatort::associate_array_to_pointer(
   return from_integer(0, f.type());
 }
 
+/// Associate an integer length to a char array.
+/// This adds an axiom ensuring that `arr.length` and `length` are equal.
+/// \param f: a function application with argument a character array `arr` and
+/// a integer `length`.
+/// \return integer expression equal to 0
 exprt string_constraint_generatort::associate_length_to_array(
   const function_application_exprt &f)
 {