diff --git a/doc/architectural/compilation-and-development.md b/doc/architectural/compilation-and-development.md index d5174856307..ba3b5746472 100644 --- a/doc/architectural/compilation-and-development.md +++ b/doc/architectural/compilation-and-development.md @@ -194,8 +194,14 @@ tools. All of these could be improved and patches are very welcome. In some cases the algorithms used are described in the relevant papers. The doxygen documentation can be [accessed online](http://cprover.diffblue.com). -To build it locally, run `doxygen` in `src/`. HTML output will be created in -`doc/html/`. The index page is `doc/html/index.html`. +To build it locally, run `scripts/run_doxygen.sh`. HTML output will be created +in `doc/html/`. The index page is `doc/html/index.html`. This script will +filter out expected warning messages from doxygen, so that new problems are more +obvious. In the event that any change fixes an old warning, then the +corresponding line(s) should be deleted from +`scripts/expected_doxygen_warnings.txt`. We want to avoid adding any more +warnings to this list of expected warnings, but that can be done to work around +limitations in Doxygen (where the code and documentation are completely correct). \section compilation-and-development-section-formatting Formatting diff --git a/scripts/expected_doxygen_warnings.txt b/scripts/expected_doxygen_warnings.txt new file mode 100644 index 00000000000..2103d866529 --- /dev/null +++ b/scripts/expected_doxygen_warnings.txt @@ -0,0 +1,183 @@ +/cbmc/src/solvers/miniBDD/miniBDD.cpp:402: warning: documented symbol `mini_bddt mini_bddt::operator &' was not declared or defined. +/cbmc/src/solvers/sat/satcheck_glucose.cpp:228: warning: no matching class member found for + template <> + satcheck_glucose_baset< Glucose::Solver >::~satcheck_glucose_baset() + +/cbmc/src/solvers/sat/satcheck_glucose.cpp:234: warning: no matching class member found for + template <> + satcheck_glucose_baset< Glucose::SimpSolver >::~satcheck_glucose_baset() + +/cbmc/src/solvers/sat/satcheck_minisat2.cpp:306: warning: no matching class member found for + template <> + satcheck_minisat2_baset< Minisat::Solver >::~satcheck_minisat2_baset() + +/cbmc/src/solvers/sat/satcheck_minisat2.cpp:312: warning: no matching class member found for + template <> + satcheck_minisat2_baset< Minisat::SimpSolver >::~satcheck_minisat2_baset() + +/cbmc/src/solvers/refinement/string_constraint_generator_transformation.cpp:255: warning: The following parameters of to_char_pair(exprt expr1, exprt expr2, std::function< array_string_exprt(const exprt &)> get_string_expr) are not documented: + parameter 'get_string_expr' +/cbmc/src/solvers/refinement/string_refinement.cpp:1511: warning: argument 'stream' of command @param is not found in the argument list of compute_inverse_function(const exprt &qvar, const exprt &val, const exprt &f) +/cbmc/src/solvers/refinement/string_refinement.cpp:239: warning: Invalid list item found +/cbmc/src/solvers/refinement/string_refinement.cpp:1823: warning: argument 'stream' of command @param is not found in the argument list of instantiate(const string_constraintt &axiom, const exprt &str, const exprt &val) +/cbmc/src/solvers/refinement/string_refinement.cpp:112: warning: The following parameters of instantiate(const string_not_contains_constraintt &axiom, const index_set_pairt &index_set, const string_constraint_generatort &generator, const std::map< string_not_contains_constraintt, symbol_exprt > &witnesses) are not documented: + parameter 'witnesses' +/cbmc/src/solvers/refinement/string_refinement.cpp:1052: warning: The following parameters of substitute_array_access(const with_exprt &expr, const exprt &index, const bool left_propagate) are not documented: + parameter 'left_propagate' +/cbmc/src/util/nondet.cpp:35: warning: The following parameters of generate_nondet_int(const int64_t min_value, const int64_t max_value, const std::string &name_prefix, const typet &int_type, const irep_idt &mode, const source_locationt &source_location, symbol_table_baset &symbol_table, code_blockt &instructions) are not documented: + parameter 'mode' +/cbmc/src/util/nondet.cpp:85: warning: The following parameters of generate_nondet_switch(const irep_idt &name_prefix, const alternate_casest &switch_cases, const typet &int_type, const irep_idt &mode, const source_locationt &source_location, symbol_table_baset &symbol_table) are not documented: + parameter 'mode' +/cbmc/src/util/nondet.h:16: warning: The following parameters of generate_nondet_int(const int64_t min_value, const int64_t max_value, const std::string &name_prefix, const typet &int_type, const irep_idt &mode, const source_locationt &source_location, symbol_table_baset &symbol_table, code_blockt &instructions) are not documented: + parameter 'mode' +/cbmc/src/util/nondet.h:28: warning: The following parameters of generate_nondet_switch(const irep_idt &name_prefix, const alternate_casest &switch_cases, const typet &int_type, const irep_idt &mode, const source_locationt &source_location, symbol_table_baset &symbol_table) are not documented: + parameter 'mode' +/cbmc/doc/architectural/howto.md:260: warning: found at different nesting level (6) than expected (3) +/cbmc/doc/architectural/howto.md:261: warning: end of comment block while expecting command +/cbmc/src/solvers/README.md:4: warning: @copydetails or @copydoc target 'generate_instantiations(messaget::mstreamt &stream, const string_constraint_generatort &generator, const index_set_pairt &index_set, const string_axiomst &axioms, const std::map ¬_contain_witnesses).' not found +/cbmc/src/util/README.md:245: warning: unable to resolve reference to `ansi_ct' for \ref command +/cbmc/src/cbmc/bmc.cpp:473: warning: argument 'message' of command @param is not found in the argument list of bmct::do_language_agnostic_bmc(const path_strategy_choosert &path_strategy_chooser, const optionst &opts, abstract_goto_modelt &model, ui_message_handlert &ui, std::function< void(bmct &, const symbol_tablet &)> driver_configure_bmc=nullptr, std::function< bool(void)> callback_after_symex=nullptr) +/cbmc/src/cbmc/bmc.h:124: warning: The following parameters of bmct::do_language_agnostic_bmc(const path_strategy_choosert &path_strategy_chooser, const optionst &opts, abstract_goto_modelt &model, ui_message_handlert &ui, std::function< void(bmct &, const symbol_tablet &)> driver_configure_bmc=nullptr, std::function< bool(void)> callback_after_symex=nullptr) are not documented: + parameter 'path_strategy_chooser' +/cbmc/src/solvers/flattening/bv_utils.cpp:1113: warning: argument 'Bit' of command @param is not found in the argument list of bv_utilst::equal(const bvt &op0, const bvt &op1) +/cbmc/src/solvers/flattening/bv_utils.cpp:1113: warning: argument 'vectors' of command @param is not found in the argument list of bv_utilst::equal(const bvt &op0, const bvt &op1) +/cbmc/src/solvers/flattening/bv_utils.h:134: warning: The following parameters of bv_utilst::equal(const bvt &op0, const bvt &op1) are not documented: + parameter 'op0' + parameter 'op1' +/cbmc/src/ansi-c/c_typecheck_initializer.cpp:347: warning: argument 'pre' of command @param is not found in the argument list of c_typecheck_baset::do_designated_initializer(exprt &result, designatort &designator, const exprt &initializer_list, exprt::operandst::const_iterator init_it, bool force_constant) +/cbmc/src/ansi-c/c_typecheck_initializer.cpp:347: warning: argument 'initialized' of command @param is not found in the argument list of c_typecheck_baset::do_designated_initializer(exprt &result, designatort &designator, const exprt &initializer_list, exprt::operandst::const_iterator init_it, bool force_constant) +/cbmc/src/ansi-c/c_typecheck_base.h:98: warning: The following parameters of c_typecheck_baset::do_designated_initializer(exprt &result, designatort &designator, const exprt &initializer_list, exprt::operandst::const_iterator init_it, bool force_constant) are not documented: + parameter 'result' + parameter 'designator' + parameter 'initializer_list' + parameter 'init_it' + parameter 'force_constant' +/cbmc/src/ansi-c/c_typecheck_expr.cpp:2779: warning: argument 'type' of command @param is not found in the argument list of c_typecheck_baset::typecheck_function_call_arguments(side_effect_expr_function_callt &expr) +/cbmc/src/ansi-c/c_typecheck_expr.cpp:2779: warning: argument 'checked' of command @param is not found in the argument list of c_typecheck_baset::typecheck_function_call_arguments(side_effect_expr_function_callt &expr) +/cbmc/src/ansi-c/c_typecheck_base.h:195: warning: The following parameters of c_typecheck_baset::typecheck_function_call_arguments(side_effect_expr_function_callt &expr) are not documented: + parameter 'expr' +/cbmc/jbmc/src/java_bytecode/ci_lazy_methods.h:100: warning: The following parameters of ci_lazy_methodst::ci_lazy_methodst(const symbol_tablet &symbol_table, const irep_idt &main_class, const std::vector< irep_idt > &main_jar_classes, const std::vector< load_extra_methodst > &lazy_methods_extra_entry_points, java_class_loadert &java_class_loader, const std::vector< irep_idt > &extra_instantiated_classes, const select_pointer_typet &pointer_type_selector, message_handlert &message_handler, const synthetic_methods_mapt &synthetic_methods) are not documented: + parameter 'synthetic_methods' +/cbmc/src/goto-instrument/wmm/event_graph.h:506: warning: The following parameters of event_grapht::explore_copy_segment(std::set< event_idt > &explored, event_idt begin, event_idt end) const are not documented: + parameter 'explored' +/cbmc/src/goto-instrument/wmm/cycle_collection.cpp:149: warning: argument 'get_po_only' of command @param is not found in the argument list of event_grapht::graph_explorert::backtrack(std::set< critical_cyclet > &set_of_cycles, event_idt source, event_idt vertex, bool unsafe_met, event_idt po_trans, bool same_var_pair, bool lwfence_met, bool has_to_be_unsafe, irep_idt var_to_avoid, memory_modelt model) +/cbmc/src/goto-instrument/wmm/event_graph.h:315: warning: The following parameters of event_grapht::graph_explorert::backtrack(std::set< critical_cyclet > &set_of_cycles, event_idt source, event_idt vertex, bool unsafe_met, event_idt po_trans, bool same_var_pair, bool lwfence_met, bool has_to_be_unsafe, irep_idt var_to_avoid, memory_modelt model) are not documented: + parameter 'set_of_cycles' + parameter 'source' + parameter 'vertex' + parameter 'unsafe_met' + parameter 'po_trans' + parameter 'same_var_pair' + parameter 'lwfence_met' + parameter 'has_to_be_unsafe' + parameter 'var_to_avoid' + parameter 'model' +/cbmc/src/ansi-c/expr2c_class.h:66: warning: The following parameters of expr2ct::convert_array_type(const typet &src, const qualifierst &qualifiers, const std::string &declarator_str) are not documented: + parameter 'qualifiers' + parameter 'declarator_str' +/cbmc/src/ansi-c/expr2c_class.h:71: warning: The following parameters of expr2ct::convert_array_type(const typet &src, const qualifierst &qualifiers, const std::string &declarator_str, bool inc_size_if_possible) are not documented: + parameter 'qualifiers' + parameter 'declarator_str' +/cbmc/src/ansi-c/expr2c_class.h:264: warning: The following parameters of expr2ct::convert_struct(const exprt &src, unsigned &precedence, bool include_padding_components) are not documented: + parameter 'precedence' +/cbmc/src/ansi-c/expr2c.cpp:671: warning: argument 'qualifiers' of command @param is not found in the argument list of expr2ct::convert_struct_type(const typet &src, const std::string &qualifiers_str, const std::string &declarator_str) +/cbmc/src/ansi-c/expr2c.cpp:671: warning: argument 'declarator' of command @param is not found in the argument list of expr2ct::convert_struct_type(const typet &src, const std::string &qualifiers_str, const std::string &declarator_str) +/cbmc/src/ansi-c/expr2c_class.h:54: warning: The following parameters of expr2ct::convert_struct_type(const typet &src, const std::string &qualifiers_str, const std::string &declarator_str) are not documented: + parameter 'qualifiers_str' + parameter 'declarator_str' +/cbmc/src/goto-programs/goto_convert_class.h:584: warning: The following parameters of goto_convertt::generate_thread_block(const code_blockt &thread_body, goto_programt &dest, const irep_idt &mode) are not documented: + parameter 'mode' +/cbmc/src/goto-programs/goto_model.h:150: warning: argument 'goto_model' of command @param is not found in the argument list of goto_model_functiont::goto_model_functiont(journalling_symbol_tablet &symbol_table, goto_functionst &goto_functions, const irep_idt &function_id, goto_functionst::goto_functiont &goto_function) +/cbmc/src/goto-programs/goto_model.h:155: warning: The following parameters of goto_model_functiont::goto_model_functiont(journalling_symbol_tablet &symbol_table, goto_functionst &goto_functions, const irep_idt &function_id, goto_functionst::goto_functiont &goto_function) are not documented: + parameter 'symbol_table' + parameter 'goto_functions' + parameter 'function_id' +/cbmc/src/goto-programs/goto_program.cpp:21: warning: argument 'instruction' of command @param is not found in the argument list of goto_programt::output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &it) const +/cbmc/src/goto-programs/goto_program.h:560: warning: The following parameters of goto_programt::output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &it) const are not documented: + parameter 'it' +/cbmc/src/goto-symex/goto_symex.h:179: warning: argument 'goto_functions' of command @param is not found in the argument list of goto_symext::initialize_entry_point(statet &state, const get_goto_functiont &get_goto_function, goto_programt::const_targett pc, goto_programt::const_targett limit) +/cbmc/src/goto-symex/goto_symex.h:185: warning: The following parameters of goto_symext::initialize_entry_point(statet &state, const get_goto_functiont &get_goto_function, goto_programt::const_targett pc, goto_programt::const_targett limit) are not documented: + parameter 'get_goto_function' +/cbmc/src/goto-instrument/wmm/goto2graph.h:260: warning: The following parameters of instrumentert::cfg_visitort::visit_cfg_function(value_setst &value_sets, memory_modelt model, bool no_dependencies, loop_strategyt duplicate_body, const irep_idt &function, std::set< nodet > &ending_vertex) are not documented: + parameter 'model' + parameter 'no_dependencies' + parameter 'duplicate_body' +/cbmc/jbmc/src/java_bytecode/java_bytecode_instrument.cpp:60: warning: The following parameters of java_bytecode_instrumentt::check_null_dereference(const exprt &expr, const source_locationt &original_loc) are not documented: + parameter 'original_loc' +/cbmc/jbmc/src/java_bytecode/java_bytecode_instrument.cpp:354: warning: argument 'tt' of command @param is not found in the argument list of java_bytecode_instrumentt::instrument_code(codet &code) +/cbmc/jbmc/src/java_bytecode/java_bytecode_instrument.cpp:354: warning: argument 'expr' of command @param is not found in the argument list of java_bytecode_instrumentt::instrument_code(codet &code) +/cbmc/jbmc/src/java_bytecode/java_bytecode_instrument.cpp:354: warning: argument 'tt' of command @param is not found in the argument list of java_bytecode_instrumentt::instrument_code(codet &code) +/cbmc/jbmc/src/java_bytecode/java_bytecode_instrument.cpp:73: warning: The following parameters of java_bytecode_instrumentt::instrument_code(codet &code) are not documented: + parameter 'code' +/cbmc/jbmc/src/java_bytecode/java_bytecode_instrument.cpp:546: warning: argument 'expr' of command @param is not found in the argument list of java_bytecode_instrumentt::operator()(codet &code) +/cbmc/jbmc/src/java_bytecode/java_bytecode_instrument.cpp:39: warning: The following parameters of java_bytecode_instrumentt::operator()(codet &code) are not documented: + parameter 'code' +/cbmc/jbmc/src/java_bytecode/java_class_loader.cpp:104: warning: unable to resolve reference to `jar_files' for \ref command +/cbmc/jbmc/src/java_bytecode/simple_method_stubbing.cpp:38: warning: The following parameters of java_simple_method_stubst::create_method_stub_at(const typet &expected_type, const exprt &ptr, const source_locationt &loc, const irep_idt &function_id, code_blockt &parent_block, unsigned insert_before_index, bool is_constructor, bool update_in_place) are not documented: + parameter 'function_id' +/cbmc/jbmc/src/java_bytecode/java_string_library_preprocess.h:250: warning: The following parameters of java_string_library_preprocesst::allocate_fresh_string(const typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table, code_blockt &code) are not documented: + parameter 'function_id' +/cbmc/jbmc/src/java_bytecode/java_string_library_preprocess.cpp:1835: warning: argument 'function_id' of command @param is not found in the argument list of java_string_library_preprocesst::code_for_function(const symbolt &symbol, symbol_table_baset &symbol_table) +/cbmc/jbmc/src/java_bytecode/java_string_library_preprocess.cpp:1835: warning: argument 'type' of command @param is not found in the argument list of java_string_library_preprocesst::code_for_function(const symbolt &symbol, symbol_table_baset &symbol_table) +/cbmc/jbmc/src/java_bytecode/java_string_library_preprocess.cpp:1835: warning: argument 'loc' of command @param is not found in the argument list of java_string_library_preprocesst::code_for_function(const symbolt &symbol, symbol_table_baset &symbol_table) +/cbmc/jbmc/src/java_bytecode/java_string_library_preprocess.h:52: warning: The following parameters of java_string_library_preprocesst::code_for_function(const symbolt &symbol, symbol_table_baset &symbol_table) are not documented: + parameter 'symbol' +/cbmc/jbmc/src/java_bytecode/java_string_library_preprocess.h:332: warning: The following parameters of java_string_library_preprocesst::make_argument_for_format(const exprt &argv, std::size_t index, const struct_typet &structured_type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table, code_blockt &code) are not documented: + parameter 'function_id' +/cbmc/jbmc/src/java_bytecode/java_string_library_preprocess.h:166: warning: The following parameters of java_string_library_preprocesst::make_copy_string_code(const java_method_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table) are not documented: + parameter 'function_id' +/cbmc/jbmc/src/java_bytecode/java_string_library_preprocess.h:148: warning: The following parameters of java_string_library_preprocesst::make_float_to_string_code(const java_method_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table) are not documented: + parameter 'function_id' +/cbmc/jbmc/src/java_bytecode/java_string_library_preprocess.cpp:1085: warning: Unsupported xml/html tag found +/cbmc/jbmc/src/java_bytecode/java_string_library_preprocess.h:184: warning: The following parameters of java_string_library_preprocesst::make_object_get_class_code(const java_method_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table) are not documented: + parameter 'function_id' +/cbmc/jbmc/src/java_bytecode/java_string_library_preprocess.h:160: warning: The following parameters of java_string_library_preprocesst::make_string_format_code(const java_method_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table) are not documented: + parameter 'function_id' +/cbmc/src/util/json_irep.cpp:21: warning: argument 'include_comments' of command @param is not found in the argument list of json_irept::json_irept(bool _include_comments) +/cbmc/src/util/json_irep.h:23: warning: The following parameters of json_irept::json_irept(bool _include_comments) are not documented: + parameter '_include_comments' +/cbmc/src/util/json_irep.cpp:98: warning: argument 'input' of command @param is not found in the argument list of json_irept::convert_from_json(const jsont &in) const +/cbmc/src/util/json_irep.h:25: warning: The following parameters of json_irept::convert_from_json(const jsont &in) const are not documented: + parameter 'in' +/cbmc/src/langapi/language_file.cpp:51: warning: argument 'should_generate_stubs' of command @param is not found in the argument list of language_filest::set_should_generate_opaque_method_stubs(bool stubs_enabled) +/cbmc/src/langapi/language_file.h:104: warning: The following parameters of language_filest::set_should_generate_opaque_method_stubs(bool stubs_enabled) are not documented: + parameter 'stubs_enabled' +/cbmc/src/langapi/language.cpp:121: warning: argument 'parameter_type' of command @param is not found in the argument list of languaget::build_stub_parameter_symbol(const symbolt &function_symbol, size_t parameter_index, const code_typet::parametert ¶meter) +/cbmc/src/langapi/language.h:176: warning: The following parameters of languaget::build_stub_parameter_symbol(const symbolt &function_symbol, size_t parameter_index, const code_typet::parametert ¶meter) are not documented: + parameter 'parameter' +/cbmc/src/goto-programs/rebuild_goto_start_function.h:31: warning: The following parameters of rebuild_goto_start_function_baset::rebuild_goto_start_function_baset(const optionst &options, maybe_lazy_goto_modelt &goto_model, message_handlert &message_handler) are not documented: + parameter 'options' + parameter 'message_handler' +/cbmc/src/goto-programs/rebuild_goto_start_function.cpp:37: warning: argument 'entry_function' of command @param is not found in the argument list of rebuild_goto_start_function_baset< maybe_lazy_goto_modelt >::operator()(void) +/cbmc/jbmc/src/java_bytecode/remove_exceptions.cpp:47: warning: Found unknown command `\class_identifier' +/cbmc/src/goto-programs/resolve_inherited_component.cpp:13: warning: argument 'class_hierarchy' of command @param is not found in the argument list of resolve_inherited_componentt::resolve_inherited_componentt(const symbol_tablet &symbol_table, const class_hierarchyt &clas_hierarchy) +/cbmc/src/goto-programs/resolve_inherited_component.h:24: warning: The following parameters of resolve_inherited_componentt::resolve_inherited_componentt(const symbol_tablet &symbol_table, const class_hierarchyt &clas_hierarchy) are not documented: + parameter 'clas_hierarchy' +/cbmc/jbmc/src/java_bytecode/select_pointer_type.h:50: warning: The following parameters of select_pointer_typet::specialize_generics(const pointer_typet &pointer_type, const generic_parameter_specialization_mapt &generic_parameter_specialization_map, generic_parameter_recursion_trackingt &visited_nodes) const are not documented: + parameter 'visited_nodes' +/cbmc/src/goto-programs/show_goto_functions_xml.cpp:35: warning: Unsupported xml/html tag found +/cbmc/src/goto-programs/show_goto_functions_xml.cpp:36: warning: Unsupported xml/html tag found +/cbmc/src/goto-programs/show_goto_functions_xml.cpp:37: warning: Unsupported xml/html tag found +/cbmc/src/goto-programs/show_goto_functions_xml.cpp:37: warning: Unsupported xml/html tag found +/cbmc/src/goto-programs/show_goto_functions_xml.cpp:38: warning: Unsupported xml/html tag found +/cbmc/src/goto-programs/show_goto_functions_xml.cpp:39: warning: Unsupported xml/html tag found +/cbmc/src/goto-programs/show_goto_functions_xml.cpp:39: warning: Unsupported xml/html tag found +/cbmc/src/goto-programs/show_goto_functions_xml.cpp:39: warning: Unsupported xml/html tag found +/cbmc/src/goto-programs/show_goto_functions_xml.cpp:39: warning: Unsupported xml/html tag found +/cbmc/src/goto-programs/show_goto_functions_xml.cpp:39: warning: Unsupported xml/html tag found +/cbmc/src/solvers/refinement/string_refinement.cpp:2099: warning: argument 'expr' of command @param is not found in the argument list of string_constraintt::universal_only_in_index(const string_constraintt &constr) +/cbmc/src/solvers/refinement/string_refinement.cpp:2106: warning: The following parameters of string_constraintt::universal_only_in_index(const string_constraintt &constr) are not documented: + parameter 'constr' +/cbmc/src/goto-programs/goto_trace.cpp:132: warning: The following parameters of numeric_representation(const constant_exprt &expr, const namespacet &ns, const trace_optionst &options) are not documented: + parameter 'ns' +/cbmc/jbmc/src/java_bytecode/README.md:26: warning: unable to resolve reference to `java-bytecode-remove-instance-of' for \ref command +/cbmc/jbmc/src/java_bytecode/README.md:89: warning: explicit link request to 'define' could not be resolved +/cbmc/jbmc/src/java_bytecode/README.md:89: warning: explicit link request to 'define' could not be resolved +/cbmc/jbmc/src/java_bytecode/ci_lazy_methods_needed.h:40: warning: The following parameters of ci_lazy_methods_neededt::add_needed_class(const irep_idt &class_symbol_name) are not documented: + parameter 'class_symbol_name' +/cbmc/jbmc/src/java_bytecode/ci_lazy_methods_needed.h:38: warning: The following parameters of ci_lazy_methods_neededt::add_needed_method(const irep_idt &method_symbol_name) are not documented: + parameter 'method_symbol_name' +/cbmc/src/pointer-analysis/dereference.h:26: warning: argument '_new_symbol_table' of command @param is not found in the argument list of dereferencet::dereferencet(const namespacet &_ns) +/cbmc/src/pointer-analysis/dereference.h:26: warning: argument '_options' of command @param is not found in the argument list of dereferencet::dereferencet(const namespacet &_ns) +/cbmc/src/pointer-analysis/dereference.h:26: warning: argument '_dereference_callback' of command @param is not found in the argument list of dereferencet::dereferencet(const namespacet &_ns) +/cbmc/src/goto-programs/rebuild_goto_start_function.cpp:22: warning: argument '_message_handler' of command @param is not found in the argument list of rebuild_goto_start_function_baset< maybe_lazy_goto_modelt >::rebuild_goto_start_function_baset(const optionst &options, maybe_lazy_goto_modelt &goto_model, message_handlert &message_handler) diff --git a/scripts/filter_expected_warnings.py b/scripts/filter_expected_warnings.py new file mode 100755 index 00000000000..bfe6476f210 --- /dev/null +++ b/scripts/filter_expected_warnings.py @@ -0,0 +1,119 @@ +#!/usr/bin/env python +"""Script to filter out old warnings from doxygen.""" + +import sys +import re + + +class DoxygenWarning(object): + """Doxygen warning class.""" + + def __init__(self, firstline, filename, warning): + self.firstline = firstline + self.filename = filename + self.warning = warning + self.otherlines = [] + + def equals_ignoring_path_and_line_number(self, other): + """Return true if warnings have same filename and warning message.""" + if self.filename != other.filename: + return False + if self.warning != other.warning: + return False + return self.otherlines == other.otherlines + + def print_with_prefix(self, prefix): + print(prefix + self.firstline) + for line in self.otherlines: + print(prefix + ' ' + line) + + +class WarningsList(object): + """List of Doxygen warnings.""" + + def __init__(self, all_lines): + """Create a list of the warnings in this file.""" + self.warnings_list = [] + current = None + + warning_start_expr = re.compile(r'[^:]+/([^:/]+):\d+: (warning.*$)') + + for line in all_lines: + if line.isspace(): + continue + + # Allow comments in the list of expected warnings. + if line.startswith('#'): + continue + + matched = warning_start_expr.match(line) + if matched: + filename = matched.group(1) + warning = matched.group(2) + current = DoxygenWarning(line.strip(), filename, warning) + self.warnings_list.append(current) + elif line.startswith(' '): + current.otherlines.append(line.strip()) + else: + # Assuming all warnings are of the form [path:line: warning:...] + # (and the warnings about too many nodes have been filtered out). + print('Error filtering warnings: Unexpected input format.') + print(' Input:' + line) + + def contains(self, warning): + """Check if a similar warning is in this list.""" + for other in self.warnings_list: + if warning.equals_ignoring_path_and_line_number(other): + return True + return False + + def print_warnings_not_in_other_list(self, other, prefix): + """Check if this a subset of other, and print anything missing.""" + missing_element_found = False + for warning in self.warnings_list: + if not other.contains(warning): + missing_element_found = True + warning.print_with_prefix(prefix) + return missing_element_found + + +def ignore_too_many_nodes(all_lines): + """Filter out lines about graphs with too many nodes.""" + too_many_nodes_expr = re.compile( + r'warning: Include(d by)? graph for .* not generated, too many nodes. ' + + r'Consider increasing DOT_GRAPH_MAX_NODES.') + return [x for x in all_lines if not too_many_nodes_expr.match(x)] + + +def filter_expected_warnings(expected_warnings_path): + """Filter lines from stdin and print to stdout.""" + with open(expected_warnings_path, "r") as warnings_file: + expected_warnings = WarningsList(warnings_file.readlines()) + + new_warnings = WarningsList(ignore_too_many_nodes(sys.stdin.readlines())) + + # print unexpected warnings + unexpected_warning_found = new_warnings.print_warnings_not_in_other_list( + expected_warnings, '') + + # print expected warnings which aren't found + expected_warning_not_found = expected_warnings.print_warnings_not_in_other_list( + new_warnings, '-') + + if expected_warning_not_found: + print('NOTE: Warnings prefixed with \'-\' are expected ' + + 'warnings which weren\'t found.') + print(' Please update the list of expected warnings.') + + return unexpected_warning_found or expected_warning_not_found + + +if __name__ == "__main__": + + if len(sys.argv) != 2: + print('usage: filter_expected_warnings.py ') + print('(warnings from stdin are filtered and printed to stdout)') + sys.exit(1) + + problem_found = filter_expected_warnings(sys.argv[1]) + sys.exit(1 if problem_found else 0) diff --git a/scripts/run_doxygen.sh b/scripts/run_doxygen.sh new file mode 100755 index 00000000000..88345e1bd3b --- /dev/null +++ b/scripts/run_doxygen.sh @@ -0,0 +1,5 @@ +#!/bin/bash + +SCRIPT_FOLDER=`dirname $0` +cd $SCRIPT_FOLDER/../src +doxygen 2>&1 | ../scripts/filter_expected_warnings.py ../scripts/expected_doxygen_warnings.txt