Doxygen corrections

Author: romainbrenguier

src/java_bytecode/java_string_library_preprocess.cpp

@@ -712,17 +712,18 @@ void add_array_to_length_association(
       symbol_table));
 }
 
-/// \param string_expr: a string expression
 /// \param function_name: the name of the function
 /// \param arguments: arguments of the function
+/// \param loc: source location
 /// \param symbol_table: symbol table
-/// \return return the following code:
+/// \param [out] code: gets added the following code:
 /// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 /// int return_code;
 /// int str.length;
 /// char str.data[str.length]
 /// return_code = <function_name>_data(str.length, str.data, arguments)
 /// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+/// \return a new string expression
 refined_string_exprt java_string_library_preprocesst::string_expr_of_function(
   const irep_idt &function_name,
   const exprt::operandst &arguments,
@@ -845,14 +846,15 @@ void java_string_library_preprocesst::code_assign_java_string_to_string_expr(
 }
 
 /// Create a string expression whose value is given by a literal
-/// \param lhs: an expression representing a java string
 /// \param s: the literal to be assigned
+/// \param loc: location in the source
 /// \param symbol_table: symbol table
-/// \param code: gets added the following:
+/// \param [out] code: gets added the following:
 /// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 /// tmp_string = "<s>"
 /// lhs = cprover_string_literal_func(tmp_string)
 /// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+/// \return a new refined string
 refined_string_exprt
 java_string_library_preprocesst::string_literal_to_string_expr(
   const std::string &s,

src/solvers/refinement/string_constraint.h

@@ -13,9 +13,9 @@ Author: Romain Brenguier, [email protected]
 /// \file
 /// Defines string constraints. These are formulas talking about strings.  We
 ///   implemented two forms of constraints: `string_constraintt`  are formulas
-///   of the form $\forall univ_var \in [lb,ub[. prem => body$, and
-///   not_contains_constraintt of the form: $\forall x in [lb,ub[. p(x) =>
-///   \exists y in [lb,ub[. s1[x+y] != s2[y]$.
+///   of the form \f$\forall univ\_var \in [lb,ub[. prem => body\f$, and
+///   not_contains_constraintt of the form: \f$\forall x \in [lb,ub[. p(x) =>
+///   \exists y \in [lb,ub[. s1[x+y] \ne s2[y]\f$.
 
 #ifndef CPROVER_SOLVERS_REFINEMENT_STRING_CONSTRAINT_H
 #define CPROVER_SOLVERS_REFINEMENT_STRING_CONSTRAINT_H

src/solvers/refinement/string_constraint_generator_code_points.cpp

@@ -14,7 +14,8 @@ Author: Romain Brenguier, [email protected]
 
 /// add axioms for the conversion of an integer representing a java
 /// code point to a utf-16 string
-/// \param code_point an expression representing a java code point
+/// \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
 exprt string_constraint_generatort::add_axioms_for_code_point(
   const array_string_exprt &res,
@@ -69,7 +70,7 @@ exprt string_constraint_generatort::add_axioms_for_code_point(
 /// encoding, see https://en.wikipedia.org/wiki/UTF-16 for more explenation
 /// about the encoding; this is true when the character is in the range
 /// 0xD800..0xDBFF
-/// \par parameters: a character expression
+/// \param chr: a character expression
 /// \return a Boolean expression
 exprt string_constraint_generatort::is_high_surrogate(const exprt &chr)
 {
@@ -82,7 +83,7 @@ exprt string_constraint_generatort::is_high_surrogate(const exprt &chr)
 /// encoding, see https://en.wikipedia.org/wiki/UTF-16 for more explenation
 /// about the encoding; this is true when the character is in the range
 /// 0xDC00..0xDFFF
-/// \par parameters: a character expression
+/// \param chr: a character expression
 /// \return a Boolean expression
 exprt string_constraint_generatort::is_low_surrogate(const exprt &chr)
 {
@@ -96,8 +97,9 @@ exprt string_constraint_generatort::is_low_surrogate(const exprt &chr)
 /// https://en.wikipedia.org/wiki/UTF-16 for more explenation about the
 /// encoding; the operation we perform is:
 /// pair_value=0x10000+(((char1%0x0800)*0x0400)+char2%0x0400)
-/// \par parameters: two character expressions and a return type
-/// char1 and char2 should be of type return_type
+/// \param char1: a character expression
+/// \param char2: a character expression
+/// \param return_type: type of the expression to return
 /// \return an integer expression of type return_type
 exprt pair_value(exprt char1, exprt char2, typet return_type)
 {

src/solvers/refinement/string_constraint_generator_concat.cpp

@@ -13,7 +13,7 @@ Author: Romain Brenguier, [email protected]
 
 #include <solvers/refinement/string_constraint_generator.h>
 
-/// Add axioms enforcing that `s0` is the concatenation of `s1` with
+/// Add axioms enforcing that `res` is the concatenation of `s1` with
 /// the substring of `s2` starting at index `start_index` and ending
 /// at index `end_index`.
 ///
@@ -64,6 +64,12 @@ exprt string_constraint_generatort::add_axioms_for_concat_substr(
   return from_integer(0, res.length().type());
 }
 
+/// Add axioms enforcing that `res` is the concatenation of `s1` with
+/// character `c`.
+/// \param res: string expression
+/// \param s1: string expression
+/// \param c: character expression
+/// \return code 0 on success
 exprt string_constraint_generatort::add_axioms_for_concat_char(
   const array_string_exprt &res,
   const array_string_exprt &s1,
@@ -87,15 +93,14 @@ exprt string_constraint_generatort::add_axioms_for_concat_char(
   m_axioms.push_back(a3);
 
   // We should have a enum type for the possible error codes
-  return from_integer(0, res.length().type());
+  return from_integer(0, return_code_type);
 }
 
-/// Add axioms to say that `s0` is equal to the concatenation of `s1` and `s2`.
-/// \param s0: string_expression corresponding to the result
+/// Add axioms to say that `res` is equal to the concatenation of `s1` and `s2`.
+/// \param res: string_expression corresponding to the result
 /// \param s1: the string expression to append to
 /// \param s2: the string expression to append to the first one
 /// \return an integer expression
-
 exprt string_constraint_generatort::add_axioms_for_concat(
   const array_string_exprt &res,
   const array_string_exprt &s1,
@@ -129,6 +134,12 @@ exprt string_constraint_generatort::add_axioms_for_concat(
     return add_axioms_for_concat(res, s1, s2);
 }
 
+/// Add axioms enforcing that the string represented by the two first
+/// expressions is equal to the concatenation of the string argument and
+/// the character argument of the function application.
+/// \param f: function application with a length, pointer, string and character
+///           argument.
+/// \return code 0 on success
 exprt string_constraint_generatort::add_axioms_for_concat_char(
   const function_application_exprt &f)
 {

src/solvers/refinement/string_constraint_generator_float.cpp

@@ -71,6 +71,7 @@ exprt get_significand(
 
 /// Create an expression to represent a float or double value.
 /// \param f: a floating point value in double precision
+/// \param float_spec: a specification for floats
 /// \return an expression representing this floating point
 exprt constant_float(const double f, const ieee_float_spect &float_spec)
 {
@@ -97,7 +98,6 @@ exprt round_expr_to_zero(const exprt &f)
 /// Note that the rounding mode is set to ROUND_TO_EVEN.
 /// \param f: a floating point expression
 /// \param g: a floating point expression
-/// \param rounding: rounding mode
 /// \return An expression representing floating point multiplication.
 exprt floatbv_mult(const exprt &f, const exprt &g)
 {
@@ -124,8 +124,8 @@ exprt floatbv_of_int_expr(const exprt &i, const ieee_float_spect &spec)
 
 /// Estimate the decimal exponent that should be used to represent a given
 /// floating point value in decimal.
-/// We are looking for d such that n * 10^d = m * 2^e, so:
-/// d = log_10(m) + log_10(2) * e - log_10(n)
+/// We are looking for \f$d\f$ such that \f$n * 10^d = m * 2^e\f$, so:
+/// \f$d = log_10(m) + log_10(2) * e - log_10(n)\f$
 /// m -- the fraction -- should be between 1 and 2 so log_10(m)
 /// in [0,log_10(2)].
 /// n -- the fraction in base 10 -- should be between 1 and 10 so
@@ -169,10 +169,10 @@ 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 `'.'` (`'\\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.
 ///
 /// TODO: this specification is not correct for negative numbers and
 /// double precision
@@ -219,11 +219,11 @@ exprt string_constraint_generatort::add_axioms_for_string_of_float(
 
 /// Add axioms for representing the fractional part of a floating point starting
 /// with a dot
+/// \param res: string expression for the result
 /// \param int_expr: an integer expression
 /// \param max_size: a maximal size for the string, this includes the
 ///   potential minus sign and therefore should be greater than 2
-/// \param ref_type: a type for refined strings
-/// \return a string expression
+/// \return code 0 on success
 exprt string_constraint_generatort::add_axioms_for_fractional_part(
   const array_string_exprt &res,
   const exprt &int_expr,
@@ -297,20 +297,18 @@ exprt string_constraint_generatort::add_axioms_for_fractional_part(
 
 /// Add axioms to write the float in scientific notation.
 ///
-/// A float is represented as $f = m * 2^e$ where $0 <= m < 2$ is the
-/// significand and $-126 <= e <= 127$ is the exponent.
-/// We want an alternate representation by finding $n$ and
-/// $d$ such that $f=n*10^d$. We can estimate $d$ the following way:
-/// $d ~= log_10(f/n) ~= log_10(m) + log_10(2) * e - log_10(n)$
-/// $d = floor(log_10(2) * e)$
-/// Then $n$ can be expressed by the equation:
-/// $log_10(n) = log_10(m) + log_10(2) * e - d$
-/// $n = f / 10^d = m * 2^e / 10^d = m * 2^e / 10^(floor(log_10(2) * e))$
+/// A float is represented as \f$f = m * 2^e\f$ where \f$0 <= m < 2\f$ is the
+/// significand and \f$-126 <= e <= 127\f$ is the exponent.
+/// We want an alternate representation by finding \f$n\f$ and
+/// \f$d\f$ such that \f$f=n*10^d\f$. We can estimate \f$d\f$ the following way:
+/// \f$d ~= log_10(f/n) ~= log_10(m) + log_10(2) * e - log_10(n)\f$
+/// \f$d = floor(log_10(2) * e)\f$
+/// Then \f$n\f$ can be expressed by the equation:
+/// \f$log_10(n) = log_10(m) + log_10(2) * e - d\f$
+/// \f$n = f / 10^d = m * 2^e / 10^d = m * 2^e / 10^(floor(log_10(2) * e))\f$
 /// TODO: For now we only consider single precision.
 /// \param res: string expression representing the float in scientific notation
 /// \param f: a float expression, which is positive
-/// \param max_size: a maximal size for the string
-/// \param ref_type: a type for refined strings
 /// \return a integer expression different from 0 to signal an exception
 exprt string_constraint_generatort::add_axioms_from_float_scientific_notation(
   const array_string_exprt &res,
@@ -476,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 a new string expression
+/// \return code 0 on succes
 exprt string_constraint_generatort::add_axioms_from_float_scientific_notation(
   const function_application_exprt &f)
 {

src/solvers/refinement/string_constraint_generator_format.cpp

@@ -253,7 +253,8 @@ static exprt get_component_in_struct(
 /// specifier.
 /// \param fs: a format specifier
 /// \param arg: a struct containing the possible value of the argument to format
-/// \param ref_type: a type  for refined string type
+/// \param index_type: type for indexes in strings
+/// \param char_type: type of characters
 /// \return String expression representing the output of String.format.
 array_string_exprt
 string_constraint_generatort::add_axioms_for_format_specifier(
@@ -341,10 +342,10 @@ string_constraint_generatort::add_axioms_for_format_specifier(
 
 /// Parse `s` and add axioms ensuring the output corresponds to the output of
 /// String.format.
+/// \param res: string expression for the result of the format function
 /// \param s: a format string
 /// \param args: a vector of arguments
-/// \param ref_type: a type  for refined string type
-/// \return String expression representing the output of String.format.
+/// \return code, 0 on success
 exprt string_constraint_generatort::add_axioms_for_format(
   const array_string_exprt &res,
   const std::string &s,

src/solvers/refinement/string_constraint_generator_transformation.cpp

@@ -317,7 +317,7 @@ exprt string_constraint_generatort::add_axioms_for_to_upper_case(
 }
 
 /// add axioms corresponding to the String.toUpperCase java function
-/// \param expr: function application with one string argument
+/// \param f: function application with one string argument
 /// \return a new string expression
 exprt string_constraint_generatort::add_axioms_for_to_upper_case(
   const function_application_exprt &f)
@@ -332,9 +332,8 @@ exprt string_constraint_generatort::add_axioms_for_to_upper_case(
 /// add axioms corresponding stating that the result is similar to that of the
 /// StringBuilder.setCharAt java function Warning: this may be underspecified in
 /// the case wher the index exceed the length of the string
-/// \par parameters: function application with three arguments, the first is a
-///   string
-/// the second an index and the third a character
+/// \param f: function application with three arguments, the first is a
+///           string, the second an index and the third a character
 /// \return a new string expression
 exprt string_constraint_generatort::add_axioms_for_char_set(
   const function_application_exprt &f)