From 84516805253ff911f9181db29497290b17689d92 Mon Sep 17 00:00:00 2001 From: John Nonweiler Date: Thu, 11 Oct 2018 13:13:06 +0100 Subject: [PATCH 1/6] Update parameter documentation Doxygen produces warnings if some parameters are documentated and not others, or if there is documentation for parameters which don't exist. --- jbmc/src/java_bytecode/java_entry_point.cpp | 6 ++---- jbmc/src/java_bytecode/java_object_factory.cpp | 14 ++++++++++++++ jbmc/src/java_bytecode/java_types.h | 2 +- src/goto-programs/class_hierarchy.h | 1 - src/goto-programs/read_goto_binary.cpp | 2 ++ 5 files changed, 19 insertions(+), 6 deletions(-) diff --git a/jbmc/src/java_bytecode/java_entry_point.cpp b/jbmc/src/java_bytecode/java_entry_point.cpp index 91107ffa127..cdabf2adb42 100644 --- a/jbmc/src/java_bytecode/java_entry_point.cpp +++ b/jbmc/src/java_bytecode/java_entry_point.cpp @@ -638,10 +638,8 @@ bool java_entry_point( /// \param message_handler: Where to write output to /// \param assume_init_pointers_not_null: When creating pointers, assume they /// always take a non-null value. -/// \param max_nondet_array_length: The length of the arrays to create when -/// filling them -/// \param max_nondet_tree_depth: defines the maximum depth of the object tree -/// (see java_entry_points documentation for details) +/// \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 bool generate_java_start_function( diff --git a/jbmc/src/java_bytecode/java_object_factory.cpp b/jbmc/src/java_bytecode/java_object_factory.cpp index 0f98c9c2429..2850ac3b1a4 100644 --- a/jbmc/src/java_bytecode/java_object_factory.cpp +++ b/jbmc/src/java_bytecode/java_object_factory.cpp @@ -176,6 +176,7 @@ class java_object_factoryt /// \param allocate_type: type of the object allocated /// \param symbol_table: symbol table /// \param loc: location in the source +/// \param function_id: function ID to associate with auxiliary variables /// \param output_code: code block to which the necessary code is added /// \param symbols_created: created symbols to be declared by the caller /// \param cast_needed: Boolean flags saying where we need to cast the malloc @@ -242,6 +243,7 @@ exprt allocate_dynamic_object( /// allocated /// \param symbol_table: symbol table /// \param loc: location in the source +/// \param function_id: function ID to associate with auxiliary variables /// \param output_code: code block to which the necessary code is added /// \return the dynamic object created exprt allocate_dynamic_object_with_decl( @@ -392,6 +394,8 @@ code_assignt java_object_factoryt::get_null_assignment( /// 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. void java_object_factoryt::gen_pointer_target_init( code_blockt &assignments, const exprt &expr, @@ -707,6 +711,8 @@ bool initialize_nondet_string_fields( /// * MAY_UPDATE_IN_PLACE: generate a runtime nondet branch between the NO_ /// and MUST_ cases. /// * MUST_UPDATE_IN_PLACE: reinitialize an existing object +/// \param location: +/// Source location associated with nondet-initialization. void java_object_factoryt::gen_nondet_pointer_init( code_blockt &assignments, const exprt &expr, @@ -930,6 +936,8 @@ void java_object_factoryt::gen_nondet_pointer_init( /// \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). @@ -994,6 +1002,8 @@ symbol_exprt java_object_factoryt::gen_nondet_subtype_pointer_init( /// 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. void java_object_factoryt::gen_nondet_struct_init( code_blockt &assignments, const exprt &expr, @@ -1159,6 +1169,8 @@ void java_object_factoryt::gen_nondet_struct_init( /// MAY_UPDATE_IN_PLACE: generate a runtime nondet branch between the NO_ /// and MUST_ cases. /// MUST_UPDATE_IN_PLACE: reinitialize an existing object +/// \param location: +/// Source location associated with nondet-initialization. void java_object_factoryt::gen_nondet_init( code_blockt &assignments, const exprt &expr, @@ -1307,6 +1319,8 @@ const symbol_exprt java_object_factoryt::gen_nondet_int_init( /// \param element_type: /// Actual element type of the array (the array for all reference types will /// have void* type, but this will be annotated as the true member type). +/// \param location: +/// Source location associated with nondet-initialization. /// \return Appends instructions to `assignments` void java_object_factoryt::allocate_nondet_length_array( code_blockt &assignments, diff --git a/jbmc/src/java_bytecode/java_types.h b/jbmc/src/java_bytecode/java_types.h index 8ca7b6f2066..4d59a502e1b 100644 --- a/jbmc/src/java_bytecode/java_types.h +++ b/jbmc/src/java_bytecode/java_types.h @@ -695,7 +695,7 @@ inline typet java_type_from_string_with_exception( } /// Get the index in the subtypes array for a given component. -/// \param t The type we search for the subtypes in. +/// \param gen_types The subtypes array. /// \param identifier The string identifier of the type of the component. /// \return Optional with the size if the identifier was found. inline const optionalt java_generics_get_index_for_subtype( diff --git a/src/goto-programs/class_hierarchy.h b/src/goto-programs/class_hierarchy.h index abc3b390290..ed4c25f4783 100644 --- a/src/goto-programs/class_hierarchy.h +++ b/src/goto-programs/class_hierarchy.h @@ -130,7 +130,6 @@ class class_hierarchy_grapht : public grapht /// Output the class hierarchy /// \param hierarchy: the class hierarchy to be printed /// \param message_handler: the message handler -/// \param ui: the UI format /// \param children_only: print the children only and do not print the parents void show_class_hierarchy( const class_hierarchyt &hierarchy, diff --git a/src/goto-programs/read_goto_binary.cpp b/src/goto-programs/read_goto_binary.cpp index d4333852dc6..a71fc3e36a4 100644 --- a/src/goto-programs/read_goto_binary.cpp +++ b/src/goto-programs/read_goto_binary.cpp @@ -261,6 +261,8 @@ bool read_object_and_link( /// \brief reads an object file, and also updates the config /// \param file_name file name of the goto binary +/// \param dest_symbol_table symbol table to update +/// \param dest_functions collection of goto functions to update /// \param message_handler for diagnostics /// \return true on error, false otherwise bool read_object_and_link( From 798fe51f0f4bcc99e99515311564f1c7c2abe5b4 Mon Sep 17 00:00:00 2001 From: John Nonweiler Date: Fri, 12 Oct 2018 09:37:40 +0100 Subject: [PATCH 2/6] Remove leading underscores from parameter names Doxygen doesn't seem to be able to handle method parameters such as '_parameters' or '_return_type' properly. --- .../src/java_bytecode/java_object_factory.cpp | 6 +++--- jbmc/src/java_bytecode/java_types.h | 16 +++++++-------- src/util/std_types.h | 20 +++++++++---------- 3 files changed, 21 insertions(+), 21 deletions(-) diff --git a/jbmc/src/java_bytecode/java_object_factory.cpp b/jbmc/src/java_bytecode/java_object_factory.cpp index 2850ac3b1a4..204811987eb 100644 --- a/jbmc/src/java_bytecode/java_object_factory.cpp +++ b/jbmc/src/java_bytecode/java_object_factory.cpp @@ -478,9 +478,9 @@ class recursion_set_entryt public: /// Initialize a recursion-set entry owner operating on a given set. /// Initially it does not own any set entry. - /// \param _recursion_set: set to operate on. - explicit recursion_set_entryt(std::unordered_set &_recursion_set) - : recursion_set(_recursion_set) + /// \param recursion_set: set to operate on. + explicit recursion_set_entryt(std::unordered_set &recursion_set) + : recursion_set(recursion_set) { } /// Removes erase_entry (if set) from the controlled set. diff --git a/jbmc/src/java_bytecode/java_types.h b/jbmc/src/java_bytecode/java_types.h index 4d59a502e1b..84048ccba42 100644 --- a/jbmc/src/java_bytecode/java_types.h +++ b/jbmc/src/java_bytecode/java_types.h @@ -249,19 +249,19 @@ class java_method_typet : public code_typet using code_typet::parametert; /// Constructs a new code type, i.e. method type - /// \param _parameters: the vector of method parameters - /// \param _return_type: the return type - java_method_typet(parameterst &&_parameters, typet &&_return_type) - : code_typet(std::move(_parameters), std::move(_return_type)) + /// \param parameters: the vector of method parameters + /// \param return_type: the return type + java_method_typet(parameterst &¶meters, typet &&return_type) + : code_typet(std::move(parameters), std::move(return_type)) { set(ID_C_java_method_type, true); } /// Constructs a new code type, i.e. method type - /// \param _parameters: the vector of method parameters - /// \param _return_type: the return type - java_method_typet(parameterst &&_parameters, const typet &_return_type) - : code_typet(std::move(_parameters), _return_type) + /// \param parameters: the vector of method parameters + /// \param return_type: the return type + java_method_typet(parameterst &¶meters, const typet &return_type) + : code_typet(std::move(parameters), return_type) { set(ID_C_java_method_type, true); } diff --git a/src/util/std_types.h b/src/util/std_types.h index 8317d68fe32..b48d670dfd0 100644 --- a/src/util/std_types.h +++ b/src/util/std_types.h @@ -775,22 +775,22 @@ class code_typet:public typet 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. - code_typet(parameterst &&_parameters, typet &&_return_type) : typet(ID_code) + /// \param parameters The vector of function parameters. + /// \param return_type The return type. + code_typet(parameterst &¶meters, typet &&return_type) : typet(ID_code) { - parameters().swap(_parameters); - return_type().swap(_return_type); + parameters().swap(parameters); + return_type().swap(return_type); } /// Constructs a new code type, i.e., function type. - /// \param _parameters The vector of function parameters. - /// \param _return_type The return type. - code_typet(parameterst &&_parameters, const typet &_return_type) + /// \param parameters The vector of function parameters. + /// \param return_type The return type. + code_typet(parameterst &¶meters, const typet &return_type) : typet(ID_code) { - parameters().swap(_parameters); - return_type() = _return_type; + parameters().swap(parameters); + return_type() = return_type; } /// \deprecated From dd33cc78b0d287118e7b0d14c23a99b61482c492 Mon Sep 17 00:00:00 2001 From: John Nonweiler Date: Fri, 12 Oct 2018 09:52:17 +0100 Subject: [PATCH 3/6] Correct doxygen syntax Doxygen was warning that the argument 'type' has muliple @param documentation sections, and producing incorrect documentation. --- src/util/std_types.h | 56 ++++++++++++++++++++++---------------------- 1 file changed, 28 insertions(+), 28 deletions(-) diff --git a/src/util/std_types.h b/src/util/std_types.h index b48d670dfd0..e13f9c084dc 100644 --- a/src/util/std_types.h +++ b/src/util/std_types.h @@ -79,7 +79,7 @@ class symbol_typet:public typet /// Check whether a reference to a typet is a \ref symbol_typet. /// \param type Source type. -/// \return True if \param type is a \ref symbol_typet. +/// \return True if type is a \ref symbol_typet. template <> inline bool can_cast_type(const typet &type) { @@ -243,7 +243,7 @@ class struct_union_typet:public typet /// Check whether a reference to a typet is a \ref struct_union_typet. /// \param type Source type. -/// \return True if \param type is a \ref struct_union_typet. +/// \return True if type is a \ref struct_union_typet. template <> inline bool can_cast_type(const typet &type) { @@ -351,7 +351,7 @@ class struct_typet:public struct_union_typet /// Check whether a reference to a typet is a \ref struct_typet. /// \param type Source type. -/// \return True if \param type is a \ref struct_typet. +/// \return True if type is a \ref struct_typet. template <> inline bool can_cast_type(const typet &type) { @@ -411,7 +411,7 @@ class class_typet:public struct_typet /// Check whether a reference to a typet is a \ref class_typet. /// \param type Source type. -/// \return True if \param type is a \ref class_typet. +/// \return True if type is a \ref class_typet. template <> inline bool can_cast_type(const typet &type) { @@ -452,7 +452,7 @@ class union_typet:public struct_union_typet /// Check whether a reference to a typet is a \ref union_typet. /// \param type Source type. -/// \return True if \param type is a \ref union_typet. +/// \return True if type is a \ref union_typet. template <> inline bool can_cast_type(const typet &type) { @@ -504,7 +504,7 @@ class tag_typet:public typet /// Check whether a reference to a typet is a \ref tag_typet. /// \param type Source type. -/// \return True if \param type is a \ref tag_typet. +/// \return True if type is a \ref tag_typet. template <> inline bool can_cast_type(const typet &type) { @@ -545,7 +545,7 @@ class struct_tag_typet:public tag_typet /// Check whether a reference to a typet is a \ref struct_tag_typet. /// \param type Source type. -/// \return True if \param type is a \ref struct_tag_typet. +/// \return True if type is a \ref struct_tag_typet. template <> inline bool can_cast_type(const typet &type) { @@ -585,7 +585,7 @@ class union_tag_typet:public tag_typet /// Check whether a reference to a typet is a \ref union_tag_typet. /// \param type Source type. -/// \return True if \param type is a \ref union_tag_typet. +/// \return True if type is a \ref union_tag_typet. template <> inline bool can_cast_type(const typet &type) { @@ -635,7 +635,7 @@ class enumeration_typet:public typet /// Check whether a reference to a typet is a \ref enumeration_typet. /// \param type Source type. -/// \return True if \param type is a \ref enumeration_typet. +/// \return True if type is a \ref enumeration_typet. template <> inline bool can_cast_type(const typet &type) { @@ -699,7 +699,7 @@ class c_enum_typet:public type_with_subtypet /// Check whether a reference to a typet is a \ref c_enum_typet. /// \param type Source type. -/// \return True if \param type is a \ref c_enum_typet. +/// \return True if type is a \ref c_enum_typet. template <> inline bool can_cast_type(const typet &type) { @@ -739,7 +739,7 @@ class c_enum_tag_typet:public tag_typet /// Check whether a reference to a typet is a \ref c_enum_tag_typet. /// \param type Source type. -/// \return True if \param type is a \ref c_enum_tag_typet. +/// \return True if type is a \ref c_enum_tag_typet. template <> inline bool can_cast_type(const typet &type) { @@ -984,7 +984,7 @@ class code_typet:public typet /// Check whether a reference to a typet is a \ref code_typet. /// \param type Source type. -/// \return True if \param type is a \ref code_typet. +/// \return True if type is a \ref code_typet. template <> inline bool can_cast_type(const typet &type) { @@ -1050,7 +1050,7 @@ class array_typet:public type_with_subtypet /// Check whether a reference to a typet is a \ref array_typet. /// \param type Source type. -/// \return True if \param type is a \ref array_typet. +/// \return True if type is a \ref array_typet. template <> inline bool can_cast_type(const typet &type) { @@ -1089,7 +1089,7 @@ class incomplete_array_typet:public type_with_subtypet /// Check whether a reference to a typet is a \ref incomplete_array_typet. /// \param type Source type. -/// \return True if \param type is a \ref incomplete_array_typet. +/// \return True if type is a \ref incomplete_array_typet. template <> inline bool can_cast_type(const typet &type) { @@ -1162,7 +1162,7 @@ class bitvector_typet:public type_with_subtypet /// Check whether a reference to a typet is a \ref bitvector_typet. /// \param type Source type. -/// \return True if \param type is a \ref bitvector_typet. +/// \return True if type is a \ref bitvector_typet. template <> inline bool can_cast_type(const typet &type) { @@ -1209,7 +1209,7 @@ class bv_typet:public bitvector_typet /// Check whether a reference to a typet is a \ref bv_typet. /// \param type Source type. -/// \return True if \param type is a \ref bv_typet. +/// \return True if type is a \ref bv_typet. template <> inline bool can_cast_type(const typet &type) { @@ -1264,7 +1264,7 @@ class unsignedbv_typet:public bitvector_typet /// Check whether a reference to a typet is a \ref unsignedbv_typet. /// \param type Source type. -/// \return True if \param type is a \ref unsignedbv_typet. +/// \return True if type is a \ref unsignedbv_typet. template <> inline bool can_cast_type(const typet &type) { @@ -1320,7 +1320,7 @@ class signedbv_typet:public bitvector_typet /// Check whether a reference to a typet is a \ref signedbv_typet. /// \param type Source type. -/// \return True if \param type is a \ref signedbv_typet. +/// \return True if type is a \ref signedbv_typet. template <> inline bool can_cast_type(const typet &type) { @@ -1384,7 +1384,7 @@ class fixedbv_typet:public bitvector_typet /// Check whether a reference to a typet is a \ref fixedbv_typet. /// \param type Source type. -/// \return True if \param type is a \ref fixedbv_typet. +/// \return True if type is a \ref fixedbv_typet. template <> inline bool can_cast_type(const typet &type) { @@ -1446,7 +1446,7 @@ class floatbv_typet:public bitvector_typet /// Check whether a reference to a typet is a \ref floatbv_typet. /// \param type Source type. -/// \return True if \param type is a \ref floatbv_typet. +/// \return True if type is a \ref floatbv_typet. template <> inline bool can_cast_type(const typet &type) { @@ -1498,7 +1498,7 @@ class c_bit_field_typet:public bitvector_typet /// Check whether a reference to a typet is a \ref c_bit_field_typet. /// \param type Source type. -/// \return True if \param type is a \ref c_bit_field_typet. +/// \return True if type is a \ref c_bit_field_typet. template <> inline bool can_cast_type(const typet &type) { @@ -1543,7 +1543,7 @@ class pointer_typet:public bitvector_typet /// Check whether a reference to a typet is a \ref pointer_typet. /// \param type Source type. -/// \return True if \param type is a \ref pointer_typet. +/// \return True if type is a \ref pointer_typet. template <> inline bool can_cast_type(const typet &type) { @@ -1596,7 +1596,7 @@ class reference_typet:public pointer_typet /// Check whether a reference to a typet is a \ref reference_typet. /// \param type Source type. -/// \return True if \param type is a \ref reference_typet. +/// \return True if type is a \ref reference_typet. template <> inline bool can_cast_type(const typet &type) { @@ -1645,7 +1645,7 @@ class c_bool_typet:public bitvector_typet /// Check whether a reference to a typet is a \ref c_bool_typet. /// \param type Source type. -/// \return True if \param type is a \ref c_bool_typet. +/// \return True if type is a \ref c_bool_typet. template <> inline bool can_cast_type(const typet &type) { @@ -1695,7 +1695,7 @@ class string_typet:public typet /// Check whether a reference to a typet is a \ref string_typet. /// \param type Source type. -/// \return True if \param type is a \ref string_typet. +/// \return True if type is a \ref string_typet. template <> inline bool can_cast_type(const typet &type) { @@ -1742,7 +1742,7 @@ class range_typet:public typet /// Check whether a reference to a typet is a \ref range_typet. /// \param type Source type. -/// \return True if \param type is a \ref range_typet. +/// \return True if type is a \ref range_typet. template <> inline bool can_cast_type(const typet &type) { @@ -1801,7 +1801,7 @@ class vector_typet:public type_with_subtypet /// Check whether a reference to a typet is a \ref vector_typet. /// \param type Source type. -/// \return True if \param type is a \ref vector_typet. +/// \return True if type is a \ref vector_typet. template <> inline bool can_cast_type(const typet &type) { @@ -1845,7 +1845,7 @@ class complex_typet:public type_with_subtypet /// Check whether a reference to a typet is a \ref complex_typet. /// \param type Source type. -/// \return True if \param type is a \ref complex_typet. +/// \return True if type is a \ref complex_typet. template <> inline bool can_cast_type(const typet &type) { From e9ec09e04162a323be06cd1cf747a44bea657532 Mon Sep 17 00:00:00 2001 From: John Nonweiler Date: Tue, 9 Oct 2018 11:06:21 +0100 Subject: [PATCH 4/6] Move forward declaration of class (to help doxygen) Before this commit, get_xml_options had the parameters "(const class xmlt &xml, cmdlinet &cmdline)" in the header file, and "(const xmlt &xml, cmdlinet &cmdline)" in the cpp file. Doxygen then produced a warning "no matching class member found". This commit adds a forward declaration "class xmlt;" in the header file, so that both versions of get_xml_options can have identical parameter lists. --- src/cbmc/xml_interface.h | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/cbmc/xml_interface.h b/src/cbmc/xml_interface.h index 945be7624bb..8230d180bad 100644 --- a/src/cbmc/xml_interface.h +++ b/src/cbmc/xml_interface.h @@ -14,6 +14,8 @@ Author: Daniel Kroening, kroening@kroening.com #include +class xmlt; + class xml_interfacet { public: @@ -24,7 +26,7 @@ class xml_interfacet protected: void get_xml_options(cmdlinet &cmdline); - void get_xml_options(const class xmlt &xml, cmdlinet &cmdline); + void get_xml_options(const xmlt &xml, cmdlinet &cmdline); }; #endif // CPROVER_CBMC_XML_INTERFACE_H From dee61e1c4bffb7e082cbb127735c1b6ae2457ab6 Mon Sep 17 00:00:00 2001 From: John Nonweiler Date: Tue, 9 Oct 2018 11:16:32 +0100 Subject: [PATCH 5/6] Change int type specifiers to equivalent types Replace 'signed int' with 'int', and 'unsigned int' with 'unsigned', so that .cpp and .h files are consistent, and doxygen doesn't get confused --- src/util/options.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/util/options.cpp b/src/util/options.cpp index 5671e7ed281..3af4bfd034c 100644 --- a/src/util/options.cpp +++ b/src/util/options.cpp @@ -28,13 +28,13 @@ void optionst::set_option(const std::string &option, } void optionst::set_option(const std::string &option, - const signed int value) + const int value) { set_option(option, std::to_string(value)); } void optionst::set_option(const std::string &option, - const unsigned int value) + const unsigned value) { set_option(option, std::to_string(value)); } From 18dfcd781c0d87ef5e6112f22330285d79e23c5a Mon Sep 17 00:00:00 2001 From: John Nonweiler Date: Fri, 12 Oct 2018 10:05:35 +0100 Subject: [PATCH 6/6] Add name to method parameter in header file The doxygen comment in the header file was referring to a parameter which was given a name only in the cpp file, and doxygen was complaining that it could not find the parameter. --- jbmc/src/java_bytecode/replace_java_nondet.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/jbmc/src/java_bytecode/replace_java_nondet.h b/jbmc/src/java_bytecode/replace_java_nondet.h index 4a0b00c3b1e..66f026441a0 100644 --- a/jbmc/src/java_bytecode/replace_java_nondet.h +++ b/jbmc/src/java_bytecode/replace_java_nondet.h @@ -19,7 +19,7 @@ class goto_model_functiont; /// Replace calls to nondet library functions with an internal nondet /// representation. /// \param goto_model: The goto program to modify. -void replace_java_nondet(goto_modelt &); +void replace_java_nondet(goto_modelt &goto_model); void replace_java_nondet(goto_functionst &);