diff --git a/CODING_STANDARD.md b/CODING_STANDARD.md index 6a8b923b0a..06ca5bc6ab 100644 --- a/CODING_STANDARD.md +++ b/CODING_STANDARD.md @@ -70,13 +70,17 @@ Formatting is enforced using clang-format. For more information about this, see /// This sentence, until the first dot followed by whitespace, becomes /// the brief description. More detailed text follows. Feel free to /// break this into paragraphs to aid readability. - /// \param arg_name: This parameter doesn't need much description - /// \param [out] long_arg_name: This parameter is mutated by the function. - /// Extra info about the parameter gets indented an extra two columns, + /// \param arg: This parameter doesn't need much description + /// \param long_arg: This parameter needs a long description. Extra + /// information about the parameter gets indented an extra two columns, /// like this. + /// \param [out] out_arg: This parameter is mutated by the function, and + /// its value at the beginning of the function is not used + /// \param [in,out] in_out_arg: This parameter is mutated by the function, and + /// its value at the beginning of the function is used /// \return The return value is literally the value returned by the - /// function. For out-parameters, use "\param [out]". - return_typet my_function(argt arg_name, argt &long_arg_name) + /// function. For out-parameters, use "\param [out]" or "\param [in,out]". + ret_typet function(argt arg, argt long_arg, argt &out_arg, argt &in_out_arg) ``` - The priority of documentation is readability. Therefore, feel free to use Doxygen features, or to add whitespace for multi-paragraph comment blocks if diff --git a/jbmc/src/java_bytecode/character_refine_preprocess.cpp b/jbmc/src/java_bytecode/character_refine_preprocess.cpp index 79b4769cb3..5202f7bdc8 100644 --- a/jbmc/src/java_bytecode/character_refine_preprocess.cpp +++ b/jbmc/src/java_bytecode/character_refine_preprocess.cpp @@ -125,14 +125,13 @@ codet character_refine_preprocesst::convert_compare(conversion_inputt &target) return code_assignt(result, expr); } - /// Converts function call to an assignment of an expression corresponding to /// the java method Character.digit:(CI)I. The function call has one character /// argument and an optional integer radix argument. If the radix is not given /// it is set to 36 by default. /// \param target: a position in a goto program /// \return code assigning the result of the Character.digit function to the -/// left-hand-side of the given target +/// left-hand-side of the given target codet character_refine_preprocesst::convert_digit_char( conversion_inputt &target) { diff --git a/jbmc/src/java_bytecode/ci_lazy_methods.cpp b/jbmc/src/java_bytecode/ci_lazy_methods.cpp index 33408a8d34..e7d949955c 100644 --- a/jbmc/src/java_bytecode/ci_lazy_methods.cpp +++ b/jbmc/src/java_bytecode/ci_lazy_methods.cpp @@ -498,7 +498,7 @@ void ci_lazy_methodst::get_virtual_method_targets( /// \param e: expression tree to search /// \param symbol_table: global symbol table /// \param [out] needed: Populated with global variable symbols referenced from -/// `e` or its children. +/// `e` or its children. void ci_lazy_methodst::gather_needed_globals( const exprt &e, const symbol_tablet &symbol_table, diff --git a/jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.cpp b/jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.cpp index be9f02ebb3..b6514d6a2e 100644 --- a/jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.cpp +++ b/jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.cpp @@ -4,9 +4,9 @@ #include -/// \param type Source type +/// \param type: Source type /// \return The vector of implicitly generic and (explicitly) generic type -/// parameters of the given type. +/// parameters of the given type. const std::vector get_all_generic_parameters(const typet &type) { @@ -37,8 +37,8 @@ get_all_generic_parameters(const typet &type) /// Add pairs to the controlled map. Own the keys and pop from their stack /// on destruction; otherwise do nothing. -/// \param parameters generic parameters that are the keys of the pairs to add -/// \param types a type to add for each parameter +/// \param parameters: generic parameters that are the keys of the pairs to add +/// \param types: a type to add for each parameter void generic_parameter_specialization_map_keyst::insert_pairs( const std::vector ¶meters, const std::vector &types) @@ -87,9 +87,9 @@ void generic_parameter_specialization_map_keyst::insert_pairs( /// Add a pair of a parameter and its types for each generic parameter of the /// given generic pointer type to the controlled map. Own the keys and pop /// from their stack on destruction; otherwise do nothing. -/// \param pointer_type pointer type to get the specialized generic types from -/// \param pointer_subtype_struct struct type to which the generic pointer -/// points, must be generic if the pointer is generic +/// \param pointer_type: pointer type to get the specialized generic types from +/// \param pointer_subtype_struct: struct type to which the generic pointer +/// points, must be generic if the pointer is generic void generic_parameter_specialization_map_keyst::insert_pairs_for_pointer( const pointer_typet &pointer_type, const typet &pointer_subtype_struct) @@ -136,9 +136,10 @@ void generic_parameter_specialization_map_keyst::insert_pairs_for_pointer( /// in the form of a symbol rather than a pointer (as opposed to the function /// insert_pairs_for_pointer). Own the keys and pop from their stack /// on destruction; otherwise do nothing. -/// \param struct_tag_type symbol type to get the specialized generic types from -/// \param symbol_struct struct type of the symbol type, must be generic if -/// the symbol is generic +/// \param struct_tag_type: symbol type to get the specialized generic types +/// from +/// \param symbol_struct: struct type of the symbol type, must be generic if +/// the symbol is generic void generic_parameter_specialization_map_keyst::insert_pairs_for_symbol( const struct_tag_typet &struct_tag_type, const typet &symbol_struct) diff --git a/jbmc/src/java_bytecode/jar_file.h b/jbmc/src/java_bytecode/jar_file.h index 64fe230163..811e9b0da7 100644 --- a/jbmc/src/java_bytecode/jar_file.h +++ b/jbmc/src/java_bytecode/jar_file.h @@ -24,13 +24,13 @@ class jar_filet final { public: /// Open java file for reading. - /// \param filename Name of the file + /// \param filename: Name of the file /// \throw Throws std::runtime_error if file cannot be opened explicit jar_filet(const std::string &filename); /// Open a JAR file of size \p size loaded in memory at address \p data. - /// \param data memory buffer with the contents of the jar file - /// \param size size of the memory buffer + /// \param data: memory buffer with the contents of the jar file + /// \param size: size of the memory buffer /// \throw Throws std::runtime_error if file cannot be opened jar_filet(const void *data, size_t size); @@ -42,7 +42,7 @@ public: /// Get contents of a file in the jar archive. /// Returns nullopt if file doesn't exist. - /// \param filename Name of the file in the archive + /// \param filename: Name of the file in the archive optionalt get_entry(const std::string &filename); /// Get contents of the Manifest file in the jar archive as a key-value map diff --git a/jbmc/src/java_bytecode/jar_pool.h b/jbmc/src/java_bytecode/jar_pool.h index 2216688bb8..88f594c801 100644 --- a/jbmc/src/java_bytecode/jar_pool.h +++ b/jbmc/src/java_bytecode/jar_pool.h @@ -19,16 +19,16 @@ class jar_poolt { public: /// Load jar archive or retrieve from cache if already loaded - /// \param jar_path name of the file + /// \param jar_path: name of the file // Throws an exception if the file does not exist jar_filet &operator()(const std::string &jar_path); - /// Add a jar archive or retrieve from cache if already added - /// \param buffer_name name of the original file - /// \param pmem memory pointer to the contents of the file - /// \param size size of the memory buffer + /// Add a jar archive or retrieve from cache if already added. /// Note that this mocks the existence of a file which may - /// or may not exist since the actual data bis retrieved from memory. + /// or may not exist since the actual data is retrieved from memory. + /// \param buffer_name: name of the original file + /// \param pmem: memory pointer to the contents of the file + /// \param size: size of the memory buffer jar_filet & add_jar(const std::string &buffer_name, const void *pmem, size_t size); diff --git a/jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp b/jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp index 89c6f6c0c0..eb1a43696f 100644 --- a/jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp @@ -62,7 +62,7 @@ static symbolt add_or_get_symbol( /// Retrieve the first label identifier. This is used to mark the start of /// a thread block. /// /param id: unique thread block identifier -/// /return: fully qualified label identifier +/// /return fully qualified label identifier static const std::string get_first_label_id(const std::string &id) { return CPROVER_PREFIX "_THREAD_ENTRY_" + id; @@ -71,7 +71,7 @@ static const std::string get_first_label_id(const std::string &id) /// Retrieve the second label identifier. This is used to mark the end of /// a thread block. /// /param id: unique thread block identifier -/// /return: fully qualified label identifier +/// /return fully qualified label identifier static const std::string get_second_label_id(const std::string &id) { return CPROVER_PREFIX "_THREAD_EXIT_" + id; @@ -80,7 +80,7 @@ static const std::string get_second_label_id(const std::string &id) /// Retrieves a thread block identifier from a function call to /// CProver.startThread:(I)V or CProver.endThread:(I)V /// /param code: function call to CProver.startThread or CProver.endThread -/// /return: unique thread block identifier +/// /return unique thread block identifier static const std::string get_thread_block_identifier( const code_function_callt &f_code) { diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp index d370672d76..c754d856de 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp @@ -176,9 +176,9 @@ private: /// - class: A extends B implements C, D /// - signature: B;LC;LD; /// - returned superclass reference: B; -/// \param signature Signature of the class +/// \param signature: Signature of the class /// \return Reference of the generic superclass, or empty if the superclass -/// is not generic +/// is not generic static optionalt extract_generic_superclass_reference(const optionalt &signature) { @@ -215,10 +215,10 @@ extract_generic_superclass_reference(const optionalt &signature) /// - signature: B;LC;LD; /// - returned interface reference for C: LC; /// - returned interface reference for D: LD; -/// \param signature Signature of the class -/// \param interface_name The interface name +/// \param signature: Signature of the class +/// \param interface_name: The interface name /// \return Reference of the generic interface, or empty if the interface -/// is not generic +/// is not generic static optionalt extract_generic_interface_reference( const optionalt &signature, const std::string &interface_name) @@ -982,8 +982,8 @@ bool java_bytecode_convert_class( /// Example: if \p parameter has identifier `java::Outer$Inner::T` and /// there is a replacement parameter with identifier `java::Outer::T`, the /// identifier of \p parameter gets set to `java::Outer::T`. -/// \param parameter -/// \param replacement_parameters vector of generic parameters (only viable +/// \param parameter: The given generic type parameter +/// \param replacement_parameters: vector of generic parameters (only viable /// ones, i.e., only those that can actually appear here such as generic /// parameters of outer classes of the class specified by the prefix of \p /// parameter identifier) @@ -1034,8 +1034,6 @@ static void find_and_replace_parameter( /// Example: class `Outer` has an inner class `Inner` that has a field /// `t` of type `Generic`. This function ensures that the parameter points to /// `java::Outer::T` instead of `java::Outer$Inner::T`. -/// \param type -/// \param replacement_parameters static void find_and_replace_parameters( typet &type, const std::vector &replacement_parameters) @@ -1118,8 +1116,6 @@ void convert_java_annotations( /// any generic class. All uses of the implicit generic type parameters within /// the inner class are updated to point to the type parameters of the /// corresponding outer classes. -/// \param class_name -/// \param symbol_table void mark_java_implicitly_generic_class_type( const irep_idt &class_name, symbol_tablet &symbol_table) diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp index 9aa2f519cf..ebde6e5c22 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp @@ -76,11 +76,11 @@ protected: /// Iterates through the parameters of the function type \p ftype, finds a new /// new name for each parameter and renames them in `ftype.parameters()` as /// well as in the \p symbol_table. -/// \param[in,out] ftype: +/// \param [in,out] ftype: /// Function type whose parameters should be named. /// \param name_prefix: /// Prefix for parameter names, typically the parent function's name. -/// \param[in,out] symbol_table: +/// \param [in,out] symbol_table: /// Global symbol table. /// \return Assigns parameter names (side-effects on `ftype`) to function stub /// parameters, which are initially nameless as method conversion hasn't @@ -191,18 +191,14 @@ symbol_exprt java_bytecode_convert_methodt::tmp_variable( /// Returns an expression indicating a local variable suitable to load/store /// from a bytecode at address `address` a value of type `type_char` stored in /// the JVM's slot `arg`. -/// -/// \param arg -/// The local variable slot -/// \param type_char -/// The type of the value stored in the slot pointed by `arg`. -/// \param address -/// Bytecode address used to find a variable that the LVT declares to be live -/// and living in the slot pointed by `arg` for this bytecode. -/// \param do_cast -/// Indicates whether we should return the original symbol_exprt or a -/// typecast_exprt if the type of the symbol_exprt does not equal that -/// represented by `type_char`. +/// \param arg: The local variable slot +/// \param type_char: The type of the value stored in the slot pointed by `arg` +/// \param address: Bytecode address used to find a variable that the LVT +/// declares to be live and living in the slot pointed by `arg` for this +/// bytecode +/// \param do_cast: Indicates whether we should return the original symbol_exprt +/// or a typecast_exprt if the type of the symbol_exprt does not equal that +/// represented by `type_char` /// \return symbol_exprt or type-cast symbol_exprt exprt java_bytecode_convert_methodt::variable( const exprt &arg, @@ -239,18 +235,12 @@ exprt java_bytecode_convert_methodt::variable( } /// Returns the member type for a method, based on signature or descriptor -/// \param descriptor -/// descriptor of the method -/// \param signature -/// signature of the method -/// \param class_name -/// string containing the name of the corresponding class -/// \param method_name -/// string containing the name of the method -/// \param message_handler -/// message handler to collect warnings -/// \return -/// the constructed member type +/// \param descriptor: descriptor of the method +/// \param signature: signature of the method +/// \param class_name: string containing the name of the corresponding class +/// \param method_name: string containing the name of the method +/// \param message_handler: message handler to collect warnings +/// \return the constructed member type java_method_typet member_type_lazy( const std::string &descriptor, const optionalt &signature, @@ -308,9 +298,9 @@ java_method_typet member_type_lazy( /// Retrieves the symbol of the lambda method associated with the given /// lambda method handle (bootstrap method). -/// \param lambda_method_handles Vector of lambda method handles (bootstrap +/// \param lambda_method_handles: Vector of lambda method handles (bootstrap /// methods) of the class where the lambda is called -/// \param index Index of the lambda method handle in the vector +/// \param index: Index of the lambda method handle in the vector /// \return Symbol of the lambda method if the method handle has a known type optionalt java_bytecode_convert_methodt::get_lambda_method_symbol( const java_class_typet::java_lambda_method_handlest &lambda_method_handles, @@ -3142,7 +3132,7 @@ irep_idt java_bytecode_convert_methodt::get_static_field( /// Create temporary variables if a write instruction can have undesired side- /// effects. /// \param tmp_var_prefix: The prefix string to use for new temporary variables -/// \param[out] block: The code block the assignment is added to if required. +/// \param [out] block: The code block the assignment is added to if required. /// \param write_type: The enumeration type of the write instruction. /// \param identifier: The identifier of the symbol in the write instruction. void java_bytecode_convert_methodt::save_stack_entries( diff --git a/jbmc/src/java_bytecode/java_bytecode_instrument.cpp b/jbmc/src/java_bytecode/java_bytecode_instrument.cpp index 04954700e3..e55894e462 100644 --- a/jbmc/src/java_bytecode/java_bytecode_instrument.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_instrument.cpp @@ -87,11 +87,11 @@ const std::vector exception_needed_classes = { /// conditional GOTO such that exc_name is thrown when /// cond is met. /// \param cond: condition to be met in order -/// to throw an exception +/// to throw an exception /// \param original_loc: source location in the original program /// \param exc_name: the name of the exception to be thrown /// \return Returns the code initialising the throwing the -/// exception +/// exception code_ifthenelset java_bytecode_instrumentt::throw_exception( const exprt &cond, const source_locationt &original_loc, @@ -135,14 +135,13 @@ code_ifthenelset java_bytecode_instrumentt::throw_exception( return if_code; } - /// Checks whether there is a division by zero /// and throws ArithmeticException if necessary. /// Exceptions are thrown when the `throw_runtime_exceptions` /// flag is set. /// \return Based on the value of the flag `throw_runtime_exceptions`, -/// it returns code that either throws an ArithmeticException -/// or asserts a nonzero denominator. +/// it returns code that either throws an ArithmeticException +/// or asserts a nonzero denominator. codet java_bytecode_instrumentt::check_arithmetic_exception( const exprt &denominator, const source_locationt &original_loc) @@ -172,8 +171,8 @@ codet java_bytecode_instrumentt::check_arithmetic_exception( /// \param idx: index into the array /// \param original_loc: source location in the original code /// \return Based on the value of the flag `throw_runtime_exceptions`, -/// it returns code that either throws an ArrayIndexOutPfBoundsException -/// or emits an assertion checking the array access +/// it returns code that either throws an ArrayIndexOutPfBoundsException +/// or emits an assertion checking the array access codet java_bytecode_instrumentt::check_array_access( const exprt &array_struct, const exprt &idx, @@ -215,8 +214,8 @@ codet java_bytecode_instrumentt::check_array_access( /// \param class2: the super class /// \param original_loc: source location in the original code /// \return Based on the value of the flag `throw_runtime_exceptions`, -/// it returns code that either throws an ClassCastException or emits an -/// assertion checking the subtype relation +/// it returns code that either throws an ClassCastException or emits an +/// assertion checking the subtype relation code_ifthenelset java_bytecode_instrumentt::check_class_cast( const exprt &class1, const exprt &class2, @@ -262,8 +261,8 @@ code_ifthenelset java_bytecode_instrumentt::check_class_cast( /// \param expr: the checked expression /// \param original_loc: source location in the original code /// \return Based on the value of the flag `throw_runtime_exceptions`, -/// it returns code that either throws an NullPointerException or emits an -/// assertion checking the subtype relation +/// it returns code that either throws an NullPointerException or emits an +/// assertion checking the subtype relation codet java_bytecode_instrumentt::check_null_dereference( const exprt &expr, const source_locationt &original_loc) @@ -291,8 +290,8 @@ codet java_bytecode_instrumentt::check_null_dereference( /// \param length: the checked length /// \param original_loc: source location in the original code /// \return Based on the value of the flag `throw_runtime_exceptions`, -/// it returns code that either throws an NegativeArraySizeException -/// or emits an assertion checking the subtype relation +/// it returns code that either throws an NegativeArraySizeException +/// or emits an assertion checking the subtype relation codet java_bytecode_instrumentt::check_array_length( const exprt &length, const source_locationt &original_loc) @@ -463,9 +462,8 @@ void java_bytecode_instrumentt::instrument_code(codet &code) /// Computes the instrumentation for \p expr in the form of /// either assertions or runtime exceptions. -/// \param expr: the expression for which we compute -/// instrumentation -/// \return: The instrumentation for \p expr if required +/// \param expr: the expression for which we compute instrumentation +/// \return The instrumentation for \p expr if required optionalt java_bytecode_instrumentt::instrument_expr(const exprt &expr) { code_blockt result; diff --git a/jbmc/src/java_bytecode/java_bytecode_language.cpp b/jbmc/src/java_bytecode/java_bytecode_language.cpp index 0d7aee9342..c63070ecee 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_language.cpp @@ -43,8 +43,8 @@ Author: Daniel Kroening, kroening@kroening.com #include "load_method_by_regex.h" /// Parse options that are java bytecode specific. -/// \param cmd Command line -/// \param [out] options The options object that will be updated. +/// \param cmd: Command line +/// \param [out] options: The options object that will be updated. void parse_java_language_options(const cmdlinet &cmd, optionst &options) { options.set_option( diff --git a/jbmc/src/java_bytecode/java_bytecode_parse_tree.cpp b/jbmc/src/java_bytecode/java_bytecode_parse_tree.cpp index c031d17154..208ad71832 100644 --- a/jbmc/src/java_bytecode/java_bytecode_parse_tree.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_parse_tree.cpp @@ -92,7 +92,7 @@ void java_bytecode_parse_treet::annotationt::element_value_pairt::output( /// \param annotation_type_name: An irep_idt representing the name of the /// annotation class, e.g. java::java.lang.SuppressWarnings /// \return The first annotation with the given name in annotations if one -/// exists, an empty optionalt otherwise. +/// exists, an empty optionalt otherwise. optionalt java_bytecode_parse_treet::find_annotation( const annotationst &annotations, diff --git a/jbmc/src/java_bytecode/java_bytecode_parser.cpp b/jbmc/src/java_bytecode/java_bytecode_parser.cpp index c6ed74717d..2e05af456f 100644 --- a/jbmc/src/java_bytecode/java_bytecode_parser.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_parser.cpp @@ -1580,7 +1580,7 @@ void java_bytecode_parsert::relement_value_pairs( /// Corresponds to the element_value structure /// Described in Java 8 specification 4.7.16.1 /// https://docs.oracle.com/javase/specs/jvms/se8/html/jvms-4.html#jvms-4.7.16.1 -/// \returns An exprt that represents the particular value of annotations field. +/// \return An exprt that represents the particular value of annotations field. /// This is usually one of: a byte, number of some sort, string, character, /// enum, Class type, array or another annotation. exprt java_bytecode_parsert::get_relement_value() @@ -1949,8 +1949,8 @@ void java_bytecode_parsert::parse_local_variable_type_table(methodt &method) /// Read method handle pointed to from constant pool entry at index, return type /// of method handle and name if lambda function is found. /// \param entry: the constant pool entry of the methodhandle_info structure -/// \returns: the method_handle type of the methodhandle_structure, -/// either for a recognized bootstrap method or for a lambda function +/// \return the method_handle type of the methodhandle_structure, +/// either for a recognized bootstrap method or for a lambda function optionalt java_bytecode_parsert::parse_method_handle(const method_handle_infot &entry) { @@ -1994,7 +1994,7 @@ java_bytecode_parsert::parse_method_handle(const method_handle_infot &entry) /// Read all entries of the `BootstrapMethods` attribute of a class file. /// \param parsed_class: the class representation of the class file that is -/// currently parsed +/// currently parsed void java_bytecode_parsert::read_bootstrapmethods_entry(classt &parsed_class) { u2 num_bootstrap_methods = read_u2(); diff --git a/jbmc/src/java_bytecode/java_class_loader.cpp b/jbmc/src/java_bytecode/java_class_loader.cpp index e80872015e..c7cd32ced4 100644 --- a/jbmc/src/java_bytecode/java_class_loader.cpp +++ b/jbmc/src/java_bytecode/java_class_loader.cpp @@ -103,7 +103,7 @@ static bool is_overlay_class(const java_bytecode_parse_treet::classt &c) /// to find the .class file. /// \param class_loader_limit: Filter to decide whether to load classes /// \param class_name: Name of class to load -/// \returns The list of valid implementations, including overlays +/// \return The list of valid implementations, including overlays /// \remarks /// Allows multiple definitions of the same class to appear on the /// classpath, so long as all but the first definition are marked with the diff --git a/jbmc/src/java_bytecode/java_entry_point.cpp b/jbmc/src/java_bytecode/java_entry_point.cpp index 068df7baed..0ca5804633 100644 --- a/jbmc/src/java_bytecode/java_entry_point.cpp +++ b/jbmc/src/java_bytecode/java_entry_point.cpp @@ -606,7 +606,7 @@ main_function_resultt get_main_symbol( /// (deterministically) set to null. This is a source of underapproximation in /// our approach to test generation, and should perhaps be fixed in the future. /// -/// \returns true if error occurred on entry point search +/// \return true if error occurred on entry point search bool java_entry_point( symbol_table_baset &symbol_table, const irep_idt &main_class, @@ -662,7 +662,7 @@ bool java_entry_point( /// \param assert_uncaught_exceptions: Add an uncaught-exception check /// \param object_factory_parameters: Parameters for creation of arguments /// \param pointer_type_selector: Logic for substituting types of pointers -/// \returns true if error occurred on entry point search, false otherwise +/// \return true if error occurred on entry point search, false otherwise bool generate_java_start_function( const symbolt &symbol, symbol_table_baset &symbol_table, diff --git a/jbmc/src/java_bytecode/java_local_variable_table.cpp b/jbmc/src/java_bytecode/java_local_variable_table.cpp index 18127f2385..544d3500fa 100644 --- a/jbmc/src/java_bytecode/java_local_variable_table.cpp +++ b/jbmc/src/java_bytecode/java_local_variable_table.cpp @@ -270,7 +270,7 @@ static void populate_variable_address_map( /// range of local variable table entries to consider /// \param live_variable_at_address: /// map from bytecode address to table entry (drawn from firstvar-varlimit) -// live at that address +/// live at that address /// \param amap: /// map from bytecode address to instructions, this is the CFG of the java /// method diff --git a/jbmc/src/java_bytecode/java_object_factory.cpp b/jbmc/src/java_bytecode/java_object_factory.cpp index 874150b26b..b6fc6a10bc 100644 --- a/jbmc/src/java_bytecode/java_object_factory.cpp +++ b/jbmc/src/java_bytecode/java_object_factory.cpp @@ -218,7 +218,7 @@ code_assignt java_object_factoryt::get_null_assignment( /// \endcode /// It is illegal to call the function with MAY_UPDATE_IN_PLACE. /// -/// \param[out] assignments: +/// \param [out] assignments: /// A code_blockt where the initialization code will be emitted to. /// \param expr: /// Pointer-typed lvalue expression to initialize. @@ -368,7 +368,7 @@ static mp_integer max_value(const typet &type) /// /// If the structure is not a nondeterministic structure, the call results in /// a precondition violation. -/// \param struct_expr [out]: struct that we initialize +/// \param [out] struct_expr: struct that we initialize /// \param code: block to add pre-requisite declarations (e.g. to allocate a /// data array) /// \param min_nondet_string_length: minimum length of strings to initialize @@ -731,21 +731,16 @@ void java_object_factoryt::gen_nondet_pointer_init( /// // assign `expr` with a suitably casted pointer to new_object /// A * p = &tmp_object /// -/// \param assignments -/// A block of code where we append the generated code. -/// \param lifetime: -/// Lifetime of the allocated objects (AUTOMATIC_LOCAL, STATIC_GLOBAL, or -/// DYNAMIC) -/// \param replacement_pointer -/// The type of the pointer we actually want to to create. -/// \param depth: -/// Number of times that a pointer has been dereferenced from the root of the -/// object tree that we are initializing. -/// \param location: -/// Source location associated with nondet-initialization. -/// \return -/// A symbol expression of type \p replacement_pointer corresponding to a -/// pointer to object `tmp_object` (see above). +/// \param assignments: A block of code where we append the generated code +/// \param lifetime: Lifetime of the allocated objects (AUTOMATIC_LOCAL, +/// STATIC_GLOBAL, or DYNAMIC) +/// \param replacement_pointer: The type of the pointer we actually want to +/// create +/// \param depth: Number of times that a pointer has been dereferenced from the +/// root of the object tree that we are initializing +/// \param location: Source location associated with nondet-initialization +/// \return A symbol expression of type \p replacement_pointer corresponding to +/// a pointer to object `tmp_object` (see above) symbol_exprt java_object_factoryt::gen_nondet_subtype_pointer_init( code_blockt &assignments, lifetimet lifetime, @@ -811,32 +806,23 @@ alternate_casest get_string_input_values_code( /// After initialization calls validation method /// `expr.cproverNondetInitialize()` if it was provided by the user. /// -/// \param assignments: -/// The code block to append the new instructions to. -/// \param expr -/// Struct-typed lvalue expression to initialize. -/// \param is_sub: -/// If true, `expr` is a substructure of a larger object, which in Java -/// necessarily means a base class. -/// \param class_identifier: -/// Name of the parent class. Used to initialize the `@class_identifier` among -/// others. -/// \param skip_classid: -/// If true, skip initializing `@class_identifier`. -/// \param lifetime: -/// Lifetime of the allocated objects (AUTOMATIC_LOCAL, STATIC_GLOBAL, or -/// DYNAMIC) -/// \param struct_type: -/// The type of the struct we are initalizing. -/// \param depth: -/// Number of times that a pointer has been dereferenced from the root of the -/// object tree that we are initializing. -/// \param update_in_place: +/// \param assignments: The code block to append the new instructions to +/// \param expr: Struct-typed lvalue expression to initialize +/// \param is_sub: If true, `expr` is a substructure of a larger object, which +/// in Java necessarily means a base class +/// \param class_identifier: Name of the parent class. Used to initialize the +/// `@class_identifier` among others +/// \param skip_classid: If true, skip initializing `@class_identifier` +/// \param lifetime: Lifetime of the allocated objects (AUTOMATIC_LOCAL, +/// STATIC_GLOBAL, or DYNAMIC) +/// \param struct_type: The type of the struct we are initializing +/// \param depth: Number of times that a pointer has been dereferenced from the +/// root of the object tree that we are initializing +/// \param update_in_place: Enum instance with the following meaning. /// NO_UPDATE_IN_PLACE: initialize `expr` from scratch /// MUST_UPDATE_IN_PLACE: reinitialize an existing object /// MAY_UPDATE_IN_PLACE: invalid input -/// \param location: -/// Source location associated with nondet-initialization. +/// \param location: Source location associated with nondet-initialization void java_object_factoryt::gen_nondet_struct_init( code_blockt &assignments, const exprt &expr, @@ -1181,7 +1167,7 @@ const symbol_exprt java_object_factoryt::gen_nondet_int_init( /// Allocates a fresh array and emits an assignment writing to \p lhs the /// address of the new array. Single-use at the moment, but useful to keep as a /// separate function for downstream branches. -/// \param[out] assignments: +/// \param [out] assignments: /// Code is emitted here. /// \param lhs: /// Symbol to assign the new array structure. @@ -1528,8 +1514,8 @@ void java_object_factoryt::gen_nondet_enum_init( /// The only new one is \p type, which is the type of the object to create. /// /// \return The object created, the \p symbol_table gains any new symbols -/// created, and \p init_code gains any instructions requried to initialize -/// either the returned value or its child objects +/// created, and \p init_code gains any instructions required to initialize +/// either the returned value or its child objects exprt object_factory( const typet &type, const irep_idt base_name, @@ -1591,7 +1577,7 @@ exprt object_factory( /// /// \param expr: /// Lvalue expression to initialize. -/// \param[out] init_code: +/// \param [out] init_code: /// A code block where the initializing assignments will be appended to. /// It gets an instruction sequence to initialize or reinitialize `expr` and /// child objects it refers to. diff --git a/jbmc/src/java_bytecode/java_object_factory_parameters.h b/jbmc/src/java_bytecode/java_object_factory_parameters.h index e01b7175f1..b638250dff 100644 --- a/jbmc/src/java_bytecode/java_object_factory_parameters.h +++ b/jbmc/src/java_bytecode/java_object_factory_parameters.h @@ -24,8 +24,8 @@ struct java_object_factory_parameterst final : public object_factory_parameterst }; /// Parse the java object factory parameters from a given command line -/// \param cmdline Command line -/// \param [out] options The options object that will be updated +/// \param cmdline: Command line +/// \param [out] options: The options object that will be updated void parse_java_object_factory_options( const cmdlinet &cmdline, optionst &options); diff --git a/jbmc/src/java_bytecode/java_root_class.cpp b/jbmc/src/java_bytecode/java_root_class.cpp index 3d33b2b667..9ac91f56f4 100644 --- a/jbmc/src/java_bytecode/java_root_class.cpp +++ b/jbmc/src/java_bytecode/java_root_class.cpp @@ -36,10 +36,10 @@ void java_root_class(symbolt &class_symbol) } /// Adds members for an object of the root class (usually java.lang.Object). -/// \param jlo [out] : object to initialize +/// \param [out] jlo: object to initialize /// \param root_type: type of the root class /// \param class_identifier: class identifier field, generally begins with -/// "java::" prefix. +/// "java::" prefix. void java_root_class_init( struct_exprt &jlo, const struct_typet &root_type, diff --git a/jbmc/src/java_bytecode/java_static_initializers.cpp b/jbmc/src/java_bytecode/java_static_initializers.cpp index 80e230afb6..c023406436 100644 --- a/jbmc/src/java_bytecode/java_static_initializers.cpp +++ b/jbmc/src/java_bytecode/java_static_initializers.cpp @@ -693,14 +693,13 @@ code_ifthenelset get_clinit_wrapper_body( return code_ifthenelset(std::move(check_already_run), std::move(init_body)); } - /// Create static initializer wrappers for all classes that need them. /// \param symbol_table: global symbol table /// \param synthetic_methods: synthetic methods map. Will be extended noting /// that any wrapper belongs to this code, and so `get_clinit_wrapper_body` /// should be used to produce the method body when required. /// \param thread_safe: if true state variables required to make the -/// clinit_wrapper thread safe will be created. +/// clinit_wrapper thread safe will be created. void create_static_initializer_wrappers( symbol_tablet &symbol_table, synthetic_methods_mapt &synthetic_methods, diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp index 2f1c5e980b..ea03ef6ba4 100644 --- a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp +++ b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp @@ -33,7 +33,7 @@ Date: April 2017 #include "java_root_class.h" /// \return tag of a struct prefixed by "java::" or symbolic tag -/// empty string if not symbol or struct +/// empty string if not symbol or struct static irep_idt get_tag(const typet &type) { /// \todo Use follow instead of assuming tag to symbol relationship. @@ -286,7 +286,7 @@ exprt::operandst java_string_library_preprocesst::process_parameters( /// Creates a string_exprt from the input exprt representing a char sequence /// \param expr_to_process: an expression of a type which implements char -/// sequence +/// sequence /// \param loc: location in the source /// \param symbol_table: symbol table /// \param init_code: code block, in which declaration will be added: @@ -297,7 +297,7 @@ exprt::operandst java_string_library_preprocesst::process_parameters( /// cprover_string_content = a->data; /// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ /// \return the processed operand: -/// {content=cprover_string_content, length=cprover_string_length} +/// {content=cprover_string_content, length=cprover_string_length} refined_string_exprt java_string_library_preprocesst::convert_exprt_to_string_exprt( const exprt &expr_to_process, @@ -495,7 +495,7 @@ symbol_exprt java_string_library_preprocesst::fresh_string( /// fresh symbols. /// \param loc: source location /// \param symbol_table: the symbol table -/// \param code [out] : code block to which the declaration is added +/// \param [out] code: code block to which the declaration is added /// \return refined string expr with fresh content and length symbols refined_string_exprt java_string_library_preprocesst::decl_string_expr( const source_locationt &loc, @@ -631,7 +631,7 @@ codet java_string_library_preprocesst::code_return_function_application( /// \param symbol_table: the symbol table /// \param loc: source location /// \param function_id: name of the function containing the array -/// \param code [out] : code block where the declaration gets added +/// \param [out] code: code block where the declaration gets added /// \return created symbol expression exprt make_nondet_infinite_char_array( symbol_table_baset &symbol_table, @@ -664,7 +664,7 @@ exprt make_nondet_infinite_char_array( /// \param array: a character array expression /// \param symbol_table: the symbol table /// \param loc: source location -/// \param code [out] : code block to which declaration and calls get added +/// \param [out] code: code block to which declaration and calls get added void add_pointer_to_array_association( const exprt &pointer, const exprt &array, @@ -698,7 +698,7 @@ void add_pointer_to_array_association( /// \param length: integer expression /// \param symbol_table: the symbol table /// \param loc: source location -/// \param code [out] : code block to which declaration and calls get added +/// \param [out] code: code block to which declaration and calls get added void add_array_to_length_association( const exprt &array, const exprt &length, @@ -729,11 +729,11 @@ void add_array_to_length_association( /// \param pointer: a character pointer expression /// \param length: length of the character sequence pointed by `pointer` /// \param char_set: character set given by a range expression consisting of -/// two characters separated by an hyphen. -/// For instance "a-z" denotes all lower case ascii letters. +/// two characters separated by an hyphen. For instance "a-z" denotes all +/// lower case ascii letters. /// \param symbol_table: the symbol table /// \param loc: source location -/// \param code [out] : code block to which declaration and calls get added +/// \param [out] code: code block to which declaration and calls get added void add_character_set_constraint( const exprt &pointer, const exprt &length, @@ -1179,14 +1179,14 @@ code_blockt java_string_library_preprocesst::make_assign_function_from_call( /// Used to access the values of the arguments of `String.format`. /// \param object: an expression representing a reference to an object /// \param type_name: name of the corresponding primitive type, this can be -/// one of the following: ID_boolean, ID_char, ID_byte, ID_short, ID_int, -/// ID_long, ID_float, ID_double, ID_void +/// one of the following: ID_boolean, ID_char, ID_byte, ID_short, ID_int, +/// ID_long, ID_float, ID_double, ID_void /// \param loc: a location in the source /// \param symbol_table: the symbol table /// \param code: code block to which we are adding some assignments -/// \return An expression contaning a symbol `tmp_type_name` where `type_name` -/// is the given argument (ie. boolean, char etc.). Which represents the -/// primitive value contained in the given object. +/// \return An expression containing a symbol `tmp_type_name` where `type_name` +/// is the given argument (ie. boolean, char etc.). Which represents the +/// primitive value contained in the given object. optionalt java_string_library_preprocesst::get_primitive_value_of_object( const exprt &object, @@ -1439,10 +1439,9 @@ struct_exprt java_string_library_preprocesst::make_argument_for_format( /// \param loc: location in the program_invocation_name /// \param function_id: function the generated code will be used in /// \param symbol_table: symbol table -/// \return Code implementing the Java String.format function. -/// Since the exact class of the arguments is not known, we give as -/// argument to the internal format function a structure containing -/// the different possible types. +/// \return Code implementing the Java String.format function. Since the exact +/// class of the arguments is not known, we give as argument to the internal +// format function a structure containing the different possible types. code_blockt java_string_library_preprocesst::make_string_format_code( const java_method_typet &type, const source_locationt &loc, diff --git a/jbmc/src/java_bytecode/java_types.cpp b/jbmc/src/java_bytecode/java_types.cpp index b4491b6cca..c195efbca3 100644 --- a/jbmc/src/java_bytecode/java_types.cpp +++ b/jbmc/src/java_bytecode/java_types.cpp @@ -90,7 +90,7 @@ reference_typet java_lang_object_type() /// Construct an array pointer type. It is a pointer to a symbol with identifier /// java::array[]. Its ID_element_type is set to the corresponding primitive /// type, or void* for arrays of references. -/// \param subtype Character indicating the type of array +/// \param subtype: Character indicating the type of array reference_typet java_array_type(const char subtype) { std::string subtype_str; @@ -125,7 +125,7 @@ reference_typet java_array_type(const char subtype) } /// Return a const reference to the element type of a given java array type -/// \param array_symbol The java array type +/// \param array_symbol: The java array type const typet &java_array_element_type(const struct_tag_typet &array_symbol) { DATA_INVARIANT( @@ -135,7 +135,7 @@ const typet &java_array_element_type(const struct_tag_typet &array_symbol) } /// Return a non-const reference to the element type of a given java array type -/// \param array_symbol The java array type +/// \param array_symbol: The java array type typet &java_array_element_type(struct_tag_typet &array_symbol) { DATA_INVARIANT( @@ -158,8 +158,8 @@ bool is_java_array_type(const typet &type) } /// Checks whether the given type is a multi-dimensional array pointer type, -// i.e., a pointer to an array type with element type also being a pointer to an -/// array type. +/// i.e., a pointer to an array type with element type also being a pointer to +/// an array type. bool is_multidim_java_array_type(const typet &type) { return is_java_array_type(type) && is_java_array_type(java_array_element_type( @@ -167,9 +167,9 @@ bool is_multidim_java_array_type(const typet &type) } /// See above -/// \param tag Tag of a struct +/// \param tag: Tag of a struct /// \return True if the given string is a Java array tag, i.e., has a prefix -/// of java::array[ +/// of java::array[ bool is_java_array_tag(const irep_idt& tag) { return has_prefix(id2string(tag), "java::array["); @@ -227,7 +227,7 @@ exprt java_bytecode_promotion(const exprt &expr) } /// Take a list of generic type arguments and parse them into the generic type. -/// \param generic_type [out]: The existing generic type to add the information +/// \param [out] generic_type: The existing generic type to add the information /// to /// \param type_arguments: The string representing the generic type arguments /// for a signature. For example `;>` @@ -449,8 +449,8 @@ build_class_name(const std::string &src, const std::string &class_name_prefix) /// \param starting_point: The string position where the opening 'L' we want to /// find the closing ';' for. /// \return The string position corresponding to the matching ';'. For example: -/// LA;, we would return 2. For LA; we would return 7. -/// See unit/java_bytecode/java_util_tests.cpp for more examples. +/// LA;, we would return 2. For LA; we would return 7. +/// See unit/java_bytecode/java_util_tests.cpp for more examples. size_t find_closing_semi_colon_for_reference_type( const std::string src, size_t starting_point) @@ -488,7 +488,7 @@ size_t find_closing_semi_colon_for_reference_type( /// \param src: the string representation as used in the class file /// \param class_name_prefix: name of class to append to generic type /// variables/parameters -/// \returns internal type representation for GOTO programs +/// \return internal type representation for GOTO programs typet java_type_from_string( const std::string &src, const std::string &class_name_prefix) @@ -671,7 +671,7 @@ char java_char_from_type(const typet &type) /// /// For example for `HashMap` a vector with two elements would be returned /// -/// \returns vector of java types representing the generic type variables +/// \return vector of java types representing the generic type variables std::vector java_generic_type_from_string( const std::string &class_name, const std::string &src) @@ -792,10 +792,10 @@ bool is_valid_java_array(const struct_typet &type) /// Compares the types, including checking element types if both types are /// arrays. -/// \param type1 First type to compare -/// \param type2 Second type to compare +/// \param type1: First type to compare +/// \param type2: Second type to compare /// \return True if the types are equal, including elemnt types if they are -/// both arrays +/// both arrays bool equal_java_types(const typet &type1, const typet &type2) { bool arrays_with_same_element_type = true; @@ -868,7 +868,7 @@ void get_dependencies_from_generic_parameters_rec( /// must be loaded but only appear as generic type argument, not as a field /// reference. /// \param signature: the string representation of the signature to analyze -/// \param refs [out]: the set to insert the names of the found dependencies +/// \param [out] refs: the set to insert the names of the found dependencies void get_dependencies_from_generic_parameters( const std::string &signature, std::set &refs) @@ -904,7 +904,7 @@ void get_dependencies_from_generic_parameters( /// used to get information about class dependencies that must be loaded but /// only appear as generic type argument, not as a field reference. /// \param t: the type to analyze -/// \param refs [out]: the set to insert the names of the found dependencies +/// \param [out] refs: the set to insert the names of the found dependencies void get_dependencies_from_generic_parameters( const typet &t, std::set &refs) @@ -946,7 +946,7 @@ java_generic_struct_tag_typet::java_generic_struct_tag_typet( /// Check if this symbol has the given generic type. If yes, return its index /// in the vector of generic types. -/// \param type The parameter type we are looking for. +/// \param type: The parameter type we are looking for. /// \return The index of the type in the vector of generic types. optionalt java_generic_struct_tag_typet::generic_type_index( const java_generic_parametert &type) const diff --git a/jbmc/src/java_bytecode/java_utils.cpp b/jbmc/src/java_bytecode/java_utils.cpp index 82be0b38d8..84e93a839b 100644 --- a/jbmc/src/java_bytecode/java_utils.cpp +++ b/jbmc/src/java_bytecode/java_utils.cpp @@ -188,10 +188,10 @@ dereference_exprt checked_dereference(const exprt &expr, const typet &type) /// /// \param src: the source string to scan /// \param open_pos: the initial position of the opening delimiter from where to -/// start the search +/// start the search /// \param open_char: the opening delimiter /// \param close_char: the closing delimiter -/// \returns the index of the matching corresponding closing delimiter in \p src +/// \return the index of the matching corresponding closing delimiter in \p src size_t find_closing_delimiter( const std::string &src, size_t open_pos, @@ -229,8 +229,8 @@ size_t find_closing_delimiter( /// Add the components in components_to_add to the class denoted by /// class symbol. -/// \param class_symbol The symbol representing the class we want to modify. -/// \param components_to_add The vector with the components we want to add. +/// \param class_symbol: The symbol representing the class we want to modify. +/// \param components_to_add: The vector with the components we want to add. void java_add_components_to_class( symbolt &class_symbol, const struct_union_typet::componentst &components_to_add) @@ -271,7 +271,7 @@ void declare_function( /// \param type: return type of the function /// \param symbol_table: a symbol table /// \return a function application expression representing: -/// `function_name(arguments)` +/// `function_name(arguments)` exprt make_function_application( const irep_idt &function_name, const exprt::operandst &arguments, @@ -302,9 +302,9 @@ irep_idt strip_java_namespace_prefix(const irep_idt &to_strip) /// Strip the package name from a java type, for the type to be /// pretty printed (java::java.lang.Integer -> Integer). -/// \param fqn_java_type The java type we want to pretty print. +/// \param fqn_java_type: The java type we want to pretty print. /// \return The pretty printed type if there was a match of the -// qualifiers, or the type as it was passed otherwise. +/// qualifiers, or the type as it was passed otherwise. std::string pretty_print_java_type(const std::string &fqn_java_type) { std::string result(fqn_java_type); diff --git a/jbmc/src/java_bytecode/java_utils.h b/jbmc/src/java_bytecode/java_utils.h index e58db51594..47eecd809c 100644 --- a/jbmc/src/java_bytecode/java_utils.h +++ b/jbmc/src/java_bytecode/java_utils.h @@ -75,8 +75,8 @@ dereference_exprt checked_dereference(const exprt &expr, const typet &type); /// Add the components in components_to_add to the class denoted /// by class symbol. -/// \param class_symbol The symbol representing the class we want to modify. -/// \param components_to_add The vector with the components we want to add. +/// \param class_symbol: The symbol representing the class we want to modify. +/// \param components_to_add: The vector with the components we want to add. void java_add_components_to_class( symbolt &class_symbol, const struct_union_typet::componentst &components_to_add); diff --git a/jbmc/src/java_bytecode/load_method_by_regex.cpp b/jbmc/src/java_bytecode/load_method_by_regex.cpp index 879eccaa27..727e7f1c4a 100644 --- a/jbmc/src/java_bytecode/load_method_by_regex.cpp +++ b/jbmc/src/java_bytecode/load_method_by_regex.cpp @@ -34,7 +34,7 @@ static std::regex build_regex_from_pattern(const std::string &pattern) /// is, does it have a colon separtor. /// \param pattern: The user provided pattern /// \return True if no descriptor is found (that is, the only : relates to the -/// java:: prefix. +/// java:: prefix. bool does_pattern_miss_descriptor(const std::string &pattern) { const size_t descriptor_index = pattern.rfind(':'); diff --git a/jbmc/src/java_bytecode/mz_zip_archive.h b/jbmc/src/java_bytecode/mz_zip_archive.h index d8caf98c45..88e3456a91 100644 --- a/jbmc/src/java_bytecode/mz_zip_archive.h +++ b/jbmc/src/java_bytecode/mz_zip_archive.h @@ -21,13 +21,13 @@ class mz_zip_archivet final { public: /// Open a zip archive - /// \param filename Path of the zip archive + /// \param filename: Path of the zip archive /// \throw Throws std::runtime_error if file cannot be opened explicit mz_zip_archivet(const std::string &filename); /// Loads a zip buffer - /// \param data pointer to the memory buffer - /// \param size size of the buffer + /// \param data: pointer to the memory buffer + /// \param size: size of the buffer /// \throw Throws std::runtime_error if file cannot be opened mz_zip_archivet(const void *data, size_t size); @@ -43,11 +43,11 @@ public: /// Get number of files in the archive size_t get_num_files(); /// Get file name of nth file in the archive - /// \param index id of the file in the archive + /// \param index: id of the file in the archive /// \return Name of the file in the archive std::string get_filename(size_t index); /// Get contents of nth file in the archive - /// \param index id of the file in the archive + /// \param index: id of the file in the archive /// \throw Throws std::runtime_error if file cannot be extracted /// \return Contents of the file in the archive std::string extract(size_t index); diff --git a/jbmc/src/java_bytecode/remove_exceptions.cpp b/jbmc/src/java_bytecode/remove_exceptions.cpp index 02876b3491..15dbe07b43 100644 --- a/jbmc/src/java_bytecode/remove_exceptions.cpp +++ b/jbmc/src/java_bytecode/remove_exceptions.cpp @@ -260,13 +260,13 @@ void remove_exceptionst::instrument_exception_handler( /// we note that try1{ try2 {} catch2c {} catch2d {}} catch1a() {} catch1b{} /// must catch in the following order: 2c 2d 1a 1b hence the numerical index /// is reversed whereas the letter ordering remains the same. -/// @param stack_catch exception table -/// @param goto_program program being evaluated -/// @param[out] universal_try returns the try block -/// corresponding to the desired exception handler -/// @param[out] universal_catch returns the catch block -/// corresponding to the exception desired exception handler -/// @return the desired exception handler +/// \param stack_catch: exception table +/// \param goto_program: program being evaluated +/// \param [out] universal_try: returns the try block corresponding to the +/// desired exception handler +/// \param [out] universal_catch: returns the catch block corresponding to the +/// exception desired exception handler +/// \return the desired exception handler goto_programt::targett remove_exceptionst::find_universal_exception( const remove_exceptionst::stack_catcht &stack_catch, goto_programt &goto_program, diff --git a/jbmc/src/java_bytecode/remove_instanceof.cpp b/jbmc/src/java_bytecode/remove_instanceof.cpp index 5684f4b1a4..273f8e3fc4 100644 --- a/jbmc/src/java_bytecode/remove_instanceof.cpp +++ b/jbmc/src/java_bytecode/remove_instanceof.cpp @@ -296,7 +296,7 @@ void remove_instanceof( /// \param class_hierarchy: class hierarchy analysis of goto_model's symbol /// table /// \param message_handler: logging output -/// symbols to. +/// symbols to. void remove_instanceof( goto_modelt &goto_model, const class_hierarchyt &class_hierarchy, diff --git a/jbmc/src/java_bytecode/select_pointer_type.cpp b/jbmc/src/java_bytecode/select_pointer_type.cpp index c6cef69079..c932371e08 100644 --- a/jbmc/src/java_bytecode/select_pointer_type.cpp +++ b/jbmc/src/java_bytecode/select_pointer_type.cpp @@ -118,9 +118,9 @@ pointer_typet select_pointer_typet::specialize_generics( /// /// Note that the top of the stacks for T and U create a recursion T -> U, /// U-> T. We want to break it and specialize `T my.gen.t` to `String my.gen.t`. -/// \param parameter_name The name of the generic parameter type we want to have -/// instantiated -/// \param generic_parameter_specialization_map Map of type names to +/// \param parameter_name: The name of the generic parameter type we want to +/// have instantiated +/// \param generic_parameter_specialization_map: Map of type names to /// specialization stack /// \return The first instantiated type for the generic type or nothing if no /// such instantiation exists. @@ -157,12 +157,12 @@ select_pointer_typet::get_recursively_instantiated_type( /// See get_recursively instantiated_type, the additional parameters just track /// the recursion to prevent visiting the same depth again and specify which /// stack depth is analyzed. -/// \param parameter_name The name of the generic parameter type we want to have -/// instantiated -/// \param generic_parameter_specialization_map Map of type names to -/// specialization stack -/// \param visited Tracks the visited parameter names -/// \param depth Stack depth to analyze +/// \param parameter_name: The name of the generic parameter type we want to +/// have instantiated +/// \param generic_parameter_specialization_map: Map of type names to +/// specialization stack +/// \param visited: Tracks the visited parameter names +/// \param depth: Stack depth to analyze /// \return if this type is not a generic type, it is returned as a valid /// instantiation, if nothing can be found at the given depth, en empty /// optional is returned diff --git a/jbmc/unit/java-testing-utils/load_java_class.cpp b/jbmc/unit/java-testing-utils/load_java_class.cpp index 55cecd1281..6288f2cdd7 100644 --- a/jbmc/unit/java-testing-utils/load_java_class.cpp +++ b/jbmc/unit/java-testing-utils/load_java_class.cpp @@ -83,7 +83,7 @@ symbol_tablet load_java_class( /// \param command_line: The command line used to configure the provided /// language /// \return The goto model containing both the functions and the symbol table -/// from loading this class. +/// from loading this class. goto_modelt load_goto_model_from_java_class( const std::string &java_class_name, const std::string &class_path, diff --git a/jbmc/unit/java-testing-utils/require_goto_statements.cpp b/jbmc/unit/java-testing-utils/require_goto_statements.cpp index 232adaabd1..30524fdb80 100644 --- a/jbmc/unit/java-testing-utils/require_goto_statements.cpp +++ b/jbmc/unit/java-testing-utils/require_goto_statements.cpp @@ -19,7 +19,7 @@ Author: Diffblue Ltd. /// Expand value of a function to include all child codets /// \param function_value: The value of the function (e.g. got by looking up /// the function in the symbol table and getting the value) -/// \return: All ID_code statements in the tree rooted at \p function_value +/// \return All ID_code statements in the tree rooted at \p function_value std::vector require_goto_statements::get_all_statements(const exprt &function_value) { @@ -37,7 +37,7 @@ require_goto_statements::get_all_statements(const exprt &function_value) return statements; } -/// \param symbol_table Symbol table for the test +/// \param symbol_table: Symbol table for the test /// \return All codet statements of the __CPROVER_start function const std::vector require_goto_statements::require_entry_point_statements( @@ -60,8 +60,8 @@ require_goto_statements::require_entry_point_statements( /// \param superclass_name: The name of the superclass (if given) /// \param component_name: The name of the component of the superclass that /// \param symbol_table: A symbol table to enable type lookups -/// should be assigned -/// \return: All the assignments to that component. +/// should be assigned +/// \return All the assignments to that component. require_goto_statements::pointer_assignment_locationt require_goto_statements::find_struct_component_assignments( const std::vector &statements, @@ -150,8 +150,8 @@ require_goto_statements::find_struct_component_assignments( } /// Find assignment statements that set this->{component_name} -/// \param statements The statements to look through -/// \param component_name The name of the component whose assignments we are +/// \param statements: The statements to look through +/// \param component_name: The name of the component whose assignments we are /// looking for. /// \return A collection of all non-null assignments to this component /// and, if present, a null assignment. @@ -200,8 +200,8 @@ require_goto_statements::find_this_component_assignment( /// instructions. /// \param pointer_name: The name of the variable /// \param instructions: The instructions to look through -/// \return: A structure that contains the null assignment if found, and a -/// vector of all other assignments +/// \return A structure that contains the null assignment if found, and a +/// vector of all other assignments require_goto_statements::pointer_assignment_locationt require_goto_statements::find_pointer_assignments( const irep_idt &pointer_name, @@ -290,13 +290,13 @@ const code_declt &require_goto_statements::require_declaration_of_name( /// Checks that the component of the structure (possibly inherited from /// the superclass) is assigned an object of the given type. -/// \param structure_name The name the variable -/// \param superclass_name The name of its superclass (if given) -/// \param component_name The name of the field of the superclass -/// \param component_type_name The name of the required type of the field -/// \param typecast_name The name of the type to which the object is cast (if -/// there is a typecast) -/// \param entry_point_instructions The statements to look through +/// \param structure_name: The name the variable +/// \param superclass_name: The name of its superclass (if given) +/// \param component_name: The name of the field of the superclass +/// \param component_type_name: The name of the required type of the field +/// \param typecast_name: The name of the type to which the object is cast (if +/// there is a typecast) +/// \param entry_point_instructions: The statements to look through /// \param symbol_table: A symbol table to enable type lookups /// \return The identifier of the variable assigned to the field const irep_idt &require_goto_statements::require_struct_component_assignment( @@ -379,11 +379,11 @@ const irep_idt &require_goto_statements::require_struct_component_assignment( /// Checks that the array component of the structure (possibly inherited from /// the superclass) is assigned an array with given element type. -/// \param structure_name The name the variable -/// \param superclass_name The name of its superclass (if given) -/// \param array_component_name The name of the array field of the superclass -/// \param array_type_name The type of the array, e.g., java::array[reference] -/// \param entry_point_instructions The statements to look through +/// \param structure_name: The name the variable +/// \param superclass_name: The name of its superclass (if given) +/// \param array_component_name: The name of the array field of the superclass +/// \param array_type_name: The type of the array, e.g., java::array[reference] +/// \param entry_point_instructions: The statements to look through /// \param symbol_table: A symbol table to enable type lookups /// \return The identifier of the variable assigned to the field const irep_idt & @@ -454,8 +454,8 @@ require_goto_statements::require_struct_array_component_assignment( /// Checks that the input argument (of method under test) with given name is /// assigned a single non-null object in the entry point function. -/// \param argument_name Name of the input argument of method under test -/// \param entry_point_statements The statements to look through +/// \param argument_name: Name of the input argument of method under test +/// \param entry_point_statements: The statements to look through /// \return The identifier of the variable assigned to the input argument const irep_idt & require_goto_statements::require_entry_point_argument_assignment( diff --git a/jbmc/unit/java-testing-utils/require_parse_tree.cpp b/jbmc/unit/java-testing-utils/require_parse_tree.cpp index 4b1e3c5d85..2054c13c1b 100644 --- a/jbmc/unit/java-testing-utils/require_parse_tree.cpp +++ b/jbmc/unit/java-testing-utils/require_parse_tree.cpp @@ -13,10 +13,10 @@ Author: Diffblue Ltd. /// Find in the parsed class a specific entry within the /// lambda_method_handle_map with a matching descriptor. Will fail if no /// matching lambda entry found. -/// \param parsed_class the class to inspect -/// \param lambda_method_ref the reference/descriptor of the lambda method +/// \param parsed_class: the class to inspect +/// \param lambda_method_ref: the reference/descriptor of the lambda method /// to which this lambda entry points to, must be unique -/// \param method_type the descriptor the lambda method should have +/// \param method_type: the descriptor the lambda method should have /// \return require_parse_tree::lambda_method_handlet require_parse_tree::require_lambda_entry_for_descriptor( diff --git a/jbmc/unit/java-testing-utils/require_type.cpp b/jbmc/unit/java-testing-utils/require_type.cpp index 9691be2f5a..75fd11f1cf 100644 --- a/jbmc/unit/java-testing-utils/require_type.cpp +++ b/jbmc/unit/java-testing-utils/require_type.cpp @@ -65,7 +65,7 @@ code_typet require_type::require_code(const typet &type) /// accepts a given number of parameters /// \param type: The type to check /// \param num_params: check the the given code_typet expects this -/// number of parameters +/// number of parameters /// \return The type cast to a code_typet code_typet require_type::require_code(const typet &type, const size_t num_params) @@ -88,7 +88,7 @@ java_method_typet require_type::require_java_method(const typet &type) /// accepts a given number of parameters /// \param type: The type to check /// \param num_params: check the the given java_method_typet expects this -/// number of parameters +/// number of parameters /// \return The type cast to a java_method_typet java_method_typet require_type::require_java_method(const typet &type, const size_t num_params) @@ -102,7 +102,7 @@ require_type::require_java_method(const typet &type, const size_t num_params) /// \param function_type: The type of the function /// \param param_name: The name of the parameter /// \return A reference to the parameter structure corresponding to this -/// parameter name. +/// parameter name. code_typet::parametert require_type::require_parameter( const code_typet &function_type, const irep_idt ¶m_name) @@ -223,7 +223,7 @@ java_generic_parametert require_type::require_java_generic_parameter( /// Test a type to ensure it is not a java generics type. /// \param type: The type to test /// \param expect_subtype: Optionally, also test that the subtype of the given -/// type matches this parameter +/// type matches this parameter /// \return The value passed in the first argument const typet &require_type::require_java_non_generic_type( const typet &type, diff --git a/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_initalizers.cpp b/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_initalizers.cpp index 3600e35562..e1359046da 100644 --- a/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_initalizers.cpp +++ b/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_initalizers.cpp @@ -26,7 +26,7 @@ struct test_datat /// Verify that a given descriptor is marked as a constructor in the symbol /// table -/// \param test_data The data to run the test on +/// \param test_data: The data to run the test on void require_is_constructor(const test_datat &test_data) { const symbolt &constructor = @@ -41,7 +41,7 @@ void require_is_constructor(const test_datat &test_data) /// Verify that a given descriptor is not marked as a constructor in the symbol /// table -/// \param test_data The data to run the test on +/// \param test_data: The data to run the test on void require_is_static_initializer(const test_datat &test_data) { REQUIRE( diff --git a/src/analyses/call_graph_helpers.h b/src/analyses/call_graph_helpers.h index 4388c55279..202590e554 100644 --- a/src/analyses/call_graph_helpers.h +++ b/src/analyses/call_graph_helpers.h @@ -55,7 +55,7 @@ std::set get_reaching_functions( /// \param start_functions: set of start functions /// \param n: number of steps to consider /// \return set of functions that can be reached from the start function -/// including the start function +/// including the start function std::set get_functions_reachable_within_n_steps( const call_grapht::directed_grapht &graph, const std::set &start_functions, @@ -67,7 +67,7 @@ std::set get_functions_reachable_within_n_steps( /// \param start_function: single start function /// \param n: number of steps to consider /// \return set of functions that can be reached from the start function -/// including the start function +/// including the start function std::set get_functions_reachable_within_n_steps( const call_grapht::directed_grapht &graph, const irep_idt &start_function, diff --git a/src/analyses/constant_propagator.cpp b/src/analyses/constant_propagator.cpp index 24901da0a9..b4368cfc5c 100644 --- a/src/analyses/constant_propagator.cpp +++ b/src/analyses/constant_propagator.cpp @@ -638,8 +638,8 @@ bool constant_propagator_domaint::merge( /// Attempt to evaluate expression using domain knowledge /// This function changes the expression that is passed into it. /// \param known_values: The constant values under which to evaluate \p expr -/// \param expr The expression to evaluate -/// \param ns The namespace for symbols in the expression +/// \param expr: The expression to evaluate +/// \param ns: The namespace for symbols in the expression /// \return True if the expression is unchanged, false otherwise bool constant_propagator_domaint::partial_evaluate( const valuest &known_values, @@ -659,10 +659,10 @@ bool constant_propagator_domaint::partial_evaluate( /// Attempt to evaluate an expression in all rounding modes. /// /// \param known_values: The constant values under which to evaluate \p expr -/// \param expr The expression to evaluate -/// \param ns The namespace for symbols in the expression +/// \param expr: The expression to evaluate +/// \param ns: The namespace for symbols in the expression /// \return If the result is the same for all rounding modes, change -/// expr to that result and return false. Otherwise, return true. +/// expr to that result and return false. Otherwise, return true. bool constant_propagator_domaint::partial_evaluate_with_all_rounding_modes( const valuest &known_values, exprt &expr, diff --git a/src/analyses/interval_analysis.cpp b/src/analyses/interval_analysis.cpp index 02f61acb23..f748eb2b20 100644 --- a/src/analyses/interval_analysis.cpp +++ b/src/analyses/interval_analysis.cpp @@ -24,8 +24,8 @@ Author: Daniel Kroening, kroening@kroening.com /// conjunction. /// Example: interval [5,10] (for variable "x") translates into conjunction /// 5 <= x && x <= 10. -/// \param interval_analysis Interval domain to be used for variable evaluation. -/// \param goto_function [out] Goto function to be analysed and instrumented. +/// \param interval_analysis: Interval domain to be used for variable evaluation +/// \param [out] goto_function: Goto function to be analysed and instrumented. void instrument_intervals( const ait &interval_analysis, goto_functionst::goto_functiont &goto_function) @@ -89,7 +89,7 @@ void instrument_intervals( /// Initialises the abstract interpretation over interval domain and /// instruments instructions using interval assumptions. -/// \param goto_model [out] Input code as goto_model. +/// \param [out] goto_model: Input code as goto_model. void interval_analysis(goto_modelt &goto_model) { ait interval_analysis; diff --git a/src/analyses/natural_loops.h b/src/analyses/natural_loops.h index d6c3cee7cd..76b82003bd 100644 --- a/src/analyses/natural_loops.h +++ b/src/analyses/natural_loops.h @@ -35,13 +35,13 @@ Author: Georg Weissenbacher, georg@weissenbacher.name /// All instructions in a natural loop are stored into \ref loop_map, keyed by /// their head - the target of the backwards goto jump. /// -/// \tparam P the program representation and needs: -/// [field] instruction which is an iterable of type T. -/// \tparam T iterator of the particular node type, ex: std::list<...>::iterator. -/// The object this iterator holds needs: -/// [function] is_backwards_goto() returning a bool. -/// [function] get_target() which returns an object that needs: -/// [field] location_number which returns an unsigned int. +/// \tparam P: the program representation and needs: +/// * [field] instruction which is an iterable of type T. +/// \tparam T: iterator of the particular node type, e.g. +/// std::list<...>::iterator. The object this iterator holds needs: +/// * [function] is_backwards_goto() returning a bool. +/// * [function] get_target() which returns an object that needs: +/// * [field] location_number which is an unsigned int. template class natural_loops_templatet { diff --git a/src/ansi-c/ansi_c_entry_point.cpp b/src/ansi-c/ansi_c_entry_point.cpp index c7986e1fa1..0cb1b2a9e3 100644 --- a/src/ansi-c/ansi_c_entry_point.cpp +++ b/src/ansi-c/ansi_c_entry_point.cpp @@ -190,7 +190,7 @@ bool ansi_c_entry_point( /// \param symbol_table: The symbol table for the program. The new _start /// function symbol will be added to this table /// \param message_handler: The message handler -/// \param object_factory_parameters configuration parameters for the object +/// \param object_factory_parameters: configuration parameters for the object /// factory /// \return Returns false if the _start method was generated correctly bool generate_ansi_c_start_function( diff --git a/src/ansi-c/c_nondet_symbol_factory.cpp b/src/ansi-c/c_nondet_symbol_factory.cpp index 33ce25271c..79accb5861 100644 --- a/src/ansi-c/c_nondet_symbol_factory.cpp +++ b/src/ansi-c/c_nondet_symbol_factory.cpp @@ -88,8 +88,8 @@ private: /// \param assignments: The code block to add code to /// \param expr: The expression which we are generating a non-determinate value /// for -/// \param depth number of pointers followed so far during initialisation -/// \param recursion_set names of structs seen so far on current pointer chain +/// \param depth: number of pointers followed so far during initialisation +/// \param recursion_set: names of structs seen so far on current pointer chain void symbol_factoryt::gen_nondet_init( code_blockt &assignments, const exprt &expr, @@ -218,7 +218,7 @@ void symbol_factoryt::gen_nondet_array_init( /// \param base_name: The name to use for the symbol created /// \param type: The type for the symbol created /// \param loc: The location to assign to generated code -/// \param object_factory_parameters configuration parameters for the object +/// \param object_factory_parameters: configuration parameters for the object /// factory /// \return Returns the symbol_exprt for the symbol created symbol_exprt c_nondet_symbol_factory( diff --git a/src/ansi-c/c_object_factory_parameters.h b/src/ansi-c/c_object_factory_parameters.h index 5a2460222b..1da85f407e 100644 --- a/src/ansi-c/c_object_factory_parameters.h +++ b/src/ansi-c/c_object_factory_parameters.h @@ -24,8 +24,8 @@ struct c_object_factory_parameterst final : public object_factory_parameterst }; /// Parse the c object factory parameters from a given command line -/// \param cmdline Command line -/// \param [out] options The options object that will be updated +/// \param cmdline: Command line +/// \param [out] options: The options object that will be updated void parse_c_object_factory_options(const cmdlinet &cmdline, optionst &options); #endif diff --git a/src/ansi-c/literals/convert_float_literal.cpp b/src/ansi-c/literals/convert_float_literal.cpp index 56804f46d9..1ff6102a5b 100644 --- a/src/ansi-c/literals/convert_float_literal.cpp +++ b/src/ansi-c/literals/convert_float_literal.cpp @@ -25,7 +25,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "parse_float.h" /// build an expression from a floating-point literal -/// \returns either a constant_exprt or a complex_exprt +/// \return either a constant_exprt or a complex_exprt exprt convert_float_literal(const std::string &src) { parse_floatt parsed_float(src); diff --git a/src/ansi-c/typedef_type.h b/src/ansi-c/typedef_type.h index cc76befbc5..de19004ed6 100644 --- a/src/ansi-c/typedef_type.h +++ b/src/ansi-c/typedef_type.h @@ -11,8 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com #include -/*! \brief A typedef -*/ +/// A typedef class typedef_typet : public typet { public: @@ -32,25 +31,19 @@ public: } }; -/*! \brief Cast a generic typet to a \ref typedef_typet - * - * This is an unchecked conversion. \a type must be known to be \ref - * typedef_typet. - * - * \param type Source type - * \return Object of type \ref typedef_typet - * - * \ingroup gr_std_types -*/ +/// Cast a generic typet to a \ref typedef_typet. This is an unchecked +/// conversion. \a type must be known to be \ref typedef_typet. +/// \param type: Source type +/// \return Object of type \ref typedef_typet +/// \ingroup gr_std_types inline const typedef_typet &to_typedef_type(const typet &type) { PRECONDITION(type.id() == ID_typedef_type); return static_cast(type); } -/*! \copydoc to_typedef_type(const typet &) - * \ingroup gr_std_types -*/ +/// \copydoc to_typedef_type(const typet &) +/// \ingroup gr_std_types inline typedef_typet &to_typedef_type(typet &type) { PRECONDITION(type.id() == ID_typedef_type); diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp index 8900180567..09b2fd8839 100644 --- a/src/cbmc/bmc.cpp +++ b/src/cbmc/bmc.cpp @@ -495,7 +495,7 @@ safety_checkert::resultt bmct::stop_on_fail(prop_convt &prop_conv) /// large equation for the whole program or an equation per path /// \param opts: command-line options affecting BMC /// \param model: provides goto function bodies and the symbol table, perhaps -// creating those function bodies on demand. +/// creating those function bodies on demand. /// \param ui: user-interface mode (plain text, XML output, JSON output, ...) /// \param driver_configure_bmc: function provided by the driver program, /// which applies driver-specific configuration to a bmct before running. diff --git a/src/cpp/cpp_typecheck_destructor.cpp b/src/cpp/cpp_typecheck_destructor.cpp index 143861274e..e9dde78f82 100644 --- a/src/cpp/cpp_typecheck_destructor.cpp +++ b/src/cpp/cpp_typecheck_destructor.cpp @@ -49,8 +49,6 @@ void cpp_typecheckt::default_dtor( } /// produces destructor code for a class object -/// -/// Note: codet cpp_typecheckt::dtor(const symbolt &symbol) { assert(symbol.type.id()==ID_struct || diff --git a/src/goto-analyzer/static_simplifier.cpp b/src/goto-analyzer/static_simplifier.cpp index 7bf82c7723..8bc555d88e 100644 --- a/src/goto-analyzer/static_simplifier.cpp +++ b/src/goto-analyzer/static_simplifier.cpp @@ -25,7 +25,7 @@ Author: Martin Brain, martin.brain@cs.ox.ac.uk /// \param options: the parsed user options /// \param message_handler: the system message handler /// \param out: output stream for the simplified program -/// \return: false on success with the domain printed to out +/// \return false on success with the domain printed to out bool static_simplifier( goto_modelt &goto_model, const ai_baset &ai, diff --git a/src/goto-analyzer/static_verifier.cpp b/src/goto-analyzer/static_verifier.cpp index b21a2e7984..a22d05e7ec 100644 --- a/src/goto-analyzer/static_verifier.cpp +++ b/src/goto-analyzer/static_verifier.cpp @@ -230,7 +230,7 @@ static void static_verifier_console( /// \param options: the parsed user options /// \param message_handler: the system message handler /// \param out: output stream for the printing -/// \return: false on success with the domain printed to out +/// \return false on success with the domain printed to out bool static_verifier( const goto_modelt &goto_model, const ai_baset &ai, diff --git a/src/goto-cc/compile.h b/src/goto-cc/compile.h index a423e356cf..442d8bdad5 100644 --- a/src/goto-cc/compile.h +++ b/src/goto-cc/compile.h @@ -81,8 +81,8 @@ public: /// \brief `__CPROVER_...` macros written to object files and their arities /// /// \return A mapping from every `__CPROVER` macro that this compiler - /// wrote to one or more object files, to how many parameters that - /// `__CPROVER` macro has. + /// wrote to one or more object files, to how many parameters that + /// `__CPROVER` macro has. void cprover_macro_arities(std::map &cprover_macros) const { diff --git a/src/goto-cc/hybrid_binary.h b/src/goto-cc/hybrid_binary.h index 3b5ac97bcb..054218d35a 100644 --- a/src/goto-cc/hybrid_binary.h +++ b/src/goto-cc/hybrid_binary.h @@ -19,11 +19,10 @@ Date: May 2018 #include /// \brief Merges a goto binary into an object file (e.g. ELF) -/// \param compiler_or_linker The name of the gcc or ld executable, -/// used to deduce the name of objcopy -/// \param goto_binary_file The file name of the goto binary -/// \param output_file The name of the object file; the result is -/// stored here. +/// \param compiler_or_linker: The name of the gcc or ld executable, used to +/// deduce the name of objcopy +/// \param goto_binary_file: The file name of the goto binary +/// \param output_file: The name of the object file; the result is stored here. int hybrid_binary( const std::string &compiler_or_linker, const std::string &goto_binary_file, diff --git a/src/goto-cc/linker_script_merge.h b/src/goto-cc/linker_script_merge.h index a6949cf756..8ab80fa0ac 100644 --- a/src/goto-cc/linker_script_merge.h +++ b/src/goto-cc/linker_script_merge.h @@ -157,11 +157,11 @@ protected: /// converted to `foo` whose type is `char*`. int pointerize_linker_defined_symbols(goto_modelt &, const linker_valuest &); - /// \param expr an expr whose subexpressions may need to be pointerized - /// \param to_pointerize The symbols that are contained in the subexpressions - /// that we will pointerize. - /// \param linker_values the names of symbols defined in linker scripts. - /// \param ns a namespace to look up types. + /// \param expr: an expr whose subexpressions may need to be pointerized + /// \param to_pointerize: The symbols that are contained in the subexpressions + /// that we will pointerize. + /// \param linker_values: the names of symbols defined in linker scripts. + /// \param ns: a namespace to look up types. /// /// The subexpressions that we pointerize should be in one-to-one /// correspondence with the symbols in `to_pointerize`. Every time we @@ -195,13 +195,12 @@ protected: /// `linker_values` map. The error messages of this function describe what it /// means for this constraint to be violated. /// - /// \param linker_defined_symbols the list of symbols that were extern with no - /// value in the goto-program) - /// \param linker_values map from the names of linker-defined symbols from - /// the object file, to synthesized values for those - /// linker symbols. - /// \return `1` if there is some mismatch between the list and map, `0` - /// if everything is OK. + /// \param linker_defined_symbols: the list of symbols that were extern with + /// no value in the goto-program + /// \param linker_values: map from the names of linker-defined symbols from + /// the object file, to synthesized values for those linker symbols. + /// \return `1` if there is some mismatch between the list and map, `0` if + /// everything is OK. int goto_and_object_mismatch( const std::list &linker_defined_symbols, const linker_valuest &linker_values); diff --git a/src/goto-instrument/aggressive_slicer.h b/src/goto-instrument/aggressive_slicer.h index 6b8fe3fc42..d9e544b343 100644 --- a/src/goto-instrument/aggressive_slicer.h +++ b/src/goto-instrument/aggressive_slicer.h @@ -56,8 +56,8 @@ public: /// \brief Adds a list of functions to the set of functions for the aggressive /// slicer to preserve - /// \param function_list: a list of functions in form - /// std::list, as returned by get_cmdline_option. + /// \param function_list: a list of functions in form std::list, + /// as returned by get_cmdline_option. void preserve_functions(const std::list &function_list) { for(const auto &f : function_list) @@ -86,7 +86,7 @@ private: /// according to the configuration parameters set in the aggressive /// slicer, i.e., shortest path between two functions, or all direct paths. /// Inserts functions to preserve into the functions_to_keep set - /// \param destination_function name of destination function for slice + /// \param destination_function: name of destination function for slice void note_functions_to_keep(const irep_idt &destination_function); /// \brief Finds all functions that contain a property, diff --git a/src/goto-instrument/cover.cpp b/src/goto-instrument/cover.cpp index a2d6d74850..3dd401dc74 100644 --- a/src/goto-instrument/cover.cpp +++ b/src/goto-instrument/cover.cpp @@ -28,7 +28,7 @@ Date: May 2016 /// \param goto_program: the goto program /// \param instrumenters: the instrumenters /// \param mode: mode of the function to instrument (for instance ID_C or -/// ID_java) +/// ID_java) /// \param message_handler: a message handler void instrument_cover_goals( goto_programt &goto_program, diff --git a/src/goto-instrument/cover_basic_blocks.h b/src/goto-instrument/cover_basic_blocks.h index 607acf9b9a..1a205a9f0d 100644 --- a/src/goto-instrument/cover_basic_blocks.h +++ b/src/goto-instrument/cover_basic_blocks.h @@ -22,19 +22,19 @@ class cover_blocks_baset { public: virtual ~cover_blocks_baset() = default; - /// \param t a goto instruction - /// \return the block number of the block - /// the given goto instruction is part of + /// \param t: a goto instruction + /// \return the block number of the block that the given goto instruction is + // part of virtual std::size_t block_of(goto_programt::const_targett t) const = 0; - /// \param block_nr a block number - /// \return the instruction selected for + /// \param block_nr: a block number + /// \return the instruction selected for /// instrumentation representative of the given block virtual optionalt instruction_of(std::size_t block_nr) const = 0; - /// \param block_nr a block number - /// \return the source location selected for + /// \param block_nr: a block number + /// \return the source location selected for /// instrumentation representative of the given block virtual const source_locationt & source_location_of(std::size_t block_nr) const = 0; @@ -43,8 +43,8 @@ public: virtual void output(std::ostream &out) const = 0; /// Output warnings about ignored blocks - /// \param goto_program The goto program - /// \param message_handler The message handler + /// \param goto_program: The goto program + /// \param message_handler: The message handler virtual void report_block_anomalies( const goto_programt &goto_program, message_handlert &message_handler) @@ -60,26 +60,26 @@ class cover_basic_blockst final : public cover_blocks_baset public: explicit cover_basic_blockst(const goto_programt &_goto_program); - /// \param t a goto instruction + /// \param t: a goto instruction /// \return the block number of the block /// the given goto instruction is part of std::size_t block_of(goto_programt::const_targett t) const override; - /// \param block_nr a block number - /// \return the instruction selected for + /// \param block_nr: a block number + /// \return the instruction selected for /// instrumentation representative of the given block optionalt instruction_of(std::size_t block_nr) const override; - /// \param block_nr a block number - /// \return the source location selected for + /// \param block_nr: a block number + /// \return the source location selected for /// instrumentation representative of the given block const source_locationt & source_location_of(std::size_t block_nr) const override; /// Output warnings about ignored blocks - /// \param goto_program The goto program - /// \param message_handler The message handler + /// \param goto_program: The goto program + /// \param message_handler: The message handler void report_block_anomalies( const goto_programt &goto_program, message_handlert &message_handler) override; @@ -133,16 +133,16 @@ private: public: explicit cover_basic_blocks_javat(const goto_programt &_goto_program); - /// \param t a goto instruction + /// \param t: a goto instruction /// \return block number the given goto instruction is part of std::size_t block_of(goto_programt::const_targett t) const override; - /// \param block_number a block number + /// \param block_number: a block number /// \return first instruction of the given block optionalt instruction_of(std::size_t block_number) const override; - /// \param block_number a block number + /// \param block_number: a block number /// \return source location corresponding to the given block const source_locationt & source_location_of(std::size_t block_number) const override; diff --git a/src/goto-instrument/cover_filter.cpp b/src/goto-instrument/cover_filter.cpp index f3c824cd8f..2e3e46720b 100644 --- a/src/goto-instrument/cover_filter.cpp +++ b/src/goto-instrument/cover_filter.cpp @@ -16,7 +16,7 @@ Author: Peter Schrammel /// Filter out functions that are not considered provided by the user /// \param identifier: a function name /// \param goto_function: a goto function -/// \return: returns true if function is considered user-provided +/// \return returns true if function is considered user-provided bool internal_functions_filtert::operator()( const irep_idt &identifier, const goto_functionst::goto_functiont &goto_function) const @@ -46,7 +46,7 @@ bool internal_functions_filtert::operator()( /// Filter functions whose name match the regex /// \param identifier: a function name /// \param goto_function: a goto function -/// \return: returns true if the function name matches +/// \return returns true if the function name matches bool include_pattern_filtert::operator()( const irep_idt &identifier, const goto_functionst::goto_functiont &goto_function) const @@ -63,7 +63,7 @@ bool include_pattern_filtert::operator()( /// These criteria are arbitrarily chosen. /// \param identifier: a function name /// \param goto_function: a goto function -/// \return: returns true if non-trivial +/// \return returns true if non-trivial bool trivial_functions_filtert::operator()( const irep_idt &identifier, const goto_functionst::goto_functiont &goto_function) const diff --git a/src/goto-instrument/nondet_static.cpp b/src/goto-instrument/nondet_static.cpp index c786d848ef..e42ac41903 100644 --- a/src/goto-instrument/nondet_static.cpp +++ b/src/goto-instrument/nondet_static.cpp @@ -24,10 +24,10 @@ Date: November 2011 #include /// See the return. -/// \param symbol_expr The symbol expression to analyze. -/// \param ns Namespace for resolving type information +/// \param symbol_expr: The symbol expression to analyze. +/// \param ns: Namespace for resolving type information /// \return True if the symbol expression holds a static symbol which can be -/// nondeterministically initialized, false otherwise. +/// nondeterministically initialized, false otherwise. bool is_nondet_initializable_static( const symbol_exprt &symbol_expr, const namespacet &ns) @@ -65,9 +65,9 @@ bool is_nondet_initializable_static( /// Iterates over instructions in the specified function and replaces all values /// assigned to nondet-initializable static variables with nondeterministic /// values. -/// \param ns Namespace for resolving type information. -/// \param [out] goto_functions Existing goto-functions to be updated. -/// \param fct_name Name of the goto-function to be updated. +/// \param ns: Namespace for resolving type information. +/// \param [out] goto_functions: Existing goto-functions to be updated. +/// \param fct_name: Name of the goto-function to be updated. void nondet_static( const namespacet &ns, goto_functionst &goto_functions, @@ -113,8 +113,8 @@ void nondet_static( /// Nondeterministically initializes global scope variables in /// CPROVER_initialize function. -/// \param ns Namespace for resolving type information. -/// \param [out] goto_functions Existing goto-functions to be updated. +/// \param ns: Namespace for resolving type information. +/// \param [out] goto_functions: Existing goto-functions to be updated. void nondet_static( const namespacet &ns, goto_functionst &goto_functions) @@ -129,7 +129,7 @@ void nondet_static( /// scope variables, except for constants (such as string literals, final /// fields) and internal variables (such as CPROVER and symex variables, /// language specific internal variables). -/// \param [out] goto_model Existing goto-model to be updated. +/// \param [out] goto_model: Existing goto-model to be updated. void nondet_static(goto_modelt &goto_model) { const namespacet ns(goto_model.symbol_table); diff --git a/src/goto-instrument/reachability_slicer.cpp b/src/goto-instrument/reachability_slicer.cpp index 7429162949..73e8c3a219 100644 --- a/src/goto-instrument/reachability_slicer.cpp +++ b/src/goto-instrument/reachability_slicer.cpp @@ -30,8 +30,8 @@ Author: Daniel Kroening, kroening@kroening.com /// Get the set of nodes that correspond to the given criterion, or that can /// appear in concurrent execution. None of these should be sliced away so /// they are used as a basis for the search. -/// \param is_threaded Instructions that might be executed concurrently -/// \param criterion The criterion we care about +/// \param is_threaded: Instructions that might be executed concurrently +/// \param criterion: The criterion we care about std::vector reachability_slicert::get_sources( const is_threadedt &is_threaded, @@ -160,8 +160,8 @@ void reachability_slicert::backward_inwards_walk_from( /// goto program, starting from the nodes corresponding to the criterion and /// the instructions that might be executed concurrently. Set reaches_assertion /// to true for every instruction visited. -/// \param is_threaded Instructions that might be executed concurrently -/// \param criterion the criterion we are trying to hit +/// \param is_threaded: Instructions that might be executed concurrently +/// \param criterion: the criterion we are trying to hit void reachability_slicert::fixedpoint_to_assertions( const is_threadedt &is_threaded, const slicing_criteriont &criterion) @@ -298,8 +298,8 @@ void reachability_slicert::forward_inwards_walk_from( /// goto program, starting from the nodes corresponding to the criterion and /// the instructions that might be executed concurrently. Set reaches_assertion /// to true for every instruction visited. -/// \param is_threaded Instructions that might be executed concurrently -/// \param criterion the criterion we are trying to hit +/// \param is_threaded: Instructions that might be executed concurrently +/// \param criterion: the criterion we are trying to hit void reachability_slicert::fixedpoint_from_assertions( const is_threadedt &is_threaded, const slicing_criteriont &criterion) @@ -344,10 +344,10 @@ void reachability_slicert::slice(goto_functionst &goto_functions) /// Perform reachability slicing on goto_model, with respect to the /// criterion given by all properties. -/// \param goto_model Goto program to slice -/// \param include_forward_reachability Determines if only instructions -/// from which the criterion is reachable should be kept (false) or also -/// those reachable from the criterion (true) +/// \param goto_model: Goto program to slice +/// \param include_forward_reachability: Determines if only instructions +/// from which the criterion is reachable should be kept (false) or also +/// those reachable from the criterion (true) void reachability_slicer( goto_modelt &goto_model, const bool include_forward_reachability) @@ -358,12 +358,12 @@ void reachability_slicer( } /// Perform reachability slicing on goto_model for selected properties. -/// \param goto_model Goto program to slice -/// \param properties The properties relevant for the slicing (i.e. starting -/// point for the search in the cfg) -/// \param include_forward_reachability Determines if only instructions -/// from which the criterion is reachable should be kept (false) or also -/// those reachable from the criterion (true) +/// \param goto_model: Goto program to slice +/// \param properties: The properties relevant for the slicing (i.e. starting +/// point for the search in the cfg) +/// \param include_forward_reachability: Determines if only instructions +/// from which the criterion is reachable should be kept (false) or also +/// those reachable from the criterion (true) void reachability_slicer( goto_modelt &goto_model, const std::list &properties, @@ -375,10 +375,10 @@ void reachability_slicer( } /// Perform reachability slicing on goto_model for selected functions. -/// \param goto_model Goto program to slice -/// \param functions_list The functions relevant for the slicing (i.e. starting -/// point for the search in the CFG). Anything that is reachable in the CFG -/// starting from these functions will be kept. +/// \param goto_model: Goto program to slice +/// \param functions_list: The functions relevant for the slicing (i.e. starting +/// point for the search in the CFG). Anything that is reachable in the CFG +/// starting from these functions will be kept. void function_path_reachability_slicer( goto_modelt &goto_model, const std::list &functions_list) @@ -400,7 +400,7 @@ void function_path_reachability_slicer( /// Perform reachability slicing on goto_model, with respect to criterion /// comprising all properties. Only instructions from which the criterion /// is reachable will be kept. -/// \param goto_model Goto program to slice +/// \param goto_model: Goto program to slice void reachability_slicer(goto_modelt &goto_model) { reachability_slicer(goto_model, false); @@ -408,9 +408,9 @@ void reachability_slicer(goto_modelt &goto_model) /// Perform reachability slicing on goto_model for selected properties. Only /// instructions from which the criterion is reachable will be kept. -/// \param goto_model Goto program to slice -/// \param properties The properties relevant for the slicing (i.e. starting -/// point for the search in the cfg) +/// \param goto_model: Goto program to slice +/// \param properties: The properties relevant for the slicing (i.e. starting +/// point for the search in the cfg) void reachability_slicer( goto_modelt &goto_model, const std::list &properties) diff --git a/src/goto-instrument/splice_call.cpp b/src/goto-instrument/splice_call.cpp index a09af770f2..a70903745d 100644 --- a/src/goto-instrument/splice_call.cpp +++ b/src/goto-instrument/splice_call.cpp @@ -11,7 +11,7 @@ Date: July 2017 /// \file /// Prepend a nullary call to another function -// useful for context/ environment setting in arbitrary nodes +/// useful for context/ environment setting in arbitrary nodes #include "splice_call.h" diff --git a/src/goto-programs/class_identifier.cpp b/src/goto-programs/class_identifier.cpp index d247583af1..bfed8ffbb0 100644 --- a/src/goto-programs/class_identifier.cpp +++ b/src/goto-programs/class_identifier.cpp @@ -74,10 +74,10 @@ exprt get_class_identifier_field( /// If expr has its components filled in then sets the `@class_identifier` /// member of the struct /// \remarks Follows through base class members until it gets to the object -/// type that contains the `@class_identifier` member +/// type that contains the `@class_identifier` member /// \param expr: An expression that represents a struct /// \param ns: The namespace used to resolve symbol references in the type of -/// the struct +/// the struct /// \param class_type: A symbol whose identifier is the name of the class void set_class_identifier( struct_exprt &expr, diff --git a/src/goto-programs/generate_function_bodies.cpp b/src/goto-programs/generate_function_bodies.cpp index 5e10607f65..c7d45a3803 100644 --- a/src/goto-programs/generate_function_bodies.cpp +++ b/src/goto-programs/generate_function_bodies.cpp @@ -330,8 +330,7 @@ public: }; /// Create the type that actually generates the functions. -/// \see generate_function_bodies for the syntax of the options -/// parameter +/// \see generate_function_bodies for the syntax of the options parameter std::unique_ptr generate_function_bodies_factory( const std::string &options, const symbol_tablet &symbol_table, @@ -446,11 +445,11 @@ std::unique_ptr generate_function_bodies_factory( /// /// nondet-return: return nondet for non-void functions /// -/// \param functions_regex Specifies the functions whose body should -/// be generated -/// \param generate_function_body Specifies what kind of body to generate -/// \param model The goto-model in which to generate the function bodies -/// \param message_handler Destination for status/warning messages +/// \param functions_regex: Specifies the functions whose body should be +/// generated +/// \param generate_function_body: Specifies what kind of body to generate +/// \param model: The goto-model in which to generate the function bodies +/// \param message_handler: Destination for status/warning messages void generate_function_bodies( const std::regex &functions_regex, const generate_function_bodiest &generate_function_body, diff --git a/src/goto-programs/generate_function_bodies.h b/src/goto-programs/generate_function_bodies.h index 29c93545ea..c909bb4bdd 100644 --- a/src/goto-programs/generate_function_bodies.h +++ b/src/goto-programs/generate_function_bodies.h @@ -26,9 +26,9 @@ protected: /// Produce a body for the passed function /// At this point the body of function is always empty, /// and all function parameters have identifiers - /// \param function whose body to generate - /// \param symbol_table of the current goto program - /// \param function_name Identifier of function + /// \param function: whose body to generate + /// \param symbol_table: of the current goto program + /// \param function_name: Identifier of function virtual void generate_function_body_impl( goto_functiont &function, const symbol_tablet &symbol_table, @@ -39,9 +39,9 @@ public: /// Replace the function body with one based on the replace_function_body /// class being used. - /// \param function whose body to replace - /// \param symbol_table of the current goto program - /// \param function_name Identifier of function + /// \param function: whose body to replace + /// \param symbol_table: of the current goto program + /// \param function_name: Identifier of function void generate_function_body( goto_functiont &function, symbol_tablet &symbol_table, diff --git a/src/goto-programs/goto_trace.cpp b/src/goto-programs/goto_trace.cpp index 97ecb3467d..629a9aa0fa 100644 --- a/src/goto-programs/goto_trace.cpp +++ b/src/goto-programs/goto_trace.cpp @@ -351,10 +351,10 @@ bool is_index_member_symbol(const exprt &src) } /// \brief show a compact variant of the goto trace on the console -/// \param out the output stream -/// \param ns the namespace -/// \param goto_trace the trace to be shown -/// \param options any options, e.g., numerical representation +/// \param out: the output stream +/// \param ns: the namespace +/// \param goto_trace: the trace to be shown +/// \param options: any options, e.g., numerical representation void show_compact_goto_trace( messaget::mstreamt &out, const namespacet &ns, diff --git a/src/goto-programs/lazy_goto_model.h b/src/goto-programs/lazy_goto_model.h index 0db373d55e..61b623c63a 100644 --- a/src/goto-programs/lazy_goto_model.h +++ b/src/goto-programs/lazy_goto_model.h @@ -146,7 +146,7 @@ public: /// \param handler: An object that defines the handlers /// \param options: The options passed to process_goto_functions /// \param message_handler: The message_handler to use for logging - /// \tparam THandler a type that defines methods process_goto_function and + /// \tparam THandler: a type that defines methods process_goto_function and /// process_goto_functions template static lazy_goto_modelt from_handler_object( @@ -196,7 +196,7 @@ public: /// load new functions, it has let it go. /// Before freezing the functions all module-level passes are run /// \param model: The lazy_goto_modelt to freeze - /// \returns The frozen goto_modelt or an empty optional if freezing fails + /// \return The frozen goto_modelt or an empty optional if freezing fails static std::unique_ptr process_whole_model_and_freeze( lazy_goto_modelt &&model) { diff --git a/src/goto-programs/link_to_library.cpp b/src/goto-programs/link_to_library.cpp index 3559b36ae5..1672308593 100644 --- a/src/goto-programs/link_to_library.cpp +++ b/src/goto-programs/link_to_library.cpp @@ -15,11 +15,11 @@ Author: Daniel Kroening, kroening@kroening.com #include "goto_convert_functions.h" /// Complete missing function definitions using the \p library. -/// \param goto_model goto model that may contain function calls and symbols +/// \param goto_model: goto model that may contain function calls and symbols /// with missing function bodies -/// \param message_handler message handler to report library processing +/// \param message_handler: message handler to report library processing /// problems -/// \param library generator function that produces function definitions for a +/// \param library: generator function that produces function definitions for a /// given set of symbol names that have no body. void link_to_library( goto_modelt &goto_model, @@ -36,13 +36,13 @@ void link_to_library( } /// Complete missing function definitions using the \p library. -/// \param symbol_table symbol table that may contain symbols with missing +/// \param symbol_table: symbol table that may contain symbols with missing /// function bodies -/// \param goto_functions goto functions that may contain function calls with +/// \param goto_functions: goto functions that may contain function calls with /// missing function bodies -/// \param message_handler message handler to report library processing +/// \param message_handler: message handler to report library processing /// problems -/// \param library generator function that produces function definitions for a +/// \param library: generator function that produces function definitions for a /// given set of symbol names that have no body. void link_to_library( symbol_tablet &symbol_table, diff --git a/src/goto-programs/read_goto_binary.cpp b/src/goto-programs/read_goto_binary.cpp index 66aa9f308c..ee714c3762 100644 --- a/src/goto-programs/read_goto_binary.cpp +++ b/src/goto-programs/read_goto_binary.cpp @@ -28,9 +28,9 @@ Author: #include "osx_fat_reader.h" /// \brief Read a goto binary from a file, but do not update \ref config -/// \param filename the file name of the goto binary -/// \param dest the goto model returned -/// \param message_handler for diagnostics +/// \param filename: the file name of the goto binary +/// \param dest: the goto model returned +/// \param message_handler: for diagnostics /// \deprecated Use read_goto_binary(file, message_handler) instead /// \return true on failure, false on success bool read_goto_binary( @@ -43,8 +43,8 @@ bool read_goto_binary( } /// \brief Read a goto binary from a file, but do not update \ref config -/// \param filename the file name of the goto binary -/// \param message_handler for diagnostics +/// \param filename: the file name of the goto binary +/// \param message_handler: for diagnostics /// \return goto model on success, {} on failure optionalt read_goto_binary(const std::string &filename, message_handlert &message_handler) @@ -61,10 +61,10 @@ read_goto_binary(const std::string &filename, message_handlert &message_handler) } /// \brief Read a goto binary from a file, but do not update \ref config -/// \param filename the file name of the goto binary -/// \param symbol_table the symbol table from the goto binary -/// \param goto_functions the goto functions from the goto binary -/// \param message_handler for diagnostics +/// \param filename: the file name of the goto binary +/// \param symbol_table: the symbol table from the goto binary +/// \param goto_functions: the goto functions from the goto binary +/// \param message_handler: for diagnostics /// \return true on failure, false on success bool read_goto_binary( const std::string &filename, @@ -227,9 +227,9 @@ bool is_goto_binary(const std::string &filename) } /// \brief reads an object file, and also updates config -/// \param file_name file name of the goto binary -/// \param dest the goto model returned -/// \param message_handler for diagnostics +/// \param file_name: file name of the goto binary +/// \param dest: the goto model returned +/// \param message_handler: for diagnostics /// \return true on error, false otherwise bool read_object_and_link( const std::string &file_name, diff --git a/src/goto-programs/remove_const_function_pointers.cpp b/src/goto-programs/remove_const_function_pointers.cpp index df6d9c9107..3b3e51c43b 100644 --- a/src/goto-programs/remove_const_function_pointers.cpp +++ b/src/goto-programs/remove_const_function_pointers.cpp @@ -47,7 +47,7 @@ remove_const_function_pointerst::remove_const_function_pointerst( /// variations within. /// \param base_expression: The function call through a function pointer /// \param out_functions: The functions that (symbols of type ID_code) the base -/// expression could take. +/// expression could take. /// \return Returns true if it was able to resolve the call, false if not. If it /// returns true, out_functions will be populated by all the possible values /// the function pointer could be. diff --git a/src/goto-programs/remove_function_pointers.cpp b/src/goto-programs/remove_function_pointers.cpp index e0c5a47c53..004d868b44 100644 --- a/src/goto-programs/remove_function_pointers.cpp +++ b/src/goto-programs/remove_function_pointers.cpp @@ -50,9 +50,9 @@ public: /// Replace a call to a dynamic function at location /// target in the given goto-program by a case-split /// over a given set of functions - /// \param goto_program The goto program that contains target - /// \param target location with function call with function pointer - /// \param functions The set of functions to consider + /// \param goto_program: The goto program that contains target + /// \param target: location with function call with function pointer + /// \param functions: The set of functions to consider void remove_function_pointer( goto_programt &goto_program, goto_programt::targett target, @@ -75,8 +75,8 @@ protected: /// Replace a call to a dynamic function at location /// target in the given goto-program by determining /// functions that have a compatible signature - /// \param goto_program The goto program that contains target - /// \param target location with function call with function pointer + /// \param goto_program: The goto program that contains target + /// \param target: location with function call with function pointer void remove_function_pointer( goto_programt &goto_program, goto_programt::targett target); diff --git a/src/goto-programs/remove_skip.cpp b/src/goto-programs/remove_skip.cpp index 58a2ec3c13..5b96f34bfd 100644 --- a/src/goto-programs/remove_skip.cpp +++ b/src/goto-programs/remove_skip.cpp @@ -15,12 +15,12 @@ Author: Daniel Kroening, kroening@kroening.com /// Determine whether the instruction is semantically equivalent to a skip /// (no-op). This includes a skip, but also if(false) goto ..., goto next; /// next: ..., and (void)0. -/// \param body goto program containing the instruction -/// \param it instruction iterator that is tested for being a skip (or -/// equivalent) -/// \param ignore_labels If the caller takes care of moving labels, then even -/// skip statements carrying labels can be treated as skips (even though they -/// may carry key information such as error labels). +/// \param body: goto program containing the instruction +/// \param it: instruction iterator that is tested for being a skip (or +/// equivalent) +/// \param ignore_labels: If the caller takes care of moving labels, then even +/// skip statements carrying labels can be treated as skips (even though they +/// may carry key information such as error labels). /// \return True, iff it is equivalent to a skip. bool is_skip( const goto_programt &body, @@ -79,10 +79,10 @@ bool is_skip( } /// remove unnecessary skip statements -/// \param goto_program goto program containing the instructions to be cleaned -/// in the range [begin, end) -/// \param begin iterator pointing to first instruction to be considered -/// \param end iterator pointing beyond last instruction to be considered +/// \param goto_program: goto program containing the instructions to be cleaned +/// in the range [begin, end) +/// \param begin: iterator pointing to first instruction to be considered +/// \param end: iterator pointing beyond last instruction to be considered void remove_skip( goto_programt &goto_program, goto_programt::targett begin, diff --git a/src/goto-programs/remove_virtual_functions.cpp b/src/goto-programs/remove_virtual_functions.cpp index 7e54bc3284..8b0e96ac0d 100644 --- a/src/goto-programs/remove_virtual_functions.cpp +++ b/src/goto-programs/remove_virtual_functions.cpp @@ -74,11 +74,11 @@ remove_virtual_functionst::remove_virtual_functionst( /// Replace specified virtual function call with a static call to its /// most derived implementation -/// \param goto_program [in/out]: GOTO program to modify -/// \param target iterator: to a function in the supplied GOTO program -/// to replace. Must point to a virtual function call. +/// \param [in,out] goto_program: GOTO program to modify +/// \param target: iterator to a function in the supplied GOTO program +/// to replace. Must point to a virtual function call. /// \return Returns a pointer to the statement in the supplied GOTO -/// program after replaced function call +/// program after replaced function call goto_programt::targett remove_virtual_functionst::remove_virtual_function( goto_programt &goto_program, goto_programt::targett target) @@ -105,7 +105,7 @@ goto_programt::targett remove_virtual_functionst::remove_virtual_function( } /// Create a concrete function call to replace a virtual one -/// \param call [in,out]: the function call to update +/// \param [in,out] call: the function call to update /// \param function_symbol: the function to be called /// \param ns: namespace static void create_static_function_call( @@ -131,16 +131,16 @@ static void create_static_function_call( /// implementation. If there's a type mismatch between implementation /// and the instance type or if fallback_action is set to /// ASSUME_FALSE, then function is substituted with a call to ASSUME(false) -/// \param goto_program [in/out]: GOTO program to modify +/// \param [in,out] goto_program: GOTO program to modify /// \param target: Iterator to the GOTO instruction in the supplied -/// GOTO program to be removed. Must point to a function call +/// GOTO program to be removed. Must point to a function call /// \param functions: Dispatch table - all possible implementations of -/// this function sorted from the least to the most derived +/// this function sorted from the least to the most derived /// \param fallback_action: - ASSUME_FALSE to replace virtual function -/// calls with ASSUME(false) or CALL_LAST_FUNCTION to replace them -/// with the most derived matching call +/// calls with ASSUME(false) or CALL_LAST_FUNCTION to replace them +/// with the most derived matching call /// \return Returns a pointer to the statement in the supplied GOTO -/// program after replaced function call +/// program after replaced function call goto_programt::targett remove_virtual_functionst::remove_virtual_function( goto_programt &goto_program, goto_programt::targett target, @@ -402,8 +402,8 @@ void remove_virtual_functionst::get_child_functions_rec( /// Used to get dispatch entries to call for the given function /// \param function: function that should be called -/// \param[out] functions: is assigned a list of dispatch entries, i.e., pairs -/// of class names and function symbol to call when encountering the class. +/// \param [out] functions: is assigned a list of dispatch entries, i.e., pairs +/// of class names and function symbol to call when encountering the class. void remove_virtual_functionst::get_functions( const exprt &function, dispatch_table_entriest &functions) @@ -491,7 +491,7 @@ void remove_virtual_functionst::get_functions( /// \param class_id: Class identifier to look up /// \param component_name: Name of the function to look up /// \return nil_exprt instance on error and a symbol_exprt pointing to -/// the method on success +/// the method on success exprt remove_virtual_functionst::get_method( const irep_idt &class_id, const irep_idt &component_name) const @@ -597,16 +597,16 @@ void remove_virtual_functions(goto_model_functiont &function) /// and the instance type or if fallback_action is set to /// ASSUME_FALSE, then function is substituted with a call to ASSUME(false) /// \param symbol_table: Symbol table -/// \param goto_program [in/out]: GOTO program to modify +/// \param [in,out] goto_program: GOTO program to modify /// \param instruction: Iterator to the GOTO instruction in the supplied -/// GOTO program to be removed. Must point to a function call +/// GOTO program to be removed. Must point to a function call /// \param dispatch_table: Dispatch table - all possible implementations of -/// this function sorted from the least to the most derived +/// this function sorted from the least to the most derived /// \param fallback_action: - ASSUME_FALSE to replace virtual function -/// calls with ASSUME(false) or CALL_LAST_FUNCTION to replace them -/// with the most derived matching call +/// calls with ASSUME(false) or CALL_LAST_FUNCTION to replace them +/// with the most derived matching call /// \return Returns a pointer to the statement in the supplied GOTO -/// program after replaced function call +/// program after replaced function call goto_programt::targett remove_virtual_function( symbol_tablet &symbol_table, goto_programt &goto_program, diff --git a/src/goto-programs/remove_virtual_functions.h b/src/goto-programs/remove_virtual_functions.h index 57a679c41d..b47854e63f 100644 --- a/src/goto-programs/remove_virtual_functions.h +++ b/src/goto-programs/remove_virtual_functions.h @@ -82,11 +82,11 @@ goto_programt::targett remove_virtual_function( /// Given a function expression representing a virtual method of a class, /// the function computes all overridden methods of that virtual method. /// \param function: The virtual function expression for which the overridden -/// methods will be searched for. +/// methods will be searched for. /// \param symbol_table: A symbol table. /// \param class_hierarchy: A class hierarchy. /// \param [out] overridden_functions: Output collection into which all -/// overridden functions will be stored. +/// overridden functions will be stored. void collect_virtual_function_callees( const exprt &function, const symbol_tablet &symbol_table, diff --git a/src/goto-programs/show_properties.h b/src/goto-programs/show_properties.h index ce4cb341c2..ea8cc46e4a 100644 --- a/src/goto-programs/show_properties.h +++ b/src/goto-programs/show_properties.h @@ -43,11 +43,11 @@ void show_properties( /// \brief Returns a source_locationt that corresponds /// to the property given by an irep_idt. -/// \param property irep_idt that identifies property -/// \param goto_functions program in which to search for +/// \param property: irep_idt that identifies property +/// \param goto_functions: program in which to search for /// the property /// \return optional the location of the -/// property, if found. +/// property, if found. optionalt find_property( const irep_idt &property, const goto_functionst &goto_functions); diff --git a/src/goto-programs/wp.h b/src/goto-programs/wp.h index d967ce3dd0..3008ed1b56 100644 --- a/src/goto-programs/wp.h +++ b/src/goto-programs/wp.h @@ -16,22 +16,19 @@ class codet; class exprt; class namespacet; -/*! \brief Compute the weakest precondition of the given program - * piece \a code with respect to the expression \a post. - * \param code Program - * \param post Postcondition - * \param ns Namespace - * \return Weakest precondition -*/ +/// Compute the weakest precondition of the given program +/// piece \a code with respect to the expression \a post. +/// \param code: Program +/// \param post: Postcondition +/// \param ns: Namespace +/// \return Weakest precondition exprt wp( const codet &code, const exprt &post, const namespacet &ns); -/*! \brief approximate the non-deterministic choice - in a way cheaper than by (proper) quantification -*/ - +/// Approximate the non-deterministic choice in a way cheaper than by (proper) +/// quantification void approximate_nondet(exprt &dest); #endif // CPROVER_GOTO_PROGRAMS_WP_H diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h index 0921be1c5d..3ea4934a93 100644 --- a/src/goto-symex/goto_symex.h +++ b/src/goto-symex/goto_symex.h @@ -166,12 +166,12 @@ protected: /// Initialise the symbolic execution and the given state with pc /// as entry point. - /// \param state Symex state to initialise. - /// \param get_goto_function producer for GOTO functions - /// \param function_identifier The function in which the instructions are - /// \param pc first instruction to symex - /// \param limit final instruction, which itself will not - /// be symexed. + /// \param state: Symex state to initialise. + /// \param get_goto_function: producer for GOTO functions + /// \param function_identifier: The function in which the instructions are + /// \param pc: first instruction to symex + /// \param limit: final instruction, which itself will not + /// be symexed. void initialize_entry_point( statet &state, const get_goto_functiont &get_goto_function, @@ -181,8 +181,8 @@ protected: /// Invokes symex_step and verifies whether additional threads can be /// executed. - /// \param state Current GOTO symex step. - /// \param get_goto_function function that retrieves function bodies + /// \param state: Current GOTO symex step. + /// \param get_goto_function: function that retrieves function bodies void symex_threaded_step( statet &, const get_goto_functiont &); diff --git a/src/goto-symex/path_storage.h b/src/goto-symex/path_storage.h index c0e1799148..e155b71bda 100644 --- a/src/goto-symex/path_storage.h +++ b/src/goto-symex/path_storage.h @@ -64,8 +64,8 @@ public: /// instruction with two successors. Thus, we always add a pair of paths to /// the path storage. /// - /// \param next_instruction the instruction following the goto instruction - /// \param jump_target the target instruction of the goto instruction + /// \param next_instruction: the instruction following the goto instruction + /// \param jump_target: the target instruction of the goto instruction virtual void push(const patht &next_instruction, const patht &jump_target) = 0; diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp index 3823cfecff..ab10ac0777 100644 --- a/src/goto-symex/symex_goto.cpp +++ b/src/goto-symex/symex_goto.cpp @@ -389,14 +389,14 @@ static void for_each2( /// Helper function for \c phi_function which merges the names of an identifier /// for two different states. /// \param goto_state: first state -/// \param[in, out] dest_state: second state +/// \param [in, out] dest_state: second state /// \param ns: namespace /// \param diff_guard: difference between the guards of the two states /// \param guard_identifier: prefix used for goto symex guards -/// \param[out] log: logger for debug messages +/// \param [out] log: logger for debug messages /// \param do_simplify: should the right-hand-side of the assignment that is /// added to the target be simplified -/// \param[out] target: equation that will receive the resulting assignment +/// \param [out] target: equation that will receive the resulting assignment /// \param ssa: SSA expression to merge /// \param goto_count: current level 2 count in \p goto_state of /// \p l1_identifier diff --git a/src/goto-symex/symex_target_equation.cpp b/src/goto-symex/symex_target_equation.cpp index 6daf2fbfa6..637715ffa0 100644 --- a/src/goto-symex/symex_target_equation.cpp +++ b/src/goto-symex/symex_target_equation.cpp @@ -945,8 +945,8 @@ void symex_target_equationt::SSA_stept::output(std::ostream &out) const } /// Check that the SSA step is well-formed -/// \param ns namespace to lookup identifiers -/// \param vm validation mode to be used for reporting failures +/// \param ns: namespace to lookup identifiers +/// \param vm: validation mode to be used for reporting failures void symex_target_equationt::SSA_stept::validate( const namespacet &ns, const validation_modet vm) const diff --git a/src/json-symtab-language/json_symbol.cpp b/src/json-symtab-language/json_symbol.cpp index 72009a2319..97ba071ec3 100644 --- a/src/json-symtab-language/json_symbol.cpp +++ b/src/json-symtab-language/json_symbol.cpp @@ -17,7 +17,7 @@ Author: Chris Smowton, chris.smowton@diffblue.com /// Return string value for a given key if present in the json object. /// \param in: The json object that is getting fetched as a string. /// \param key: The key for the json value to be fetched. -/// \return: A string value for the corresponding key. +/// \return A string value for the corresponding key. static const std::string & try_get_string(const jsont &in, const std::string &key) { @@ -30,7 +30,7 @@ try_get_string(const jsont &in, const std::string &key) /// Return boolean value for a given key if present in the json object. /// \param in: The json object that is getting fetched as a boolean. /// \param key: The key for the json value to be fetched. -/// \return: A boolean value for the corresponding key. +/// \return A boolean value for the corresponding key. static bool try_get_bool(const jsont &in, const std::string &key) { if(!(in.is_true() || in.is_false())) @@ -41,7 +41,7 @@ static bool try_get_bool(const jsont &in, const std::string &key) /// Deserialise a json object to a symbolt. /// \param in: The json object that is getting fetched as an object. -/// \return: A symbolt representing the json object. +/// \return A symbolt representing the json object. symbolt symbol_from_json(const jsont &in) { if(!in.is_object()) diff --git a/src/json-symtab-language/json_symtab_language.cpp b/src/json-symtab-language/json_symtab_language.cpp index 8c9d9024b8..84b5cd373f 100644 --- a/src/json-symtab-language/json_symtab_language.cpp +++ b/src/json-symtab-language/json_symtab_language.cpp @@ -16,7 +16,7 @@ Author: Chris Smowton, chris.smowton@diffblue.com /// Parse a goto program in json form. /// \param instream: The input stream /// \param path: A file path -/// \return: boolean signifying success or failure of the parsing +/// \return boolean signifying success or failure of the parsing bool json_symtab_languaget::parse( std::istream &instream, const std::string &path) @@ -27,7 +27,7 @@ bool json_symtab_languaget::parse( /// Typecheck a goto program in json form. /// \param symbol_table: The symbol table containing symbols read from file. /// \param module: A useless parameter, there for interface consistency. -/// \return: boolean signifying success or failure of the typechecking. +/// \return boolean signifying success or failure of the typechecking. bool json_symtab_languaget::typecheck( symbol_tablet &symbol_table, const std::string &module) diff --git a/src/langapi/mode.cpp b/src/langapi/mode.cpp index d2bc247418..b89d501d7d 100644 --- a/src/langapi/mode.cpp +++ b/src/langapi/mode.cpp @@ -76,7 +76,7 @@ get_mode_from_identifier(const namespacet &ns, const irep_idt &identifier) /// \param ns: a namespace /// \param identifier: an identifier /// \return the corresponding language if the mode is not `ID_unknown`, or -/// the default language otherwise; +/// the default language otherwise; /// Note: It is assumed as an invariant that languages of symbols in the symbol /// table have been registered. std::unique_ptr diff --git a/src/pointer-analysis/goto_program_dereference.cpp b/src/pointer-analysis/goto_program_dereference.cpp index 35921242fd..3c67474791 100644 --- a/src/pointer-analysis/goto_program_dereference.cpp +++ b/src/pointer-analysis/goto_program_dereference.cpp @@ -20,7 +20,7 @@ Author: Daniel Kroening, kroening@kroening.com #include /// \param expr: expression to check -/// \param[out] symbol: symbol which gets assigned the value from the +/// \param [out] symbol: symbol which gets assigned the value from the /// `failed_symbol` comment /// \return true when `expr` is a symbol, whose type contains a `failed_symbol` /// comment which exists in the namespace. @@ -233,7 +233,7 @@ void goto_program_dereferencet::dereference_rec( /// Gets the value set corresponding to the current target and /// expression `expr`. /// \param expr: an expression -/// \param[out] dest: gets the value set +/// \param [out] dest: gets the value set void goto_program_dereferencet::get_value_set( const exprt &expr, value_setst::valuest &dest) diff --git a/src/pointer-analysis/value_set.h b/src/pointer-analysis/value_set.h index 433c553152..fe950d9865 100644 --- a/src/pointer-analysis/value_set.h +++ b/src/pointer-analysis/value_set.h @@ -457,8 +457,8 @@ protected: /// Reads the set of objects pointed to by `expr`, including making /// recursive lookups for dereference operations etc. /// \param expr: query expression - /// \param dest [out]: overwritten by the set of object numbers pointed to - /// \param ns; global namespace + /// \param [out] dest: overwritten by the set of object numbers pointed to + /// \param ns: global namespace /// \param is_simplified: if false, simplify `expr` before reading. void get_value_set( const exprt &expr, diff --git a/src/pointer-analysis/value_set_dereference.h b/src/pointer-analysis/value_set_dereference.h index eea6271ba0..f1e8c08f9c 100644 --- a/src/pointer-analysis/value_set_dereference.h +++ b/src/pointer-analysis/value_set_dereference.h @@ -27,14 +27,14 @@ class symbolt; class value_set_dereferencet { public: - /// \param _ns Namespace - /// \param _new_symbol_table A symbol_table to store new symbols in - /// \param _dereference_callback Callback object for getting the set of - /// objects a given pointer may point to. - /// \param _language_mode Mode for any new symbols created to represent - /// a dereference failure - /// \param _exclude_null_derefs Ignore value-set entries that indicate a given - /// dereference may follow a null pointer + /// \param _ns: Namespace + /// \param _new_symbol_table: A symbol_table to store new symbols in + /// \param _dereference_callback: Callback object for getting the set of + /// objects a given pointer may point to. + /// \param _language_mode: Mode for any new symbols created to represent a + /// dereference failure + /// \param _exclude_null_derefs: Ignore value-set entries that indicate a + // given dereference may follow a null pointer value_set_dereferencet( const namespacet &_ns, symbol_tablet &_new_symbol_table, @@ -54,12 +54,11 @@ public: /// Dereference the given pointer-expression. Any errors are /// reported to the callback method given in the constructor. - /// \param pointer A pointer-typed expression, to + /// \param pointer: A pointer-typed expression, to /// be dereferenced. - /// \param guard A guard, which is assumed to hold when - /// dereferencing. - /// \param mode Indicates whether the dereferencing - /// is a load or store (unused). + /// \param guard: A guard, which is assumed to hold when dereferencing. + /// \param mode: Indicates whether the dereferencing is a load or store + // (unused). virtual exprt dereference( const exprt &pointer, const guardt &guard, diff --git a/src/solvers/flattening/bv_utils.cpp b/src/solvers/flattening/bv_utils.cpp index 831736f217..87500ca48d 100644 --- a/src/solvers/flattening/bv_utils.cpp +++ b/src/solvers/flattening/bv_utils.cpp @@ -991,11 +991,10 @@ void bv_utilst::equal_const_register(const bvt &var) return; } - /// The obvious recursive comparison, the interesting thing is that it is cached /// so the literals are shared between constants. /// \param Bit:vectors for a variable and a const to compare, note that -/// to avoid significant amounts of copying these are mutable and consumed. +/// to avoid significant amounts of copying these are mutable and consumed. /// \return The literal that is true if and only if all the bits in var and /// const are equal. literalt bv_utilst::equal_const_rec(bvt &var, bvt &constant) diff --git a/src/solvers/lowering/expr_lowering.h b/src/solvers/lowering/expr_lowering.h index 69a00c7ad9..2f033a45d1 100644 --- a/src/solvers/lowering/expr_lowering.h +++ b/src/solvers/lowering/expr_lowering.h @@ -22,8 +22,8 @@ exprt lower_byte_operators(const exprt &src, const namespacet &ns); bool has_byte_operator(const exprt &src); /// Lower a popcount_exprt to arithmetic and logic expressions -/// \param expr Input expression to be translated -/// \param ns Namespace for type lookups +/// \param expr: Input expression to be translated +/// \param ns: Namespace for type lookups /// \return Semantically equivalent expression exprt lower_popcount(const popcount_exprt &expr, const namespacet &ns); diff --git a/src/solvers/prop/literal_expr.h b/src/solvers/prop/literal_expr.h index 6694033716..c039e66bbe 100644 --- a/src/solvers/prop/literal_expr.h +++ b/src/solvers/prop/literal_expr.h @@ -36,16 +36,11 @@ public: } }; -/*! \brief Cast a generic exprt to a \ref literal_exprt - * - * This is an unchecked conversion. \a expr must be known to be \ref - * literal_exprt. - * - * \param expr Source expression - * \return Object of type \ref literal_exprt - * - * \ingroup gr_std_expr -*/ +/// Cast a generic exprt to a \ref literal_exprt. This is an unchecked +/// conversion. \a expr must be known to be \ref literal_exprt. +/// \param expr: Source expression +/// \return Object of type \ref literal_exprt +/// \ingroup gr_std_expr inline const literal_exprt &to_literal_expr(const exprt &expr) { PRECONDITION(expr.id() == ID_literal); @@ -54,9 +49,8 @@ inline const literal_exprt &to_literal_expr(const exprt &expr) return static_cast(expr); } -/*! \copydoc to_literal_expr(const exprt &) - * \ingroup gr_std_expr -*/ +/// \copydoc to_literal_expr(const exprt &) +/// \ingroup gr_std_expr inline literal_exprt &to_literal_expr(exprt &expr) { PRECONDITION(expr.id() == ID_literal); diff --git a/src/solvers/refinement/string_builtin_function.h b/src/solvers/refinement/string_builtin_function.h index 7338d38363..addbebadcc 100644 --- a/src/solvers/refinement/string_builtin_function.h +++ b/src/solvers/refinement/string_builtin_function.h @@ -431,7 +431,7 @@ public: /// Functions that are not yet supported in this class but are supported by /// string_constraint_generatort. /// \note Ultimately this should be disappear, once all builtin function have -/// a corresponding string_builtin_functiont class. +/// a corresponding string_builtin_functiont class. class string_builtin_function_with_no_evalt : public string_builtin_functiont { public: diff --git a/src/solvers/refinement/string_constraint.cpp b/src/solvers/refinement/string_constraint.cpp index ec0911abcd..0441daeabf 100644 --- a/src/solvers/refinement/string_constraint.cpp +++ b/src/solvers/refinement/string_constraint.cpp @@ -12,7 +12,7 @@ Author: Diffblue Ltd. #include /// Runs a solver instance to verify whether an expression can only be -// non-negative. +/// non-negative. /// \param expr: the expression to check for negativity /// \return true if `expr < 0` is unsatisfiable, false otherwise static bool cannot_be_neg(const exprt &expr) diff --git a/src/solvers/refinement/string_constraint_generator_code_points.cpp b/src/solvers/refinement/string_constraint_generator_code_points.cpp index 70e22b1048..da89d9ae20 100644 --- a/src/solvers/refinement/string_constraint_generator_code_points.cpp +++ b/src/solvers/refinement/string_constraint_generator_code_points.cpp @@ -186,7 +186,7 @@ std::pair add_axioms_for_code_point_before( /// String.codePointCount java function /// \param fresh_symbol: generator of fresh symbols /// \param f: function application with three arguments string `str`, integer -/// `begin` and integer `end`. +/// `begin` and integer `end`. /// \param array_pool: pool of arrays representing strings /// \return an integer expression std::pair add_axioms_for_code_point_count( diff --git a/src/solvers/refinement/string_constraint_generator_comparison.cpp b/src/solvers/refinement/string_constraint_generator_comparison.cpp index d3a55270aa..9fe1b92759 100644 --- a/src/solvers/refinement/string_constraint_generator_comparison.cpp +++ b/src/solvers/refinement/string_constraint_generator_comparison.cpp @@ -25,7 +25,7 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com /// \lor (0 \le witness<|s_1| \land s_1[witness] \ne s_2[witness]) \f$ /// \param fresh_symbol: generator of fresh symbols /// \param f: function application with arguments refined_string `s1` and -/// refined_string `s2` +/// refined_string `s2` /// \param pool: pool of arrays representing strings /// \return Boolean expression `eq` std::pair add_axioms_for_equals( @@ -126,7 +126,7 @@ static exprt character_equals_ignore_case( /// \land\lnot {\tt equal\_ignore\_case}(s_1[witness],s_2[witness]) \f$ /// \param fresh_symbol: generator of fresh symbols /// \param f: function application with arguments refined_string `s1` and -/// refined_string `s2` +/// refined_string `s2` /// \param pool: pool of arrays representing strings /// \return Boolean expression `eq` std::pair add_axioms_for_equals_ignore_case( @@ -234,8 +234,8 @@ string_constraint_generatort::add_axioms_for_hash_code( /// \land res=|s1|-|s2|) \f$ /// * \f$ \forall i' add_axioms_for_compare_to( diff --git a/src/solvers/refinement/string_constraint_generator_constants.cpp b/src/solvers/refinement/string_constraint_generator_constants.cpp index c6d4b79ded..cd1ca773f2 100644 --- a/src/solvers/refinement/string_constraint_generator_constants.cpp +++ b/src/solvers/refinement/string_constraint_generator_constants.cpp @@ -57,7 +57,7 @@ std::pair add_axioms_for_constant( /// Add axioms to say that the returned string expression is empty /// \param f: function application with arguments integer `length` and character -/// pointer `ptr`. +/// pointer `ptr`. /// \return integer expression equal to zero std::pair add_axioms_for_empty_string( const function_application_exprt &f) @@ -76,8 +76,8 @@ std::pair add_axioms_for_empty_string( /// \param arg: expression of type string typet /// \param guard: condition under which `res` should be equal to arg /// \return 0 if constraints were added, 1 if expression could not be handled -/// and no constraint was added. Expression we can handle are of the -/// form \f$ e := "" | (expr)? e : e \f$ +/// and no constraint was added. Expression we can handle are of the form +/// \f$ e := "" | (expr)? e : e \f$ std::pair add_axioms_for_cprover_string( symbol_generatort &fresh_symbol, const array_string_exprt &res, @@ -107,7 +107,7 @@ std::pair add_axioms_for_cprover_string( /// \todo The name of the function should be changed to reflect what it does. /// \param fresh_symbol: generator of fresh symbols /// \param f: function application with an argument which is a string literal -/// that is a constant with a string value. +/// that is a constant with a string value. /// \param array_pool: pool of arrays representing strings /// \return string expression std::pair add_axioms_from_literal( diff --git a/src/solvers/refinement/string_constraint_generator_indexof.cpp b/src/solvers/refinement/string_constraint_generator_indexof.cpp index 48e0366f01..1fa6c53b4d 100644 --- a/src/solvers/refinement/string_constraint_generator_indexof.cpp +++ b/src/solvers/refinement/string_constraint_generator_indexof.cpp @@ -284,8 +284,8 @@ std::pair add_axioms_for_last_index_of_string( /// \warning slow for string targets /// \param fresh_symbol: generator of fresh symbols /// \param f: function application with arguments refined_string `haystack`, -/// refined_string or character `needle`, and optional integer -/// `from_index` with default value `0` +/// refined_string or character `needle`, and optional integer `from_index` +/// with default value `0` /// \param array_pool: pool of arrays representing strings /// \return integer expression std::pair add_axioms_for_index_of( @@ -342,7 +342,7 @@ std::pair add_axioms_for_index_of( /// \param c: a character expression /// \param from_index: an integer expression /// \return integer expression `index` representing the last index of `needle` -/// in `haystack` before or at `from_index`, or `-1` if there is none +/// in `haystack` before or at `from_index`, or `-1` if there is none std::pair add_axioms_for_last_index_of( symbol_generatort &fresh_symbol, const array_string_exprt &str, @@ -408,8 +408,8 @@ std::pair add_axioms_for_last_index_of( /// \warning slow for string targets /// \param fresh_symbol: generator of fresh symbols /// \param f: function application with arguments refined_string `haystack`, -/// refined_string or character `needle`, and optional integer -/// `from_index` with default value `|haystack|-1` +/// refined_string or character `needle`, and optional integer +/// `from_index` with default value `|haystack|-1` /// \param array_pool: pool of arrays representing strings /// \return an integer expression std::pair add_axioms_for_last_index_of( diff --git a/src/solvers/refinement/string_constraint_generator_insert.cpp b/src/solvers/refinement/string_constraint_generator_insert.cpp index b783aad566..617911c2de 100644 --- a/src/solvers/refinement/string_constraint_generator_insert.cpp +++ b/src/solvers/refinement/string_constraint_generator_insert.cpp @@ -29,7 +29,7 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com /// \param s2: array of characters expression /// \param offset: integer expression /// \return an expression expression which is different from zero if there is -/// an exception to signal +/// an exception to signal std::pair add_axioms_for_insert( symbol_generatort &fresh_symbol, const array_string_exprt &res, @@ -97,12 +97,11 @@ exprt length_constraint_for_insert( /// is considered instead of `s2`. /// \param fresh_symbol: generator of fresh symbols /// \param f: function application with arguments integer `|res|`, character -/// pointer `&res[0]`, refined_string `s1`, refined_string`s2`, -/// integer `offset`, optional integer `start` and optional integer -/// `end` +/// pointer `&res[0]`, refined_string `s1`, refined_string`s2`, integer +/// `offset`, optional integer `start` and optional integer `end` /// \param pool: pool of arrays representing strings -/// \return an integer expression which is different from zero if there is -/// an exception to signal +/// \return an integer expression which is different from zero if there is an +/// exception to signal std::pair add_axioms_for_insert( symbol_generatort &fresh_symbol, const function_application_exprt &f, diff --git a/src/solvers/refinement/string_constraint_generator_main.cpp b/src/solvers/refinement/string_constraint_generator_main.cpp index e1d1cc411b..5f16df11e8 100644 --- a/src/solvers/refinement/string_constraint_generator_main.cpp +++ b/src/solvers/refinement/string_constraint_generator_main.cpp @@ -167,7 +167,7 @@ const std::set &array_poolt::created_strings() const /// is infinite, a new integer symbol is created and stored in `array_pool`. /// This also adds the default axioms for `arr`. /// \param f: a function application with argument a character array `arr` and -/// a character pointer `ptr`. +/// a character pointer `ptr`. exprt string_constraint_generatort::associate_array_to_pointer( const function_application_exprt &f) { @@ -188,7 +188,7 @@ exprt string_constraint_generatort::associate_array_to_pointer( /// 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`. +/// an integer `length`. /// \return integer expression equal to 0 exprt string_constraint_generatort::associate_length_to_array( const function_application_exprt &f) @@ -247,8 +247,8 @@ void merge(string_constraintst &result, string_constraintst other) /// \param start: index of the first character to constrain /// \param end: index at which we stop adding constraints /// \param char_set: a string of the form "-" where -/// `` and `` are two characters, which represents -/// the set of characters that are between `low_char` and `high_char`. +/// `` and `` are two characters, which represents the +/// set of characters that are between `low_char` and `high_char`. /// \return a string expression that is linked to the argument through axioms /// that are added to the list string_constraintst add_constraint_on_characters( @@ -283,8 +283,8 @@ string_constraintst add_constraint_on_characters( /// `char_set` if \f$low_char \le c \le high_char\f$. /// \param fresh_symbol: generator of fresh symbols /// \param f: a function application with arguments: integer `|s|`, character -/// pointer `&s[0]`, string `char_set_string`, -/// optional integers `start` and `end` +/// pointer `&s[0]`, string `char_set_string`, optional integers `start` and +/// `end` /// \param array_pool: pool of arrays representing strings /// \return integer expression whose value is zero std::pair add_axioms_for_constrain_characters( @@ -483,7 +483,7 @@ string_constraint_generatort::add_axioms_for_function_application( /// \deprecated should use substring instead /// \param fresh_symbol: generator of fresh symbols /// \param f: function application with one argument, which is a string, -/// or three arguments: string, integer offset and count +/// or three arguments: string, integer offset and count /// \param array_pool: pool of arrays representing strings /// \return a new string expression DEPRECATED("should use substring instead") @@ -587,7 +587,7 @@ exprt maximum(const exprt &a, const exprt &b) } /// Returns a non-negative version of the argument. -/// \param expr: expression of which we want a non-negative version +/// \param expr: expression of which we want a non-negative version /// \return `max(0, expr)` exprt zero_if_negative(const exprt &expr) { diff --git a/src/solvers/refinement/string_constraint_generator_testing.cpp b/src/solvers/refinement/string_constraint_generator_testing.cpp index 4fbf7727a2..5310304b37 100644 --- a/src/solvers/refinement/string_constraint_generator_testing.cpp +++ b/src/solvers/refinement/string_constraint_generator_testing.cpp @@ -90,10 +90,10 @@ std::pair add_axioms_for_is_prefix( /// \todo Get rid of the boolean flag. /// \param fresh_symbol: generator of fresh symbols /// \param f: a function application with arguments refined_string `s0`, -/// refined string `s1` and optional integer argument `offset` -/// whose default value is 0 +/// refined string `s1` and optional integer argument `offset`whose default +/// value is 0 /// \param swap_arguments: a Boolean telling whether the prefix is the second -/// argument or the first argument +/// argument or the first argument /// \param array_pool: pool of arrays representing strings /// \return boolean expression `isprefix` std::pair add_axioms_for_is_prefix( @@ -159,9 +159,9 @@ std::pair add_axioms_for_is_empty( /// \todo The primitive should be renamed `ends_with`. /// \param fresh_symbol: generator of fresh symbols /// \param f: a function application with arguments refined_string `s0` -/// and refined_string `s1` +/// and refined_string `s1` /// \param swap_arguments: boolean flag telling whether the suffix is the second -/// argument or the first argument +/// argument or the first argument /// \param array_pool: pool of arrays representing strings /// \return Boolean expression `issuffix` DEPRECATED("should use `strings_startwith(s0, s1, s1.length - s0.length)`") diff --git a/src/solvers/refinement/string_constraint_generator_transformation.cpp b/src/solvers/refinement/string_constraint_generator_transformation.cpp index f3f215a282..d31f4c8adf 100644 --- a/src/solvers/refinement/string_constraint_generator_transformation.cpp +++ b/src/solvers/refinement/string_constraint_generator_transformation.cpp @@ -31,7 +31,7 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com /// \todo We can reduce the number of constraints by merging 2 and 3. /// \param fresh_symbol: generator of fresh symbols /// \param f: function application with arguments integer `|res|`, character -/// pointer `&res[0]`, refined_string `s1`, integer `k` +/// pointer `&res[0]`, refined_string `s1`, integer `k` /// \param array_pool: pool of arrays representing strings /// \return integer expression equal to `0` std::pair add_axioms_for_set_length( @@ -86,11 +86,11 @@ std::pair add_axioms_for_set_length( /// tan the end index. /// \param fresh_symbol: generator of fresh symbols /// \param f: function application with arguments integer `|res|`, character -/// pointer `&res[0]`, refined_string `str`, integer `start`, -/// optional integer `end` with default value `|str|`. +/// pointer `&res[0]`, refined_string `str`, integer `start`, optional integer +/// `end` with default value `|str|`. /// \param array_pool: pool of arrays representing strings /// \return integer expression which is different from 0 when there is an -/// exception to signal +/// exception to signal std::pair add_axioms_for_substring( symbol_generatort &fresh_symbol, const function_application_exprt &f, @@ -176,10 +176,10 @@ std::pair add_axioms_for_substring( /// \note Some of the constraints among 1, 2, 3, 4 and 5 seems to be redundant /// \param fresh_symbol: generator of fresh symbols /// \param f: function application with arguments integer `|res|`, character -/// pointer `&res[0]`, refined_string `str`. +/// pointer `&res[0]`, refined_string `str`. /// \param array_pool: pool of arrays representing strings /// \return integer expression which is different from 0 when there is an -/// exception to signal +/// exception to signal std::pair add_axioms_for_trim( symbol_generatort &fresh_symbol, const function_application_exprt &f, @@ -248,8 +248,8 @@ std::pair add_axioms_for_trim( /// If both expressions are characters, return pair of them /// If both expressions are 1-length strings, return first character of each /// Otherwise return empty optional -/// \param expr1 First expression -/// \param expr2 Second expression +/// \param expr1: First expression +/// \param expr2: Second expression /// \param get_string_expr: Function that yields an array_string_exprt /// corresponding to either `expr1` or `expr2`, for the case where they are /// not primitive chars. @@ -290,8 +290,8 @@ static optionalt> to_char_pair( /// be fixed in the future) /// \param fresh_symbol: generator of fresh symbols /// \param f: function application with arguments integer `|res|`, character -/// pointer `&res[0]`, refined_string `str`, character `old_char` and -/// character `new_char` +/// pointer `&res[0]`, refined_string `str`, character `old_char` and +/// character `new_char` /// \param array_pool: pool of arrays representing strings /// \return an integer expression equal to 0 std::pair add_axioms_for_replace( @@ -404,8 +404,7 @@ std::pair add_axioms_for_delete( /// (More...) \endlink /// \param fresh_symbol: generator of fresh symbols /// \param f: function application with arguments integer `|res|`, character -/// pointer `&res[0]`, refined_string `str`, integer `start` -/// and integer `end` +/// pointer `&res[0]`, refined_string `str`, integer `start` and integer `end` /// \param array_pool: pool of arrays representing strings /// \return an integer expression whose value is different from 0 to signal /// an exception diff --git a/src/solvers/refinement/string_constraint_generator_valueof.cpp b/src/solvers/refinement/string_constraint_generator_valueof.cpp index e7ba1b887f..a6210e57ea 100644 --- a/src/solvers/refinement/string_constraint_generator_valueof.cpp +++ b/src/solvers/refinement/string_constraint_generator_valueof.cpp @@ -286,9 +286,9 @@ std::pair add_axioms_from_int_hex( /// \copybrief add_axioms_from_char(const array_string_exprt &res, const exprt &c) // NOLINTNEXTLINE /// \link add_axioms_from_char(const array_string_exprt &res, const exprt &c) -/// (More...) \endlink +/// (More...) \endlink /// \param f: function application with arguments integer `|res|`, character -/// pointer `&res[0]` and character `c` +/// pointer `&res[0]` and character `c` /// \param array_pool: pool of arrays representing strings /// \return code 0 on success std::pair add_axioms_from_char( @@ -408,7 +408,7 @@ string_constraintst add_axioms_for_correct_number_format( /// \param input_int: the integer represented by str /// \param type: the type for input_int /// \param strict_formatting: if true, don't allow a leading plus, redundant -/// zeros or upper case letters +/// zeros or upper case letters /// \param str: input string /// \param max_string_length: the maximum length str can have /// \param radix: the radix, with the same type as input_int @@ -502,7 +502,7 @@ string_constraintst add_axioms_for_characters_in_integer_string( /// to the value represented by `str` /// \param fresh_symbol: generator of fresh symbols /// \param f: a function application with arguments refined_string `str` and -/// an optional integer for the radix +/// an optional integer for the radix /// \param array_pool: pool of arrays representing strings /// \param ns: namespace /// \return integer expression equal to the value represented by `str` @@ -555,7 +555,7 @@ std::pair add_axioms_for_parse_int( /// radix is 10 then check if the character is in the range 0-9. /// \param chr: the character /// \param strict_formatting: if true, don't allow upper case characters -/// \param radix_as_char: the radix as an expression of the same type as chr +/// \param radix_as_char: the radix as an expression of the same type as chr /// \param radix_ul: the radix, which should be between 2 and 36, or 0, in /// which case the return value will work for any radix /// \return an expression for the condition diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp index 1b4b61ac8b..8aa89e992c 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/refinement/string_refinement.cpp @@ -53,9 +53,9 @@ static optionalt find_counter_example( /// * we give lemma `b` to a fresh solver; /// * if no counter-example to `b` is found, this means the constraint `a` /// is satisfied by the valuation given by get. -/// \return `true` if the current model satisfies all the axioms, -/// `false` otherwise with a list of lemmas which are obtained by -/// instantiating constraints at indexes given by counter-examples. +/// \return `true` if the current model satisfies all the axioms, `false` +/// otherwise with a list of lemmas which are obtained by instantiating +/// constraints at indexes given by counter-examples. static std::pair> check_axioms( const string_axiomst &axioms, string_constraint_generatort &generator, @@ -308,7 +308,7 @@ void string_refinementt::set_to(const exprt &expr, bool value) /// \param ns: namespace /// \param stream: output stream /// \return union_find_replacet where char pointer that have been set equal -/// by an equation are associated to the same element +/// by an equation are associated to the same element static void add_equations_for_symbol_resolution( union_find_replacet &symbol_solver, const std::vector &equations, @@ -845,7 +845,7 @@ decision_proceduret::resultt string_refinementt::dec_solve() /// Add the given lemma to the solver. /// \param lemma: a Boolean expression /// \param simplify_lemma: whether the lemma should be simplified before being -/// given to the underlying solver. +/// given to the underlying solver. void string_refinementt::add_lemma( const exprt &lemma, const bool simplify_lemma) @@ -892,7 +892,7 @@ void string_refinementt::add_lemma( /// Get a model of an array and put it in a certain form. /// If the model is incomplete or if it is too big, return no value. /// \param super_get: function returning the valuation of an expression -/// in a model +/// in a model /// \param ns: namespace /// \param stream: output stream for warning messages /// \param arr: expression of type array representing a string @@ -1055,7 +1055,7 @@ void debug_model( /// array valuations coming from the underlying solver are given. /// \param index: An index with which to build the equality condition /// \param left_propagate: If set to true, the expression will look like -/// `index<=0 ? 24 : index<=2 ? 42 : 12` +/// `index<=0 ? 24 : index<=2 ? 42 : 12` /// \return An expression containing no 'with' expression static exprt substitute_array_access( const with_exprt &expr, @@ -1162,9 +1162,9 @@ static void substitute_array_access_in_place( /// something like: `index <= 0 ? 24 : index <= 2 ? 42 : 12` /// \param expr: an expression containing array accesses /// \param symbol_generator: function which given a prefix and a type generates -/// a fresh symbol of the given type +/// a fresh symbol of the given type /// \param left_propagate: should values be propagated to the left in with -/// expressions +/// expressions /// \return an expression containing no array access exprt substitute_array_access( exprt expr, @@ -1185,7 +1185,7 @@ exprt substitute_array_access( /// \param constraint: the not_contains constraint to add the negation of /// \param univ_var: the universal variable for the negation of the axiom /// \param get: valuation function, the result should have been simplified -/// \return: the negation of the axiom under the current evaluation +/// \return the negation of the axiom under the current evaluation static exprt negation_of_not_contains_constraint( const string_not_contains_constraintt &constraint, const symbol_exprt &univ_var, @@ -1519,7 +1519,7 @@ exprt simplify_sum(const exprt &f) /// \param qvar: a symbol representing a universally quantified variable /// \param val: an expression /// \param f: an expression containing `+` and `-` -/// operations in which `qvar` should appear exactly once. +/// operations in which `qvar` should appear exactly once. /// \return an expression corresponding of $f^{-1}(val)$ where $f$ is seen as /// a function of $qvar$, i.e. the value that is necessary for `qvar` for `f` /// to be equal to `val`. For instance, if `f` corresponds to the expression @@ -1622,7 +1622,7 @@ static void update_index_set( /// An expression representing an array of characters can be in the form of an /// if expression for instance `cond?array1:(cond2:array2:array3)`. /// We return all the array expressions contained in `array_expr`. -/// \param array_expr : an expression representing an array +/// \param array_expr: an expression representing an array /// \param accu: a vector to which symbols and constant arrays contained in the /// expression will be appended static void get_sub_arrays(const exprt &array_expr, std::vector &accu) @@ -2039,8 +2039,8 @@ exprt string_refinementt::get(const exprt &expr) const /// \param ns: namespace /// \param [in] axiom: the axiom to be checked /// \param [in] var: the variable whose evaluation will be stored in witness -/// \return: the witness of the satisfying assignment if one -/// exists. If UNSAT, then behaviour is undefined. +/// \return the witness of the satisfying assignment if one +/// exists. If UNSAT, then behaviour is undefined. static optionalt find_counter_example( const namespacet &ns, const exprt &axiom, diff --git a/src/solvers/refinement/string_refinement_util.h b/src/solvers/refinement/string_refinement_util.h index 004dd5310d..230c34127f 100644 --- a/src/solvers/refinement/string_refinement_util.h +++ b/src/solvers/refinement/string_refinement_util.h @@ -39,10 +39,9 @@ bool is_char_pointer_type(const typet &type); /// \param type: a type /// \param ns: namespace /// \return true if a subtype of `type` is an pointer of characters. -/// The meaning of "subtype" is in the algebraic datatype sense: -/// for example, the subtypes of a struct are the types of its -/// components, the subtype of a pointer is the type it points to, -/// etc... +/// The meaning of "subtype" is in the algebraic datatype sense: for example, +/// the subtypes of a struct are the types of its components, the subtype of +/// a pointer is the type it points to, etc... bool has_char_pointer_subtype(const typet &type, const namespacet &ns); /// \param expr: an expression diff --git a/src/util/allocate_objects.cpp b/src/util/allocate_objects.cpp index 434d4a1bb1..d9d088791d 100644 --- a/src/util/allocate_objects.cpp +++ b/src/util/allocate_objects.cpp @@ -235,7 +235,7 @@ exprt allocate_objectst::allocate_non_dynamic_object( /// Add a pointer to a symbol to the list of pointers to symbols created so far /// -/// \param symbol_ptr pointer to a symbol in the symbol table +/// \param symbol_ptr: pointer to a symbol in the symbol table void allocate_objectst::add_created_symbol(const symbolt *symbol_ptr) { symbols_created.push_back(symbol_ptr); @@ -243,7 +243,7 @@ void allocate_objectst::add_created_symbol(const symbolt *symbol_ptr) /// Adds declarations for all non-static symbols created /// -/// \param init_code code block to which to add the declarations +/// \param init_code: code block to which to add the declarations void allocate_objectst::declare_created_symbols(code_blockt &init_code) { // Add the following code to init_code for each symbol that's been created: @@ -261,7 +261,7 @@ void allocate_objectst::declare_created_symbols(code_blockt &init_code) /// Adds code to mark the created symbols as input /// -/// \param init_code code block to which to add the generated code +/// \param init_code: code block to which to add the generated code void allocate_objectst::mark_created_symbols_as_input(code_blockt &init_code) { // Add the following code to init_code for each symbol that's been created: diff --git a/src/util/arith_tools.cpp b/src/util/arith_tools.cpp index 12bce90c24..3e16dd4037 100644 --- a/src/util/arith_tools.cpp +++ b/src/util/arith_tools.cpp @@ -324,7 +324,7 @@ static char nibble2hex(unsigned char nibble) /// construct a bit-vector representation from a functor /// \param width: the width of the bit-vector /// \param f: the functor -- the parameter is the bit index -/// \returns new bitvector representation +/// \return new bitvector representation irep_idt make_bvrep(const std::size_t width, const std::function f) { @@ -369,7 +369,7 @@ make_bvrep(const std::size_t width, const std::function f) /// \param b: the representation of the second bit vector /// \param width: the width of the bit-vector /// \param f: the functor -/// \returns new bitvector representation +/// \return new bitvector representation irep_idt bvrep_bitwise_op( const irep_idt &a, const irep_idt &b, @@ -386,7 +386,7 @@ irep_idt bvrep_bitwise_op( /// \param a: the bit-vector representation /// \param width: the width of the bit-vector /// \param f: the functor -/// \returns new bitvector representation +/// \return new bitvector representation irep_idt bvrep_bitwise_op( const irep_idt &a, const std::size_t width, diff --git a/src/util/arith_tools.h b/src/util/arith_tools.h index 50bb593ddf..a015f305a1 100644 --- a/src/util/arith_tools.h +++ b/src/util/arith_tools.h @@ -117,8 +117,8 @@ public: /// Converts an expression to any integral type /// \tparam Target: type to convert to /// \param arg: expression to convert -/// \return optional integer of type Target if conversion is possible, -/// empty optional otherwise. +/// \return optional integer of type Target if conversion is possible, empty +/// optional otherwise. template optionalt numeric_cast(const exprt &arg) { diff --git a/src/util/base_type.cpp b/src/util/base_type.cpp index d2eb388baf..03059cc6f5 100644 --- a/src/util/base_type.cpp +++ b/src/util/base_type.cpp @@ -320,9 +320,9 @@ bool base_type_eqt::base_type_eq_rec( /// - `symbol_typet("a")` and `ns.lookup("a").type` will compare equal, /// - `struct_typet {symbol_typet("a")}` and `struct_typet {ns.lookup("a") /// .type}` will also compare equal. -/// \param type1 The first type to compare. -/// \param type2 The second type to compare. -/// \param ns The namespace, needed for resolution of symbols. +/// \param type1: The first type to compare. +/// \param type2: The second type to compare. +/// \param ns: The namespace, needed for resolution of symbols. bool base_type_eq( const typet &type1, const typet &type2, @@ -333,9 +333,9 @@ bool base_type_eq( } /// Check expressions for equality across all levels of hierarchy. -/// \param expr1 The first expression to compare. -/// \param expr2 The second expression to compare. -/// \param ns The namespace, needed for resolution of symbols. +/// \param expr1: The first expression to compare. +/// \param expr2: The second expression to compare. +/// \param ns: The namespace, needed for resolution of symbols. bool base_type_eq( const exprt &expr1, const exprt &expr2, diff --git a/src/util/config.cpp b/src/util/config.cpp index 42bf2efecb..63583022e0 100644 --- a/src/util/config.cpp +++ b/src/util/config.cpp @@ -1230,7 +1230,7 @@ void configt::set_from_symbol_table( } /// Sets the number of bits used for object addresses -/// \param symbol_table The symbol table +/// \param symbol_table: The symbol table void configt::set_object_bits_from_symbol_table( const symbol_tablet &symbol_table) { diff --git a/src/util/container_utils.h b/src/util/container_utils.h index 629896f573..6406435105 100644 --- a/src/util/container_utils.h +++ b/src/util/container_utils.h @@ -18,11 +18,11 @@ Author: Diffblue Ltd. /// `target.insert(source.begin(), source.end())` which has complexity /// O(n2 * log(n1 + n2)). /// -/// \tparam T value type of the sets -/// \tparam Compare comparison predicate of the sets -/// \tparam Alloc allocator of the sets -/// \param target first input set, will contain the result of the union -/// \param source second input set +/// \tparam T: value type of the sets +/// \tparam Compare: comparison predicate of the sets +/// \tparam Alloc: allocator of the sets +/// \param target: first input set, will contain the result of the union +/// \param source: second input set /// \return true iff `target` was changed template bool util_inplace_set_union( diff --git a/src/util/cow.h b/src/util/cow.h index 1db6469bbc..ac91b35dc1 100644 --- a/src/util/cow.h +++ b/src/util/cow.h @@ -133,7 +133,7 @@ private: /// A helper class to store use-counts of copy-on-write objects. /// The suggested usage pattern is to have copy-on-write data types inherit /// from this class, and then to access them through a copy_on_writet. -/// \tparam Num some numeric type, used to store a reference count +/// \tparam Num: some numeric type, used to store a reference count template class copy_on_write_pointeet { diff --git a/src/util/expr.cpp b/src/util/expr.cpp index 4a44a3b453..6509fe501c 100644 --- a/src/util/expr.cpp +++ b/src/util/expr.cpp @@ -225,7 +225,7 @@ bool exprt::is_one() const /// (non-recursively). /// If no source location is found, a nil `source_locationt` is returned. /// \return A source location if found in the expression or its operands, nil -/// otherwise. +/// otherwise. const source_locationt &exprt::find_source_location() const { const source_locationt &l=source_location(); diff --git a/src/util/expr_cast.h b/src/util/expr_cast.h index 31c1ac5771..1bbf823680 100644 --- a/src/util/expr_cast.h +++ b/src/util/expr_cast.h @@ -24,8 +24,8 @@ Author: Nathan Phillips /// /// Implement template specializations of this function to enable casting /// -/// \tparam T The exprt-derived class to check for -/// \param base Reference to a generic \ref exprt +/// \tparam T: The exprt-derived class to check for +/// \param base: Reference to a generic \ref exprt /// \return true if \a base is of type \a T template inline bool can_cast_expr(const exprt &base); @@ -34,8 +34,8 @@ template inline bool can_cast_expr(const exprt &base); /// /// Implement template specializations of this function to enable casting /// -/// \tparam T The typet-derived class to check for -/// \param base Reference to a generic \ref typet +/// \tparam T: The typet-derived class to check for +/// \param base: Reference to a generic \ref typet /// \return true if \a base is of type \a T template inline bool can_cast_type(const typet &base); @@ -81,10 +81,10 @@ struct expr_try_dynamic_cast_return_typet final /// \brief Try to cast a reference to a generic exprt to a specific derived /// class -/// \tparam T The reference or const reference type to \a TUnderlying to cast +/// \tparam T: The reference or const reference type to \a TUnderlying to cast /// to -/// \tparam TExpr The original type to cast from, either exprt or const exprt -/// \param base Reference to a generic \ref exprt +/// \tparam TExpr: The original type to cast from, either exprt or const exprt +/// \param base: Reference to a generic \ref exprt /// \return Ptr to object of type \a TUnderlying /// or nullptr if \a base is not an instance of \a TUnderlying template @@ -108,11 +108,11 @@ auto expr_try_dynamic_cast(TExpr &base) } /// \brief Try to cast a reference to a generic typet to a specific derived -/// class -/// \tparam T The reference or const reference type to \a TUnderlying to cast -/// to -/// \tparam TType The original type to cast from, either typet or const typet -/// \param base Reference to a generic \ref typet +/// class +/// \tparam T: The reference or const reference type to \a TUnderlying to cast +/// to +/// \tparam TType: The original type to cast from, either typet or const typet +/// \param base: Reference to a generic \ref typet /// \return Ptr to object of type \a TUnderlying /// or nullptr if \a base is not an instance of \a TUnderlying template @@ -156,9 +156,10 @@ struct expr_dynamic_cast_return_typet final } // namespace detail /// \brief Cast a reference to a generic exprt to a specific derived class. -/// \tparam T The reference or const reference type to \a TUnderlying to cast to -/// \tparam TExpr The original type to cast from, either exprt or const exprt -/// \param base Reference to a generic \ref exprt +/// \tparam T: The reference or const reference type to \a TUnderlying to cast +/// to +/// \tparam TExpr: The original type to cast from, either exprt or const exprt +/// \param base: Reference to a generic \ref exprt /// \return Reference to object of type \a T /// \throw std::bad_cast If \a base is not an instance of \a TUnderlying template @@ -173,9 +174,10 @@ auto expr_dynamic_cast(TExpr &base) /// \brief Cast a reference to a generic exprt to a specific derived class. /// Also assert that the expression has the expected type. -/// \tparam T The reference or const reference type to \a TUnderlying to cast to -/// \tparam TExpr The original type to cast from, either exprt or const exprt -/// \param base Reference to a generic \ref exprt +/// \tparam T: The reference or const reference type to \a TUnderlying to cast +/// to +/// \tparam TExpr: The original type to cast from, either exprt or const exprt +/// \param base: Reference to a generic \ref exprt /// \return Reference to object of type \a T /// \throw std::bad_cast If \a base is not an instance of \a TUnderlying /// \remark If CBMC assertions (PRECONDITION) are set to abort then this will @@ -190,9 +192,10 @@ auto expr_checked_cast(TExpr &base) /// \brief Cast a reference to a generic typet to a specific derived class and /// checks that the type could be converted. -/// \tparam T The reference or const reference type to \a TUnderlying to cast to -/// \tparam TType The original type to cast from, either typet or const typet -/// \param base Reference to a generic \ref typet +/// \tparam T: The reference or const reference type to \a TUnderlying to cast +/// to +/// \tparam TType: The original type to cast from, either typet or const typet +/// \param base: Reference to a generic \ref typet /// \return Reference to object of type \a T template auto type_checked_cast(TType &base) -> diff --git a/src/util/expr_initializer.cpp b/src/util/expr_initializer.cpp index 2506b0c969..364d8db1b2 100644 --- a/src/util/expr_initializer.cpp +++ b/src/util/expr_initializer.cpp @@ -318,7 +318,7 @@ exprt expr_initializert::expr_initializer_rec( /// \param source_location: Location to record in all created sub-expressions. /// \param ns: Namespace to perform type symbol/tag lookups. /// \return An expression if a constant expression of the input type can be -/// built. +/// built. optionalt zero_initializer( const typet &type, const source_locationt &source_location, @@ -338,7 +338,7 @@ optionalt zero_initializer( /// \param source_location: Location to record in all created sub-expressions. /// \param ns: Namespace to perform type symbol/tag lookups. /// \return An expression if a non-deterministic expression of the input type -/// can be built. +/// can be built. optionalt nondet_initializer( const typet &type, const source_locationt &source_location, diff --git a/src/util/expr_iterator.h b/src/util/expr_iterator.h index c8ab84e27d..3de5faab3b 100644 --- a/src/util/expr_iterator.h +++ b/src/util/expr_iterator.h @@ -206,8 +206,7 @@ protected: /// If overridden, this function should be called from the inheriting /// class by the override function /// \return true if element was successfully pushed onto the stack, - /// false otherwise - /// If returning false, child will not be iterated over + /// false otherwise. If returning false, child will not be iterated over. bool push_expr(const exprt &expr) { m_stack.emplace_back(expr, expr.operands().begin(), expr.operands().end()); @@ -272,7 +271,7 @@ public: /// by the iterator. /// If the iterator is currently using a const root exprt then calls /// mutate_root to get a non-const root and copies it if it is shared - /// \returns A non-const reference to the element this iterator is + /// \return A non-const reference to the element this iterator is /// currently pointing to exprt &mutate() { diff --git a/src/util/expr_util.h b/src/util/expr_util.h index f65643474a..bc0b509907 100644 --- a/src/util/expr_util.h +++ b/src/util/expr_util.h @@ -57,13 +57,12 @@ bool has_subexpr(const exprt &, const irep_idt &); /// \param pred: a predicate /// \param ns: namespace for symbol type lookups /// \return true if one of the subtype of `type` satisfies predicate `pred`. -/// The meaning of "subtype" is in the algebraic datatype sense: -/// for example, the subtypes of a struct are the types of its -/// components, the subtype of a pointer is the type it points to, -/// etc... -/// For instance in the type `t` defined by -/// `{ int a; char[] b; double * c; { bool d} e}`, `int`, `char`, -/// `double` and `bool` are subtypes of `t`. +/// The meaning of "subtype" is in the algebraic datatype sense: for example, +/// the subtypes of a struct are the types of its components, the subtype of +/// a pointer is the type it points to, etc... +/// For instance in the type `t` defined by +/// `{ int a; char[] b; double * c; { bool d} e}`, `int`, `char`, +/// `double` and `bool` are subtypes of `t`. bool has_subtype( const typet &type, const std::function &pred, diff --git a/src/util/graph.h b/src/util/graph.h index 69971d8ab2..a055205415 100644 --- a/src/util/graph.h +++ b/src/util/graph.h @@ -590,9 +590,9 @@ void get_reachable( /// Run depth-first search on the graph, starting from a single source /// node. -/// \param src The node to start the search from. -/// \param forwards true (false) if the forward (backward) reachability -/// should be performed. +/// \param src: The node to start the search from. +/// \param forwards: true (false) if the forward (backward) reachability +/// should be performed. template std::vector grapht::get_reachable(node_indext src, bool forwards) const @@ -605,9 +605,9 @@ grapht::get_reachable(node_indext src, bool forwards) const /// Run depth-first search on the graph, starting from multiple source /// nodes. -/// \param src The nodes to start the search from. -/// \param forwards true (false) if the forward (backward) reachability -/// should be performed. +/// \param src: The nodes to start the search from. +/// \param forwards: true (false) if the forward (backward) reachability +/// should be performed. template std::vector grapht::get_reachable( const std::vector &src, @@ -642,8 +642,8 @@ std::vector grapht::get_reachable( /// Run recursive depth-limited search on the graph, starting /// from multiple source nodes, to find the nodes reachable within n steps. /// This function initialises the search. -/// \param src The node to start the search from. -/// \param limit limit on steps +/// \param src: The node to start the search from. +/// \param limit: limit on steps /// \return a vector of reachable node indices template std::vector grapht::depth_limited_search( @@ -657,8 +657,8 @@ std::vector grapht::depth_limited_search( /// Run recursive depth-limited search on the graph, starting /// from multiple source nodes, to find the nodes reachable within n steps. /// This function initialises the search. -/// \param src The nodes to start the search from. -/// \param limit limit on steps +/// \param src: The nodes to start the search from. +/// \param limit: limit on steps /// \return a vector of reachable node indices template std::vector grapht::depth_limited_search( @@ -677,10 +677,11 @@ std::vector grapht::depth_limited_search( } /// Run recursive depth-limited search on the graph, starting -// from multiple source nodes, to find the nodes reachable within n steps -/// \param src The nodes to start the search from. -/// \param limit limit on steps -/// \param visited vector of booleans indicating whether a node has been visited +/// from multiple source nodes, to find the nodes reachable within n steps +/// \param src: The nodes to start the search from. +/// \param limit: limit on steps +/// \param visited: vector of booleans indicating whether a node has been +/// visited /// \return a vector of reachable node indices template std::vector grapht::depth_limited_search( @@ -819,7 +820,7 @@ void grapht::tarjan(tarjant &t, node_indext v) const /// Lower-numbered SCCs are closer to the leaves, so in the particular case /// of a DAG, sorting by SCC number gives a topological sort, and for a cyclic /// graph the SCCs are topologically sorted but arbitrarily ordered internally. -/// \param subgraph_nr [in, out]: should be pre-allocated with enough storage +/// \param [in,out] subgraph_nr: should be pre-allocated with enough storage /// for one entry per graph node. Will be populated with the SCC indices of /// each node. /// \return the number of distinct SCCs. diff --git a/src/util/invariant.h b/src/util/invariant.h index 2d8383200c..ce63707a63 100644 --- a/src/util/invariant.h +++ b/src/util/invariant.h @@ -206,11 +206,11 @@ void report_exception_to_stderr(const invariant_failedt &); /// reason.what() (which therefore includes the backtrace). /// In future this may throw `reason` instead of aborting. /// Template parameter ET: type of exception to construct -/// \param file : C string giving the name of the file. -/// \param function : C string giving the name of the function. -/// \param line : The line number of the invariant -/// \param condition : the condition this invariant is checking. -/// \param params : (variadic) parameters to forward to ET's constructor +/// \param file: C string giving the name of the file. +/// \param function: C string giving the name of the function. +/// \param line: The line number of the invariant +/// \param condition: the condition this invariant is checking. +/// \param params: (variadic) parameters to forward to ET's constructor /// its backtrace member will be set before it is used. template CBMC_NORETURN @@ -240,11 +240,11 @@ CBMC_NORETURN /// It constructs an invariant_violatedt from reason and the /// backtrace, then aborts after printing the invariant's description. /// In future this may throw rather than aborting. -/// \param file : C string giving the name of the file. -/// \param function : C string giving the name of the function. -/// \param line : The line number of the invariant -/// \param reason : brief description of the invariant violation. -/// \param condition : the condition this invariant is checking. +/// \param file: C string giving the name of the file. +/// \param function: C string giving the name of the function. +/// \param line: The line number of the invariant +/// \param reason: brief description of the invariant violation. +/// \param condition: the condition this invariant is checking. CBMC_NORETURN inline void invariant_violated_string( diff --git a/src/util/json_irep.cpp b/src/util/json_irep.cpp index 1e23aa7be5..57b97258d3 100644 --- a/src/util/json_irep.cpp +++ b/src/util/json_irep.cpp @@ -20,7 +20,7 @@ Author: Thomas Kiley, thomas.kiley@diffblue.com /// To convert to JSON from an irep structure by recursively generating JSON /// for the different sub trees. /// \param _include_comments: when writing JSON, should the comments -/// sub tree be included. +/// sub tree be included. json_irept::json_irept(bool _include_comments): include_comments(_include_comments) { @@ -29,7 +29,7 @@ json_irept::json_irept(bool _include_comments): /// To convert to JSON from an irep structure by recursively generating JSON /// for the different sub trees. /// \param irep: The irep structure to turn into json -/// \return: The json object. +/// \return The json object. json_objectt json_irept::convert_from_irep(const irept &irep) const { json_objectt irep_object; diff --git a/src/util/json_stream.h b/src/util/json_stream.h index 40776fcbc6..7c70786d65 100644 --- a/src/util/json_stream.h +++ b/src/util/json_stream.h @@ -158,7 +158,7 @@ public: /// Lookup the key of a non-streaming JSON element. /// \param key: The key to be looked up inside the /// attributes of the JSON object. - /// \return: The value that corresponds to the key + /// \return The value that corresponds to the key /// if found, a null_json_object otherwise. const jsont &operator[](const std::string &key) const { diff --git a/src/util/mathematical_types.h b/src/util/mathematical_types.h index 44243c5451..9378277cca 100644 --- a/src/util/mathematical_types.h +++ b/src/util/mathematical_types.h @@ -100,8 +100,8 @@ public: }; /// Check whether a reference to a typet is a \ref mathematical_function_typet. -/// \param type Source type. -/// \return True if \param type is a \ref mathematical_function_typet. +/// \param type: Source type. +/// \return True if \p type is a \ref mathematical_function_typet. template <> inline bool can_cast_type(const typet &type) { @@ -114,7 +114,7 @@ inline bool can_cast_type(const typet &type) /// mathematical_function_typet. Will fail with a precondition violation if type /// doesn't match. /// -/// \param type Source type. +/// \param type: Source type. /// \return Object of type \ref mathematical_function_typet. inline const mathematical_function_typet & to_mathematical_function_type(const typet &type) diff --git a/src/util/message.cpp b/src/util/message.cpp index 88691a9632..daf0b813f7 100644 --- a/src/util/message.cpp +++ b/src/util/message.cpp @@ -91,9 +91,9 @@ const messaget::commandt messaget::bright_cyan(96); /// Parse a (user-)provided string as a verbosity level and set it as the /// verbosity of dest. -/// \param user_input Input string; if empty, the default verbosity is used. -/// \param default_verbosity Verbosity to use if no value is provided. -/// \param dest message handler the verbosity of which is to be set. +/// \param user_input: Input string; if empty, the default verbosity is used. +/// \param default_verbosity: Verbosity to use if no value is provided. +/// \param dest: message handler the verbosity of which is to be set. /// \return Computed verbosity unsigned messaget::eval_verbosity( const std::string &user_input, @@ -127,8 +127,8 @@ unsigned messaget::eval_verbosity( /// configured verbosity is at least as high as that of \p message_stream. Use /// whenever generating output involves additional computational effort that /// should only be spent when such output will actually be displayed. -/// \param message_stream Output message stream -/// \param output_generator Function generating output +/// \param message_stream: Output message stream +/// \param output_generator: Function generating output void messaget::conditional_output( mstreamt &message_stream, const std::function &output_generator) const diff --git a/src/util/message.h b/src/util/message.h index 151647baf4..112996b29d 100644 --- a/src/util/message.h +++ b/src/util/message.h @@ -137,7 +137,7 @@ protected: /// Common practice is to inherit from the \ref messaget class, to provide /// local infrastructure for messaging, by calling one of the utility /// methods, e.g. `debug()`, `warning()` etc. - which return a reference to a -// new instance of `mstreamt` set with the appropriate level. +/// new instance of `mstreamt` set with the appropriate level. /// Individual messages are stored in \ref mstreamt - an `ostringstream` /// subtype. \ref eomt is used to flush the internal string of \ref mstreamt. /// A static member `eom`, of \ref eomt type is provided. diff --git a/src/util/namespace.h b/src/util/namespace.h index ee6d15f5ed..c7555a8d39 100644 --- a/src/util/namespace.h +++ b/src/util/namespace.h @@ -39,7 +39,7 @@ public: /// Lookup a symbol in the namespace. /// \param name: The name of the symbol to lookup. - /// \return: A reference to the symbol found. + /// \return A reference to the symbol found. /// \remarks: It is a PRECONDITION that the symbol name exists /// in the namespace. const symbolt &lookup(const irep_idt &name) const @@ -81,7 +81,7 @@ public: /// returned. With multiple symbol tables, `symbol_table1` is searched first /// and then symbol_table2. /// \return False iff the requested symbol is found in at least one of the - /// tables. + /// tables. virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const=0; }; @@ -161,7 +161,7 @@ public: /// Add symbol table to the list of symbol tables this multi-namespace /// is working with. /// \param symbol_table: Reference to the symbol table to be added to this - /// namespace. + /// namespace. void add(const symbol_table_baset &symbol_table) { symbol_table_list.push_back(&symbol_table); diff --git a/src/util/nondet.cpp b/src/util/nondet.cpp index 5b179d0510..e1dc471b15 100644 --- a/src/util/nondet.cpp +++ b/src/util/nondet.cpp @@ -29,7 +29,7 @@ Author: Diffblue Ltd. /// \param mode: Mode (language) of the symbol to be generated. /// \param source_location: The location to mark the generated int with. /// \param symbol_table: The global symbol table. -/// \param instructions [out]: Output instructions are written to +/// \param [out] instructions: Output instructions are written to /// 'instructions'. These declare, nondet-initialise and range-constrain (with /// assume statements) a fresh integer. /// \return Returns a symbol expression for the resulting integer. diff --git a/src/util/nondet_bool.h b/src/util/nondet_bool.h index 8827d83ead..d5be6abd8a 100644 --- a/src/util/nondet_bool.h +++ b/src/util/nondet_bool.h @@ -15,8 +15,8 @@ Author: Chris Smowton, chris@smowton.net #include "std_expr.h" #include "std_types.h" -/// \param type desired type (C_bool or plain bool) -/// \param source_location source location +/// \param type: desired type (C_bool or plain bool) +/// \param source_location: source location /// \return nondet expr of that type inline exprt get_nondet_bool(const typet &type, const source_locationt &source_location) diff --git a/src/util/numbering.h b/src/util/numbering.h index 42e18354e2..b658bc299c 100644 --- a/src/util/numbering.h +++ b/src/util/numbering.h @@ -16,7 +16,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "invariant.h" #include "optional.h" -/// \tparam Map a map from a key type to some numeric type +/// \tparam Map: a map from a key type to some numeric type template class template_numberingt final { diff --git a/src/util/object_factory_parameters.cpp b/src/util/object_factory_parameters.cpp index e9aab0b9fa..b3ae8ecf35 100644 --- a/src/util/object_factory_parameters.cpp +++ b/src/util/object_factory_parameters.cpp @@ -49,8 +49,8 @@ void object_factory_parameterst::set(const optionst &options) } /// Parse the object factory parameters from a given command line -/// \param cmdline Command line -/// \param [out] options The options object that will be updated. +/// \param cmdline: Command line +/// \param [out] options: The options object that will be updated. void parse_object_factory_options(const cmdlinet &cmdline, optionst &options) { if(cmdline.isset("max-nondet-array-length")) diff --git a/src/util/sharing_map.h b/src/util/sharing_map.h index ebd591408a..ecae777392 100644 --- a/src/util/sharing_map.h +++ b/src/util/sharing_map.h @@ -520,7 +520,7 @@ SHARING_MAPT(std::size_t) /// \param begin: begin iterator /// \param end: end iterator /// \param f: function applied to the iterator to get a sharing map -/// \return: sharing stats +/// \return sharing stats SHARING_MAPT3(Iterator, , sharing_map_statst) ::get_sharing_stats( Iterator begin, @@ -574,7 +574,7 @@ SHARING_MAPT3(Iterator, , sharing_map_statst) /// /// \param begin: begin iterator of a map /// \param end: end iterator of a map -/// \return: sharing stats +/// \return sharing stats SHARING_MAPT3(Iterator, , sharing_map_statst) ::get_sharing_stats_map(Iterator begin, Iterator end) { @@ -590,7 +590,7 @@ SHARING_MAPT3(Iterator, , sharing_map_statst) /// - Worst case: O(N * H * log(S)) /// - Best case: O(N + H) /// -/// \param[out] view: Empty view +/// \param [out] view: Empty view SHARING_MAPT(void)::get_view(viewt &view) const { SM_ASSERT(view.empty()); @@ -645,7 +645,7 @@ SHARING_MAPT(void) /// The symbols N1, M1 refer to map A, and symbols N2, M2 refer to map B. /// /// \param other: other map -/// \param[out] delta_view: Empty delta view +/// \param [out] delta_view: Empty delta view /// \param only_common: Indicates if the returned delta view should only /// contain key-value pairs for keys that exist in both maps SHARING_MAPT(void) diff --git a/src/util/small_map.h b/src/util/small_map.h index c8845dfb23..ad5f2e3084 100644 --- a/src/util/small_map.h +++ b/src/util/small_map.h @@ -96,10 +96,10 @@ struct indicator_maskt> /// * useful: 48 B /// * total: 64 B /// -/// \tparam T mapped type -/// \tparam Ind unsigned integer type, used to map integer indices to internal +/// \tparam T: mapped type +/// \tparam Ind: unsigned integer type, used to map integer indices to internal /// indices that index into the memory block that stores the mapped values -/// \tparam Num gives range of valid indices, i.e., the valid indices are {0, +/// \tparam Num: gives range of valid indices, i.e., the valid indices are {0, /// ..., Num-1}, must satisfy Num * num_bits(Num-1) + Num < sizeof(Ind) * 8, /// with num_bits(n) denoting the minimum number of bits required to represent /// integer n diff --git a/src/util/small_shared_ptr.h b/src/util/small_shared_ptr.h index fbc61a0572..556b4620d2 100644 --- a/src/util/small_shared_ptr.h +++ b/src/util/small_shared_ptr.h @@ -177,7 +177,7 @@ bool operator>=( /// This approach provides us with shared_ptr-like semantics, but without the /// space overhead required by shared_ptr. The idea is similar to /// boost's intrusive_ptr. -/// \tparam Num some numeric type, used to store a reference count +/// \tparam Num: some numeric type, used to store a reference count template class small_shared_pointeet { diff --git a/src/util/source_location.cpp b/src/util/source_location.cpp index b564c4089e..7db8bd96ca 100644 --- a/src/util/source_location.cpp +++ b/src/util/source_location.cpp @@ -73,7 +73,7 @@ void source_locationt::merge(const source_locationt &from) /// Get a path to the file, including working directory. /// \return Full path unless the file name is empty or refers -/// to a built-in, in which case {} is returned. +/// to a built-in, in which case {} is returned. optionalt source_locationt::full_path() const { const auto file = id2string(get_file()); diff --git a/src/util/ssa_expr.h b/src/util/ssa_expr.h index 136065fcfe..4a9547cc26 100644 --- a/src/util/ssa_expr.h +++ b/src/util/ssa_expr.h @@ -12,8 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "std_expr.h" -/*! \brief Expression providing an SSA-renamed symbol of expressions -*/ +/// Expression providing an SSA-renamed symbol of expressions class ssa_exprt:public symbol_exprt { public: @@ -22,9 +21,8 @@ public: set(ID_C_SSA_symbol, true); } - /*! \brief Constructor - * \param expr Expression to be converted to SSA symbol - */ + /// Constructor + /// \param expr: Expression to be converted to SSA symbol explicit ssa_exprt(const exprt &expr): symbol_exprt(expr.type()) { @@ -121,8 +119,8 @@ public: void update_identifier(); - /* Used to determine whether or not an identifier can be built - * before trying and getting an exception */ + /// Used to determine whether or not an identifier can be built before trying + /// and getting an exception static bool can_build_identifier(const exprt &src); static void check( @@ -147,16 +145,11 @@ public: } }; -/*! \brief Cast a generic exprt to an \ref ssa_exprt - * - * This is an unchecked conversion. \a expr must be known to be \ref - * ssa_exprt. - * - * \param expr Source expression - * \return Object of type \ref ssa_exprt - * - * \ingroup gr_std_expr -*/ +/// Cast a generic exprt to an \ref ssa_exprt. This is an unchecked conversion. +/// \a expr must be known to be \ref ssa_exprt. +/// \param expr: Source expression +/// \return Object of type \ref ssa_exprt +/// \ingroup gr_std_expr inline const ssa_exprt &to_ssa_expr(const exprt &expr) { PRECONDITION( @@ -165,9 +158,8 @@ inline const ssa_exprt &to_ssa_expr(const exprt &expr) return static_cast(expr); } -/*! \copydoc to_ssa_expr(const exprt &) - * \ingroup gr_std_expr -*/ +/// \copydoc to_ssa_expr(const exprt &) +/// \ingroup gr_std_expr inline ssa_exprt &to_ssa_expr(exprt &expr) { PRECONDITION( diff --git a/src/util/std_code.h b/src/util/std_code.h index 49b1ae8abf..0d2a5bc0cc 100644 --- a/src/util/std_code.h +++ b/src/util/std_code.h @@ -606,7 +606,7 @@ inline void validate_expr(const code_assertt &x) /// conventionally this should have `comment` and `property_class` fields set /// to indicate the nature of the assertion. /// \return A code block that asserts a condition then aborts if it does not -/// hold. +/// hold. code_blockt create_fatal_assertion( const exprt &condition, const source_locationt &source_location); diff --git a/src/util/std_expr.h b/src/util/std_expr.h index 5d6d692ddd..f5da4265ca 100644 --- a/src/util/std_expr.h +++ b/src/util/std_expr.h @@ -629,7 +629,7 @@ inline void validate_expr(const bswap_exprt &value) } /// \brief A base class for expressions that are predicates, -/// i.e., Boolean-typed. +/// i.e., Boolean-typed. class predicate_exprt:public exprt { public: @@ -662,7 +662,7 @@ public: }; /// \brief A base class for expressions that are predicates, -/// i.e., Boolean-typed, and that take exactly one argument. +/// i.e., Boolean-typed, and that take exactly one argument. class unary_predicate_exprt:public unary_exprt { public: @@ -829,9 +829,8 @@ template<> inline bool can_cast_expr(const exprt &base) return base.operands().size()==2; } - /// \brief A base class for expressions that are predicates, -/// i.e., Boolean-typed, and that take exactly two arguments. +/// i.e., Boolean-typed, and that take exactly two arguments. class binary_predicate_exprt:public binary_exprt { public: @@ -3507,10 +3506,9 @@ inline void validate_expr(const if_exprt &value) validate_operands(value, 3, "If-then-else must have three operands"); } - /// \brief Operator to update elements in structs and arrays /// \remark This expression will eventually be replaced by separate -/// array and struct update operators. +/// array and struct update operators. class with_exprt:public exprt { public: diff --git a/src/util/std_types.cpp b/src/util/std_types.cpp index b7804ac1d8..77cc1f73a4 100644 --- a/src/util/std_types.cpp +++ b/src/util/std_types.cpp @@ -101,7 +101,7 @@ optionalt struct_typet::get_base(const irep_idt &id) const /// Returns true if the struct is a prefix of \a other, i.e., if this struct /// has n components then the component types and names of this struct must /// match the first n components of \a other struct. -/// \param other Struct type to compare with. +/// \param other: Struct type to compare with. bool struct_typet::is_prefix_of(const struct_typet &other) const { const componentst &ot_components=other.components(); @@ -217,8 +217,8 @@ constant_exprt unsignedbv_typet::largest_expr() const /// - const int a; /// - struct contains_constant_pointer { int x; int * const p; }; /// - const int b[3]; -/// \param type The type we want to query constness of. -/// \param ns The namespace, needed for resolution of symbols. +/// \param type: The type we want to query constness of. +/// \param ns: The namespace, needed for resolution of symbols. /// \return Whether passed in type is const or not. bool is_constant_or_has_constant_components( const typet &type, diff --git a/src/util/std_types.h b/src/util/std_types.h index 554f13544f..7b0a28d467 100644 --- a/src/util/std_types.h +++ b/src/util/std_types.h @@ -79,7 +79,7 @@ public: }; /// Check whether a reference to a typet is a \ref symbol_typet. -/// \param type Source type. +/// \param type: Source type. /// \return True if \p type is a \ref symbol_typet. template <> inline bool can_cast_type(const typet &type) @@ -93,7 +93,7 @@ inline bool can_cast_type(const typet &type) /// \ref symbol_typet. Will fail with a precondition violation if type /// doesn't match. /// -/// \param type Source type. +/// \param type: Source type. /// \return Object of type \ref symbol_typet. inline const symbol_typet &to_symbol_type(const typet &type) { @@ -241,7 +241,7 @@ public: }; /// Check whether a reference to a typet is a \ref struct_union_typet. -/// \param type Source type. +/// \param type: Source type. /// \return True if \p type is a \ref struct_union_typet. template <> inline bool can_cast_type(const typet &type) @@ -255,7 +255,7 @@ inline bool can_cast_type(const typet &type) /// struct_union_typet. Will fail with a precondition violation if type /// doesn't match. /// -/// \param type Source type +/// \param type: Source type /// \return Object of type \ref struct_union_typet inline const struct_union_typet &to_struct_union_type(const typet &type) { @@ -316,7 +316,7 @@ public: void add_base(const struct_tag_typet &base); /// Return the base with the given name, if exists. - /// \param id The name of the base we are looking for. + /// \param id: The name of the base we are looking for. /// \return The base if exists. optionalt get_base(const irep_idt &id) const; @@ -330,7 +330,7 @@ public: }; /// Check whether a reference to a typet is a \ref struct_typet. -/// \param type Source type. +/// \param type: Source type. /// \return True if \p type is a \ref struct_typet. template <> inline bool can_cast_type(const typet &type) @@ -344,7 +344,7 @@ inline bool can_cast_type(const typet &type) /// struct_typet. Will fail with a precondition violation if type /// doesn't match. /// -/// \param type Source type. +/// \param type: Source type. /// \return Object of type \ref struct_typet. inline const struct_typet &to_struct_type(const typet &type) { @@ -390,7 +390,7 @@ public: }; /// Check whether a reference to a typet is a \ref class_typet. -/// \param type Source type. +/// \param type: Source type. /// \return True if \p type is a \ref class_typet. template <> inline bool can_cast_type(const typet &type) @@ -404,7 +404,7 @@ inline bool can_cast_type(const typet &type) /// class_typet. Will fail with a precondition violation if type /// doesn't match. /// -/// \param type Source type. +/// \param type: Source type. /// \return Object of type \ref class_typet. inline const class_typet &to_class_type(const typet &type) { @@ -431,7 +431,7 @@ public: }; /// Check whether a reference to a typet is a \ref union_typet. -/// \param type Source type. +/// \param type: Source type. /// \return True if \p type is a \ref union_typet. template <> inline bool can_cast_type(const typet &type) @@ -445,7 +445,7 @@ inline bool can_cast_type(const typet &type) /// union_typet. Will fail with a precondition violation if type /// doesn't match. /// -/// \param type Source type. +/// \param type: Source type. /// \return Object of type \ref union_typet inline const union_typet &to_union_type(const typet &type) { @@ -483,7 +483,7 @@ public: }; /// Check whether a reference to a typet is a \ref tag_typet. -/// \param type Source type. +/// \param type: Source type. /// \return True if \p type is a \ref tag_typet. template <> inline bool can_cast_type(const typet &type) @@ -498,7 +498,7 @@ inline bool can_cast_type(const typet &type) /// tag_typet. Will fail with a precondition violation if type /// doesn't match. /// -/// \param type Source type. +/// \param type: Source type. /// \return Object of type \ref tag_typet. inline const tag_typet &to_tag_type(const typet &type) { @@ -524,7 +524,7 @@ public: }; /// Check whether a reference to a typet is a \ref struct_tag_typet. -/// \param type Source type. +/// \param type: Source type. /// \return True if \p type is a \ref struct_tag_typet. template <> inline bool can_cast_type(const typet &type) @@ -538,7 +538,7 @@ inline bool can_cast_type(const typet &type) /// struct_tag_typet. Will fail with a precondition violation if type /// doesn't match. /// -/// \param type Source type. +/// \param type: Source type. /// \return Object of type \ref struct_tag_typet inline const struct_tag_typet &to_struct_tag_type(const typet &type) { @@ -564,7 +564,7 @@ public: }; /// Check whether a reference to a typet is a \ref union_tag_typet. -/// \param type Source type. +/// \param type: Source type. /// \return True if \p type is a \ref union_tag_typet. template <> inline bool can_cast_type(const typet &type) @@ -578,7 +578,7 @@ inline bool can_cast_type(const typet &type) /// union_tag_typet. Will fail with a precondition violation if type /// doesn't match. /// -/// \param type Source type. +/// \param type: Source type. /// \return Object of type \ref union_tag_typet. inline const union_tag_typet &to_union_tag_type(const typet &type) { @@ -614,7 +614,7 @@ public: }; /// Check whether a reference to a typet is a \ref enumeration_typet. -/// \param type Source type. +/// \param type: Source type. /// \return True if \p type is a \ref enumeration_typet. template <> inline bool can_cast_type(const typet &type) @@ -628,7 +628,7 @@ inline bool can_cast_type(const typet &type) /// enumeration_typet. Will fail with a precondition violation if type /// doesn't match. /// -/// \param type Source type. +/// \param type: Source type. /// \return Object of type \ref enumeration_typet. inline const enumeration_typet &to_enumeration_type(const typet &type) { @@ -678,7 +678,7 @@ public: }; /// Check whether a reference to a typet is a \ref c_enum_typet. -/// \param type Source type. +/// \param type: Source type. /// \return True if \p type is a \ref c_enum_typet. template <> inline bool can_cast_type(const typet &type) @@ -692,7 +692,7 @@ inline bool can_cast_type(const typet &type) /// c_enum_typet. Will fail with a precondition violation if type /// doesn't match. /// -/// \param type Source type. +/// \param type: Source type. /// \return Object of type \ref c_enum_typet. inline const c_enum_typet &to_c_enum_type(const typet &type) { @@ -718,7 +718,7 @@ public: }; /// Check whether a reference to a typet is a \ref c_enum_tag_typet. -/// \param type Source type. +/// \param type: Source type. /// \return True if \p type is a \ref c_enum_tag_typet. template <> inline bool can_cast_type(const typet &type) @@ -732,7 +732,7 @@ inline bool can_cast_type(const typet &type) /// c_enum_tag_typet. Will fail with a precondition violation if type /// doesn't match. /// -/// \param type Source type. +/// \param type: Source type. /// \return Object of type \ref c_enum_tag_typet. inline const c_enum_tag_typet &to_c_enum_tag_type(const typet &type) { @@ -755,8 +755,8 @@ public: typedef std::vector parameterst; /// Constructs a new code type, i.e., function type. - /// \param _parameters The vector of function parameters. - /// \param _return_type The return type. + /// \param _parameters: The vector of function parameters. + /// \param _return_type: The return type. code_typet(parameterst &&_parameters, typet &&_return_type) : typet(ID_code) { parameters().swap(_parameters); @@ -764,8 +764,8 @@ public: } /// Constructs a new code type, i.e., function type. - /// \param _parameters The vector of function parameters. - /// \param _return_type The return type. + /// \param _parameters: The vector of function parameters. + /// \param _return_type: The return type. code_typet(parameterst &&_parameters, const typet &_return_type) : typet(ID_code) { @@ -963,7 +963,7 @@ public: }; /// Check whether a reference to a typet is a \ref code_typet. -/// \param type Source type. +/// \param type: Source type. /// \return True if \p type is a \ref code_typet. template <> inline bool can_cast_type(const typet &type) @@ -977,7 +977,7 @@ inline bool can_cast_type(const typet &type) /// code_typet. Will fail with a precondition violation if type /// doesn't match. /// -/// \param type Source type. +/// \param type: Source type. /// \return Object of type \ref code_typet. inline const code_typet &to_code_type(const typet &type) { @@ -1029,7 +1029,7 @@ public: }; /// Check whether a reference to a typet is a \ref array_typet. -/// \param type Source type. +/// \param type: Source type. /// \return True if \p type is a \ref array_typet. template <> inline bool can_cast_type(const typet &type) @@ -1043,7 +1043,7 @@ inline bool can_cast_type(const typet &type) /// array_typet. Will fail with a precondition violation if type /// doesn't match. /// -/// \param type Source type. +/// \param type: Source type. /// \return Object of type \ref array_typet. inline const array_typet &to_array_type(const typet &type) { @@ -1095,7 +1095,7 @@ public: }; /// Check whether a reference to a typet is a \ref bitvector_typet. -/// \param type Source type. +/// \param type: Source type. /// \return True if \p type is a \ref bitvector_typet. template <> inline bool can_cast_type(const typet &type) @@ -1114,7 +1114,7 @@ inline bool can_cast_type(const typet &type) /// bitvector_typet. Will fail with a precondition violation if type /// doesn't match. /// -/// \param type Source type. +/// \param type: Source type. /// \return Object of type \ref bitvector_typet. inline const bitvector_typet &to_bitvector_type(const typet &type) { @@ -1142,7 +1142,7 @@ public: }; /// Check whether a reference to a typet is a \ref bv_typet. -/// \param type Source type. +/// \param type: Source type. /// \return True if \p type is a \ref bv_typet. template <> inline bool can_cast_type(const typet &type) @@ -1161,7 +1161,7 @@ inline void validate_type(const bv_typet &type) /// bv_typet. Will fail with a precondition violation if type /// doesn't match. /// -/// \param type Source type. +/// \param type: Source type. /// \return Object of type \ref bv_typet. inline const bv_typet &to_bv_type(const typet &type) { @@ -1204,7 +1204,7 @@ public: }; /// Check whether a reference to a typet is a \ref unsignedbv_typet. -/// \param type Source type. +/// \param type: Source type. /// \return True if \p type is a \ref unsignedbv_typet. template <> inline bool can_cast_type(const typet &type) @@ -1218,7 +1218,7 @@ inline bool can_cast_type(const typet &type) /// unsignedbv_typet. Will fail with a precondition violation if type /// doesn't match. /// -/// \param type Source type. +/// \param type: Source type. /// \return Object of type \ref unsignedbv_typet. inline const unsignedbv_typet &to_unsignedbv_type(const typet &type) { @@ -1252,7 +1252,7 @@ public: }; /// Check whether a reference to a typet is a \ref signedbv_typet. -/// \param type Source type. +/// \param type: Source type. /// \return True if \p type is a \ref signedbv_typet. template <> inline bool can_cast_type(const typet &type) @@ -1272,7 +1272,7 @@ inline void validate_type(const signedbv_typet &type) /// signedbv_typet. Will fail with a precondition violation if type /// doesn't match. /// -/// \param type Source type. +/// \param type: Source type. /// \return Object of type \ref signedbv_typet. inline const signedbv_typet &to_signedbv_type(const typet &type) { @@ -1316,7 +1316,7 @@ public: }; /// Check whether a reference to a typet is a \ref fixedbv_typet. -/// \param type Source type. +/// \param type: Source type. /// \return True if \p type is a \ref fixedbv_typet. template <> inline bool can_cast_type(const typet &type) @@ -1336,7 +1336,7 @@ inline void validate_type(const fixedbv_typet &type) /// fixedbv_typet. Will fail with a precondition violation if type /// doesn't match. /// -/// \param type Source type. +/// \param type: Source type. /// \return Object of type \ref fixedbv_typet. inline const fixedbv_typet &to_fixedbv_type(const typet &type) { @@ -1378,7 +1378,7 @@ public: }; /// Check whether a reference to a typet is a \ref floatbv_typet. -/// \param type Source type. +/// \param type: Source type. /// \return True if \p type is a \ref floatbv_typet. template <> inline bool can_cast_type(const typet &type) @@ -1398,7 +1398,7 @@ inline void validate_type(const floatbv_typet &type) /// floatbv_typet. Will fail with a precondition violation if type /// doesn't match. /// -/// \param type Source type. +/// \param type: Source type. /// \return Object of type \ref floatbv_typet. inline const floatbv_typet &to_floatbv_type(const typet &type) { @@ -1433,7 +1433,7 @@ public: }; /// Check whether a reference to a typet is a \ref c_bit_field_typet. -/// \param type Source type. +/// \param type: Source type. /// \return True if \p type is a \ref c_bit_field_typet. template <> inline bool can_cast_type(const typet &type) @@ -1447,7 +1447,7 @@ inline bool can_cast_type(const typet &type) /// c_bit_field_typet. Will fail with a precondition violation if type /// doesn't match. /// -/// \param type Source type. +/// \param type: Source type. /// \return Object of type \ref c_bit_field_typet. inline const c_bit_field_typet &to_c_bit_field_type(const typet &type) { @@ -1481,7 +1481,7 @@ public: }; /// Check whether a reference to a typet is a \ref pointer_typet. -/// \param type Source type. +/// \param type: Source type. /// \return True if \p type is a \ref pointer_typet. template <> inline bool can_cast_type(const typet &type) @@ -1500,7 +1500,7 @@ inline void validate_type(const pointer_typet &type) /// pointer_typet. Will fail with a precondition violation if type /// doesn't match. /// -/// \param type Source type. +/// \param type: Source type. /// \return Object of type \ref pointer_typet. inline const pointer_typet &to_pointer_type(const typet &type) { @@ -1534,7 +1534,7 @@ public: }; /// Check whether a reference to a typet is a \ref reference_typet. -/// \param type Source type. +/// \param type: Source type. /// \return True if \p type is a \ref reference_typet. template <> inline bool can_cast_type(const typet &type) @@ -1549,7 +1549,7 @@ inline bool can_cast_type(const typet &type) /// reference_typet. Will fail with a precondition violation if type /// doesn't match. /// -/// \param type Source type. +/// \param type: Source type. /// \return Object of type \ref reference_typet. inline const reference_typet &to_reference_type(const typet &type) { @@ -1579,7 +1579,7 @@ public: }; /// Check whether a reference to a typet is a \ref c_bool_typet. -/// \param type Source type. +/// \param type: Source type. /// \return True if \p type is a \ref c_bool_typet. template <> inline bool can_cast_type(const typet &type) @@ -1598,7 +1598,7 @@ inline void validate_type(const c_bool_typet &type) /// c_bool_typet. Will fail with a precondition violation if type /// doesn't match. /// -/// \param type Source type. +/// \param type: Source type. /// \return Object of type \ref c_bool_typet. inline const c_bool_typet &to_c_bool_type(const typet &type) { @@ -1629,7 +1629,7 @@ public: }; /// Check whether a reference to a typet is a \ref string_typet. -/// \param type Source type. +/// \param type: Source type. /// \return True if \p type is a \ref string_typet. template <> inline bool can_cast_type(const typet &type) @@ -1643,7 +1643,7 @@ inline bool can_cast_type(const typet &type) /// string_typet. Will fail with a precondition violation if type /// doesn't match. /// -/// \param type Source type. +/// \param type: Source type. /// \return Object of type \ref string_typet. inline const string_typet &to_string_type(const typet &type) { @@ -1676,7 +1676,7 @@ public: }; /// Check whether a reference to a typet is a \ref range_typet. -/// \param type Source type. +/// \param type: Source type. /// \return True if \p type is a \ref range_typet. template <> inline bool can_cast_type(const typet &type) @@ -1690,7 +1690,7 @@ inline bool can_cast_type(const typet &type) /// range_typet. Will fail with a precondition violation if type /// doesn't match. /// -/// \param type Source type. +/// \param type: Source type. /// \return Object of type \ref range_typet. inline const range_typet &to_range_type(const typet &type) { @@ -1735,7 +1735,7 @@ public: }; /// Check whether a reference to a typet is a \ref vector_typet. -/// \param type Source type. +/// \param type: Source type. /// \return True if \p type is a \ref vector_typet. template <> inline bool can_cast_type(const typet &type) @@ -1749,7 +1749,7 @@ inline bool can_cast_type(const typet &type) /// vector_typet. Will fail with a precondition violation if type /// doesn't match. /// -/// \param type Source type. +/// \param type: Source type. /// \return Object of type \ref vector_typet. inline const vector_typet &to_vector_type(const typet &type) { @@ -1780,7 +1780,7 @@ public: }; /// Check whether a reference to a typet is a \ref complex_typet. -/// \param type Source type. +/// \param type: Source type. /// \return True if \p type is a \ref complex_typet. template <> inline bool can_cast_type(const typet &type) @@ -1794,7 +1794,7 @@ inline bool can_cast_type(const typet &type) /// complex_typet. Will fail with a precondition violation if type /// doesn't match. /// -/// \param type Source type. +/// \param type: Source type. /// \return Object of type \ref complex_typet. inline const complex_typet &to_complex_type(const typet &type) { diff --git a/src/util/string_utils.cpp b/src/util/string_utils.cpp index 6112670255..19a39825e5 100644 --- a/src/util/string_utils.cpp +++ b/src/util/string_utils.cpp @@ -42,10 +42,10 @@ std::string strip_string(const std::string &s) /// \param delim: The character to use as the delimiter /// \param [out] result: The sub strings. Must be empty. /// \param strip: If true, strip_string will be used on each element, removing -/// whitespace from the beginning and end of each element +/// whitespace from the beginning and end of each element /// \param remove_empty: If true, all empty-string elements will be removed. -/// This is applied after strip so whitespace only elements will be removed if -/// both are set to true +/// This is applied after strip so whitespace only elements will be removed if +/// both are set to true. void split_string( const std::string &s, char delim, diff --git a/src/util/string_utils.h b/src/util/string_utils.h index 803a4ab4d0..4e2679f13d 100644 --- a/src/util/string_utils.h +++ b/src/util/string_utils.h @@ -41,12 +41,12 @@ std::string trim_from_last_delimiter( const char delim); /// Prints items to an stream, separated by a constant delimiter -/// \tparam It An iterator type -/// \tparam Delimiter A delimiter type which supports printing to ostreams -/// \param os An ostream to write to -/// \param b Iterator pointing to first item to print -/// \param e Iterator pointing past last item to print -/// \param delimiter Object to print between each item in the iterator range +/// \tparam It: An iterator type +/// \tparam Delimiter: A delimiter type which supports printing to ostreams +/// \param os: An ostream to write to +/// \param b: Iterator pointing to first item to print +/// \param e: Iterator pointing past last item to print +/// \param delimiter: Object to print between each item in the iterator range /// \return A reference to the ostream that was passed in template Stream &join_strings( diff --git a/src/util/symbol.cpp b/src/util/symbol.cpp index 758b18583c..74221d377b 100644 --- a/src/util/symbol.cpp +++ b/src/util/symbol.cpp @@ -124,7 +124,7 @@ symbol_exprt symbolt::symbol_expr() const } /// Check that the instance object is well formed. -/// \return: true if well-formed; false otherwise. +/// \return true if well-formed; false otherwise. bool symbolt::is_well_formed() const { // Well-formedness criterion number 1 is for a symbol diff --git a/src/util/symbol_table_base.h b/src/util/symbol_table_base.h index b5beb31bc8..262c415d09 100644 --- a/src/util/symbol_table_base.h +++ b/src/util/symbol_table_base.h @@ -121,7 +121,7 @@ public: /// result as both move and add /// \param symbol: The symbol to be added to the symbol table - can be /// moved or copied in. - /// \return: Returns a reference to the newly inserted symbol or to the + /// \return Returns a reference to the newly inserted symbol or to the /// existing symbol if a symbol with the same name already exists in the /// symbol table, along with a bool that is true if a new symbol was /// inserted. diff --git a/src/util/type.cpp b/src/util/type.cpp index cbfefd0b0b..4e96dbe453 100644 --- a/src/util/type.cpp +++ b/src/util/type.cpp @@ -13,7 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "type.h" /// Copy the provided type to the subtypes of this type. -/// \param type The type to add to subtypes +/// \param type: The type to add to subtypes void type_with_subtypest::copy_to_subtypes(const typet &type) { subtypes().push_back(type); @@ -21,7 +21,7 @@ void type_with_subtypest::copy_to_subtypes(const typet &type) /// Move the provided type to the subtypes of this type. Destroys the /// provided type. -/// \param type The type to add to subtypes +/// \param type: The type to add to subtypes void type_with_subtypest::move_to_subtypes(typet &type) { subtypest &sub=subtypes(); diff --git a/src/util/type_eq.cpp b/src/util/type_eq.cpp index 05a69204f4..6ba8036d48 100644 --- a/src/util/type_eq.cpp +++ b/src/util/type_eq.cpp @@ -25,9 +25,9 @@ Author: Daniel Kroening, kroening@kroening.com /// - `symbol_typet("a")` and `ns.lookup("a").type` will compare equal, /// - `struct_typet {symbol_typet("a")}` and `struct_typet {ns.lookup("a") /// .type}` will not compare equal. -/// \param type1 The first type to compare. -/// \param type2 The second type to compare. -/// \param ns The namespace, needed for resolution of symbols. +/// \param type1: The first type to compare. +/// \param type2: The second type to compare. +/// \param ns: The namespace, needed for resolution of symbols. bool type_eq(const typet &type1, const typet &type2, const namespacet &ns) { if(type1==type2) diff --git a/src/util/unicode.cpp b/src/util/unicode.cpp index 3799cb0465..aca434cf3c 100644 --- a/src/util/unicode.cpp +++ b/src/util/unicode.cpp @@ -134,7 +134,7 @@ static void utf8_append_code(unsigned int c, std::string &result) } } -/// \param s UTF-32 encoded wide string +/// \param s: UTF-32 encoded wide string /// \return utf8-encoded string with the same unicode characters as the input. std::string utf32_native_endian_to_utf8(const std::basic_string &s) @@ -254,7 +254,7 @@ std::wstring utf8_to_utf16_native_endian(const std::string &in) /// \param ch: UTF-16 character in architecture-native endianness encoding /// \param result: stream to receive string in US-ASCII format, with \\uxxxx -/// escapes for other characters +/// escapes for other characters /// \param loc: locale to check for printable characters static void utf16_native_endian_to_java( const wchar_t ch, diff --git a/src/util/union_find_replace.cpp b/src/util/union_find_replace.cpp index 9d92c01e3e..c1b9b0a0f2 100644 --- a/src/util/union_find_replace.cpp +++ b/src/util/union_find_replace.cpp @@ -42,7 +42,7 @@ exprt union_find_replacet::find(exprt expr) const } /// \return pairs of expression composed of expressions and a representative -/// expression for the set they below to. +/// expression for the set they below to. std::vector> union_find_replacet::to_vector() const { std::vector> equations; diff --git a/unit/util/string_utils/split_string.cpp b/unit/util/string_utils/split_string.cpp index 99117cb7db..11ada1444c 100644 --- a/unit/util/string_utils/split_string.cpp +++ b/unit/util/string_utils/split_string.cpp @@ -26,7 +26,7 @@ struct expected_resultst /// \param string: The string to split /// \param delimiter: The delimter to split on /// \param expected_results: The results expected for each of the versions of -/// the method +/// the method void run_on_all_variants( std::string string, char delimiter,