The documentation build system has numerous broken links

[thomasspriggs]

The documentation build system has numerous broken links. The steps to reproduce are -

• git checkout develop
• cd doc/doxygen-root
• make 2> output.txt
• grep resolve output.txt

The results are below -

Click here to see warnings which should really be considered errors.

src/goto-instrument/contracts/dynamic-frames/dfcc_library.h:436: warning: unable to resolve reference to '__CPROVER_contracts_check_replace_ensures_was_freed_preconditions' for \ref command
src/goto-instrument/contracts/dynamic-frames/dfcc_library.h:422: warning: unable to resolve reference to '__CPROVER_contracts_link_allocated' for \ref command
src/goto-instrument/contracts/dynamic-frames/dfcc_library.h:429: warning: unable to resolve reference to '__CPROVER_contracts_link_deallocated' for \ref command
src/goto-instrument/contracts/dynamic-frames/dfcc_library.h:415: warning: unable to resolve reference to '__CPROVER_contracts_link_is_fresh' for \ref command
src/goto-instrument/contracts/dynamic-frames/dfcc_library.h:443: warning: unable to resolve reference to '__CPROVER_contracts_obj_set_create_indexed_by_object_id' for \ref command
src/goto-instrument/contracts/dynamic-frames/dfcc_library.h:449: warning: unable to resolve reference to '__CPROVER_contracts_obj_set_release' for \ref command
src/goto-instrument/contracts/dynamic-frames/dfcc_library.h:309: warning: unable to resolve reference to '__CPROVER_contracts_write_set_add_allocated' for \ref command
src/goto-instrument/contracts/dynamic-frames/dfcc_library.h:315: warning: unable to resolve reference to '__CPROVER_contracts_write_set_add_decl' for \ref command
src/goto-instrument/contracts/dynamic-frames/dfcc_library.h:335: warning: unable to resolve reference to '__CPROVER_contracts_write_set_check_allocated_deallocated_is_empty' for \ref command
src/goto-instrument/contracts/dynamic-frames/dfcc_library.h:359: warning: unable to resolve reference to '__CPROVER_contracts_write_set_check_array_copy' for \ref command
src/goto-instrument/contracts/dynamic-frames/dfcc_library.h:367: warning: unable to resolve reference to '__CPROVER_contracts_write_set_check_array_replace' for \ref command
src/goto-instrument/contracts/dynamic-frames/dfcc_library.h:351: warning: unable to resolve reference to '__CPROVER_contracts_write_set_check_array_set' for \ref command
src/goto-instrument/contracts/dynamic-frames/dfcc_library.h:342: warning: unable to resolve reference to '__CPROVER_contracts_write_set_check_assignment' for \ref command
src/goto-instrument/contracts/dynamic-frames/dfcc_library.h:392: warning: unable to resolve reference to '__CPROVER_contracts_write_set_check_assigns_clause_inclusion' for \ref command
src/goto-instrument/contracts/dynamic-frames/dfcc_library.h:384: warning: unable to resolve reference to '__CPROVER_contracts_write_set_check_deallocate' for \ref command
src/goto-instrument/contracts/dynamic-frames/dfcc_library.h:400: warning: unable to resolve reference to '__CPROVER_contracts_write_set_check_frees_clause_inclusion' for \ref command
src/goto-instrument/contracts/dynamic-frames/dfcc_library.h:376: warning: unable to resolve reference to '__CPROVER_contracts_write_set_check_havoc_object' for \ref command
src/goto-instrument/contracts/dynamic-frames/dfcc_library.h:291: warning: unable to resolve reference to '__CPROVER_contracts_write_set_create' for \ref command
src/goto-instrument/contracts/dynamic-frames/dfcc_library.h:408: warning: unable to resolve reference to '__CPROVER_contracts_write_set_deallocate_freeable' for \ref command
src/goto-instrument/contracts/dynamic-frames/dfcc_library.h:321: warning: unable to resolve reference to '__CPROVER_contracts_write_set_record_dead' for \ref command
src/goto-instrument/contracts/dynamic-frames/dfcc_library.h:328: warning: unable to resolve reference to '__CPROVER_contracts_write_set_record_deallocated' for \ref command
src/goto-instrument/contracts/dynamic-frames/dfcc_library.h:304: warning: unable to resolve reference to '__CPROVER_contracts_write_set_release' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-spec-rewriting.md:53: warning: unable to resolve reference to 'cprover_contracts.c' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-spec-rewriting.md:126: warning: unable to resolve reference to 'cprover_contracts.c' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc.md:25: warning: unable to resolve reference to '__CPROVER_contracts_write_set_t' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc.md:25: warning: unable to resolve reference to 'cprover_contracts.c' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc.md:27: warning: unable to resolve reference to '__CPROVER_contracts_write_set_t' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc.md:61: warning: unable to resolve reference to '__CPROVER_contracts_write_set_t' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc.md:62: warning: unable to resolve reference to 'cprover_contracts.c' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc.md:74: warning: unable to resolve reference to '__CPROVER_contracts_write_set_ptr_t' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:10: warning: unable to resolve reference to 'cprover_contracts.c' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:13: warning: unable to resolve reference to '__CPROVER_contracts_car_t' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:33: warning: unable to resolve reference to '__CPROVER_contracts_car_t' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:34: warning: unable to resolve reference to '__CPROVER_contracts_car_set_t' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:35: warning: unable to resolve reference to '__CPROVER_contracts_car_set_create' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:48: warning: unable to resolve reference to '__CPROVER_contracts_car_t' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:51: warning: unable to resolve reference to '__CPROVER_contracts_obj_set_t' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:94: warning: unable to resolve reference to '__CPROVER_contracts_write_set_t' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:144: warning: unable to resolve reference to '__CPROVER_contracts_write_set_t' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:145: warning: unable to resolve reference to 'cprover_contracts.c' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:146: warning: unable to resolve reference to '__CPROVER_contracts_write_set_create' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:147: warning: unable to resolve reference to '__CPROVER_contracts_write_set_release' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:148: warning: unable to resolve reference to '__CPROVER_contracts_write_set_insert_assignable' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:149: warning: unable to resolve reference to '__CPROVER_contracts_write_set_insert_object_whole' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:150: warning: unable to resolve reference to '__CPROVER_contracts_write_set_insert_object_from' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:151: warning: unable to resolve reference to '__CPROVER_contracts_write_set_insert_object_upto' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:152: warning: unable to resolve reference to '__CPROVER_contracts_write_set_add_freeable' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:153: warning: unable to resolve reference to '__CPROVER_contracts_write_set_add_allocated' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:154: warning: unable to resolve reference to '__CPROVER_contracts_write_set_record_dead' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:155: warning: unable to resolve reference to '__CPROVER_contracts_write_set_record_deallocated' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:156: warning: unable to resolve reference to '__CPROVER_contracts_write_set_check_allocated_deallocated_is_empty' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:157: warning: unable to resolve reference to '__CPROVER_contracts_write_set_check_assignment' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:158: warning: unable to resolve reference to '__CPROVER_contracts_write_set_check_array_set' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:159: warning: unable to resolve reference to '__CPROVER_contracts_write_set_check_array_copy' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:160: warning: unable to resolve reference to '__CPROVER_contracts_write_set_check_array_replace' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:161: warning: unable to resolve reference to '__CPROVER_contracts_write_set_check_havoc_object' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:162: warning: unable to resolve reference to '__CPROVER_contracts_write_set_check_deallocate' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:163: warning: unable to resolve reference to '__CPROVER_contracts_write_set_check_assigns_clause_inclusion' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:164: warning: unable to resolve reference to '__CPROVER_contracts_write_set_check_frees_clause_inclusion' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:165: warning: unable to resolve reference to '__CPROVER_contracts_write_set_deallocate_freeable' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:166: warning: unable to resolve reference to '__CPROVER_contracts_link_allocated' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:167: warning: unable to resolve reference to '__CPROVER_contracts_link_deallocated' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:168: warning: unable to resolve reference to '__CPROVER_contracts_is_fresh' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:169: warning: unable to resolve reference to '__CPROVER_contracts_write_set_havoc_get_assignable_target' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:170: warning: unable to resolve reference to '__CPROVER_contracts_write_set_havoc_object_whole' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:171: warning: unable to resolve reference to '__CPROVER_contracts_write_set_havoc_slice' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:172: warning: unable to resolve reference to '__CPROVER_contracts_is_freeable' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:173: warning: unable to resolve reference to '__CPROVER_contracts_was_freed' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:174: warning: unable to resolve reference to '__CPROVER_contracts_check_replace_ensures_was_freed_preconditions' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-arch.md:50: warning: unable to resolve reference to 'cprover_contracts.c' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-arch.md:50: warning: unable to resolve reference to 'cprover_contracts.c' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:10: warning: unable to resolve reference to 'cprover_contracts.c' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:13: warning: unable to resolve reference to '__CPROVER_contracts_car_t' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:33: warning: unable to resolve reference to '__CPROVER_contracts_car_t' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:34: warning: unable to resolve reference to '__CPROVER_contracts_car_set_t' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:35: warning: unable to resolve reference to '__CPROVER_contracts_car_set_create' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:48: warning: unable to resolve reference to '__CPROVER_contracts_car_t' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:51: warning: unable to resolve reference to '__CPROVER_contracts_obj_set_t' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:94: warning: unable to resolve reference to '__CPROVER_contracts_write_set_t' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:144: warning: unable to resolve reference to '__CPROVER_contracts_write_set_t' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:145: warning: unable to resolve reference to 'cprover_contracts.c' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:146: warning: unable to resolve reference to '__CPROVER_contracts_write_set_create' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:147: warning: unable to resolve reference to '__CPROVER_contracts_write_set_release' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:148: warning: unable to resolve reference to '__CPROVER_contracts_write_set_insert_assignable' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:149: warning: unable to resolve reference to '__CPROVER_contracts_write_set_insert_object_whole' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:150: warning: unable to resolve reference to '__CPROVER_contracts_write_set_insert_object_from' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:151: warning: unable to resolve reference to '__CPROVER_contracts_write_set_insert_object_upto' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:152: warning: unable to resolve reference to '__CPROVER_contracts_write_set_add_freeable' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:153: warning: unable to resolve reference to '__CPROVER_contracts_write_set_add_allocated' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:154: warning: unable to resolve reference to '__CPROVER_contracts_write_set_record_dead' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:155: warning: unable to resolve reference to '__CPROVER_contracts_write_set_record_deallocated' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:156: warning: unable to resolve reference to '__CPROVER_contracts_write_set_check_allocated_deallocated_is_empty' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:157: warning: unable to resolve reference to '__CPROVER_contracts_write_set_check_assignment' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:158: warning: unable to resolve reference to '__CPROVER_contracts_write_set_check_array_set' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:159: warning: unable to resolve reference to '__CPROVER_contracts_write_set_check_array_copy' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:160: warning: unable to resolve reference to '__CPROVER_contracts_write_set_check_array_replace' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:161: warning: unable to resolve reference to '__CPROVER_contracts_write_set_check_havoc_object' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:162: warning: unable to resolve reference to '__CPROVER_contracts_write_set_check_deallocate' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:163: warning: unable to resolve reference to '__CPROVER_contracts_write_set_check_assigns_clause_inclusion' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:164: warning: unable to resolve reference to '__CPROVER_contracts_write_set_check_frees_clause_inclusion' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:165: warning: unable to resolve reference to '__CPROVER_contracts_write_set_deallocate_freeable' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:166: warning: unable to resolve reference to '__CPROVER_contracts_link_allocated' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:167: warning: unable to resolve reference to '__CPROVER_contracts_link_deallocated' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:168: warning: unable to resolve reference to '__CPROVER_contracts_is_fresh' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:169: warning: unable to resolve reference to '__CPROVER_contracts_write_set_havoc_get_assignable_target' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:170: warning: unable to resolve reference to '__CPROVER_contracts_write_set_havoc_object_whole' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:171: warning: unable to resolve reference to '__CPROVER_contracts_write_set_havoc_slice' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:172: warning: unable to resolve reference to '__CPROVER_contracts_is_freeable' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:173: warning: unable to resolve reference to '__CPROVER_contracts_was_freed' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:174: warning: unable to resolve reference to '__CPROVER_contracts_check_replace_ensures_was_freed_preconditions' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc.md:25: warning: unable to resolve reference to '__CPROVER_contracts_write_set_t' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc.md:25: warning: unable to resolve reference to 'cprover_contracts.c' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc.md:27: warning: unable to resolve reference to '__CPROVER_contracts_write_set_t' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc.md:61: warning: unable to resolve reference to '__CPROVER_contracts_write_set_t' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc.md:62: warning: unable to resolve reference to 'cprover_contracts.c' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc.md:74: warning: unable to resolve reference to '__CPROVER_contracts_write_set_ptr_t' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:10: warning: unable to resolve reference to 'cprover_contracts.c' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:13: warning: unable to resolve reference to '__CPROVER_contracts_car_t' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:33: warning: unable to resolve reference to '__CPROVER_contracts_car_t' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:34: warning: unable to resolve reference to '__CPROVER_contracts_car_set_t' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:35: warning: unable to resolve reference to '__CPROVER_contracts_car_set_create' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:48: warning: unable to resolve reference to '__CPROVER_contracts_car_t' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:51: warning: unable to resolve reference to '__CPROVER_contracts_obj_set_t' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:94: warning: unable to resolve reference to '__CPROVER_contracts_write_set_t' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:144: warning: unable to resolve reference to '__CPROVER_contracts_write_set_t' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:145: warning: unable to resolve reference to 'cprover_contracts.c' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:146: warning: unable to resolve reference to '__CPROVER_contracts_write_set_create' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:147: warning: unable to resolve reference to '__CPROVER_contracts_write_set_release' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:148: warning: unable to resolve reference to '__CPROVER_contracts_write_set_insert_assignable' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:149: warning: unable to resolve reference to '__CPROVER_contracts_write_set_insert_object_whole' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:150: warning: unable to resolve reference to '__CPROVER_contracts_write_set_insert_object_from' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:151: warning: unable to resolve reference to '__CPROVER_contracts_write_set_insert_object_upto' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:152: warning: unable to resolve reference to '__CPROVER_contracts_write_set_add_freeable' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:153: warning: unable to resolve reference to '__CPROVER_contracts_write_set_add_allocated' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:154: warning: unable to resolve reference to '__CPROVER_contracts_write_set_record_dead' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:155: warning: unable to resolve reference to '__CPROVER_contracts_write_set_record_deallocated' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:156: warning: unable to resolve reference to '__CPROVER_contracts_write_set_check_allocated_deallocated_is_empty' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:157: warning: unable to resolve reference to '__CPROVER_contracts_write_set_check_assignment' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:158: warning: unable to resolve reference to '__CPROVER_contracts_write_set_check_array_set' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:159: warning: unable to resolve reference to '__CPROVER_contracts_write_set_check_array_copy' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:160: warning: unable to resolve reference to '__CPROVER_contracts_write_set_check_array_replace' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:161: warning: unable to resolve reference to '__CPROVER_contracts_write_set_check_havoc_object' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:162: warning: unable to resolve reference to '__CPROVER_contracts_write_set_check_deallocate' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:163: warning: unable to resolve reference to '__CPROVER_contracts_write_set_check_assigns_clause_inclusion' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:164: warning: unable to resolve reference to '__CPROVER_contracts_write_set_check_frees_clause_inclusion' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:165: warning: unable to resolve reference to '__CPROVER_contracts_write_set_deallocate_freeable' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:166: warning: unable to resolve reference to '__CPROVER_contracts_link_allocated' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:167: warning: unable to resolve reference to '__CPROVER_contracts_link_deallocated' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:168: warning: unable to resolve reference to '__CPROVER_contracts_is_fresh' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:169: warning: unable to resolve reference to '__CPROVER_contracts_write_set_havoc_get_assignable_target' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:170: warning: unable to resolve reference to '__CPROVER_contracts_write_set_havoc_object_whole' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:171: warning: unable to resolve reference to '__CPROVER_contracts_write_set_havoc_slice' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:172: warning: unable to resolve reference to '__CPROVER_contracts_is_freeable' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:173: warning: unable to resolve reference to '__CPROVER_contracts_was_freed' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:174: warning: unable to resolve reference to '__CPROVER_contracts_check_replace_ensures_was_freed_preconditions' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-spec-rewriting.md:53: warning: unable to resolve reference to 'cprover_contracts.c' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-spec-rewriting.md:126: warning: unable to resolve reference to 'cprover_contracts.c' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-spec-rewriting.md:53: warning: unable to resolve reference to 'cprover_contracts.c' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-spec-rewriting.md:126: warning: unable to resolve reference to 'cprover_contracts.c' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc.md:25: warning: unable to resolve reference to '__CPROVER_contracts_write_set_t' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc.md:25: warning: unable to resolve reference to 'cprover_contracts.c' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc.md:27: warning: unable to resolve reference to '__CPROVER_contracts_write_set_t' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc.md:61: warning: unable to resolve reference to '__CPROVER_contracts_write_set_t' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc.md:62: warning: unable to resolve reference to 'cprover_contracts.c' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc.md:74: warning: unable to resolve reference to '__CPROVER_contracts_write_set_ptr_t' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:10: warning: unable to resolve reference to 'cprover_contracts.c' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:13: warning: unable to resolve reference to '__CPROVER_contracts_car_t' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:33: warning: unable to resolve reference to '__CPROVER_contracts_car_t' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:34: warning: unable to resolve reference to '__CPROVER_contracts_car_set_t' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:35: warning: unable to resolve reference to '__CPROVER_contracts_car_set_create' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:48: warning: unable to resolve reference to '__CPROVER_contracts_car_t' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:51: warning: unable to resolve reference to '__CPROVER_contracts_obj_set_t' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:94: warning: unable to resolve reference to '__CPROVER_contracts_write_set_t' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:144: warning: unable to resolve reference to '__CPROVER_contracts_write_set_t' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:145: warning: unable to resolve reference to 'cprover_contracts.c' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:146: warning: unable to resolve reference to '__CPROVER_contracts_write_set_create' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:147: warning: unable to resolve reference to '__CPROVER_contracts_write_set_release' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:148: warning: unable to resolve reference to '__CPROVER_contracts_write_set_insert_assignable' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:149: warning: unable to resolve reference to '__CPROVER_contracts_write_set_insert_object_whole' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:150: warning: unable to resolve reference to '__CPROVER_contracts_write_set_insert_object_from' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:151: warning: unable to resolve reference to '__CPROVER_contracts_write_set_insert_object_upto' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:152: warning: unable to resolve reference to '__CPROVER_contracts_write_set_add_freeable' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:153: warning: unable to resolve reference to '__CPROVER_contracts_write_set_add_allocated' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:154: warning: unable to resolve reference to '__CPROVER_contracts_write_set_record_dead' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:155: warning: unable to resolve reference to '__CPROVER_contracts_write_set_record_deallocated' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:156: warning: unable to resolve reference to '__CPROVER_contracts_write_set_check_allocated_deallocated_is_empty' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:157: warning: unable to resolve reference to '__CPROVER_contracts_write_set_check_assignment' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:158: warning: unable to resolve reference to '__CPROVER_contracts_write_set_check_array_set' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:159: warning: unable to resolve reference to '__CPROVER_contracts_write_set_check_array_copy' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:160: warning: unable to resolve reference to '__CPROVER_contracts_write_set_check_array_replace' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:161: warning: unable to resolve reference to '__CPROVER_contracts_write_set_check_havoc_object' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:162: warning: unable to resolve reference to '__CPROVER_contracts_write_set_check_deallocate' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:163: warning: unable to resolve reference to '__CPROVER_contracts_write_set_check_assigns_clause_inclusion' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:164: warning: unable to resolve reference to '__CPROVER_contracts_write_set_check_frees_clause_inclusion' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:165: warning: unable to resolve reference to '__CPROVER_contracts_write_set_deallocate_freeable' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:166: warning: unable to resolve reference to '__CPROVER_contracts_link_allocated' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:167: warning: unable to resolve reference to '__CPROVER_contracts_link_deallocated' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:168: warning: unable to resolve reference to '__CPROVER_contracts_is_fresh' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:169: warning: unable to resolve reference to '__CPROVER_contracts_write_set_havoc_get_assignable_target' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:170: warning: unable to resolve reference to '__CPROVER_contracts_write_set_havoc_object_whole' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:171: warning: unable to resolve reference to '__CPROVER_contracts_write_set_havoc_slice' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:172: warning: unable to resolve reference to '__CPROVER_contracts_is_freeable' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:173: warning: unable to resolve reference to '__CPROVER_contracts_was_freed' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:174: warning: unable to resolve reference to '__CPROVER_contracts_check_replace_ensures_was_freed_preconditions' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-spec-rewriting.md:53: warning: unable to resolve reference to 'cprover_contracts.c' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-spec-rewriting.md:126: warning: unable to resolve reference to 'cprover_contracts.c' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc.md:25: warning: unable to resolve reference to '__CPROVER_contracts_write_set_t' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc.md:25: warning: unable to resolve reference to 'cprover_contracts.c' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc.md:27: warning: unable to resolve reference to '__CPROVER_contracts_write_set_t' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc.md:61: warning: unable to resolve reference to '__CPROVER_contracts_write_set_t' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc.md:62: warning: unable to resolve reference to 'cprover_contracts.c' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc.md:74: warning: unable to resolve reference to '__CPROVER_contracts_write_set_ptr_t' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:10: warning: unable to resolve reference to 'cprover_contracts.c' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:13: warning: unable to resolve reference to '__CPROVER_contracts_car_t' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:33: warning: unable to resolve reference to '__CPROVER_contracts_car_t' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:34: warning: unable to resolve reference to '__CPROVER_contracts_car_set_t' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:35: warning: unable to resolve reference to '__CPROVER_contracts_car_set_create' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:48: warning: unable to resolve reference to '__CPROVER_contracts_car_t' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:51: warning: unable to resolve reference to '__CPROVER_contracts_obj_set_t' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:94: warning: unable to resolve reference to '__CPROVER_contracts_write_set_t' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:144: warning: unable to resolve reference to '__CPROVER_contracts_write_set_t' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:145: warning: unable to resolve reference to 'cprover_contracts.c' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:146: warning: unable to resolve reference to '__CPROVER_contracts_write_set_create' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:147: warning: unable to resolve reference to '__CPROVER_contracts_write_set_release' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:148: warning: unable to resolve reference to '__CPROVER_contracts_write_set_insert_assignable' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:149: warning: unable to resolve reference to '__CPROVER_contracts_write_set_insert_object_whole' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:150: warning: unable to resolve reference to '__CPROVER_contracts_write_set_insert_object_from' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:151: warning: unable to resolve reference to '__CPROVER_contracts_write_set_insert_object_upto' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:152: warning: unable to resolve reference to '__CPROVER_contracts_write_set_add_freeable' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:153: warning: unable to resolve reference to '__CPROVER_contracts_write_set_add_allocated' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:154: warning: unable to resolve reference to '__CPROVER_contracts_write_set_record_dead' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:155: warning: unable to resolve reference to '__CPROVER_contracts_write_set_record_deallocated' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:156: warning: unable to resolve reference to '__CPROVER_contracts_write_set_check_allocated_deallocated_is_empty' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:157: warning: unable to resolve reference to '__CPROVER_contracts_write_set_check_assignment' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:158: warning: unable to resolve reference to '__CPROVER_contracts_write_set_check_array_set' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:159: warning: unable to resolve reference to '__CPROVER_contracts_write_set_check_array_copy' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:160: warning: unable to resolve reference to '__CPROVER_contracts_write_set_check_array_replace' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:161: warning: unable to resolve reference to '__CPROVER_contracts_write_set_check_havoc_object' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:162: warning: unable to resolve reference to '__CPROVER_contracts_write_set_check_deallocate' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:163: warning: unable to resolve reference to '__CPROVER_contracts_write_set_check_assigns_clause_inclusion' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:164: warning: unable to resolve reference to '__CPROVER_contracts_write_set_check_frees_clause_inclusion' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:165: warning: unable to resolve reference to '__CPROVER_contracts_write_set_deallocate_freeable' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:166: warning: unable to resolve reference to '__CPROVER_contracts_link_allocated' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:167: warning: unable to resolve reference to '__CPROVER_contracts_link_deallocated' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:168: warning: unable to resolve reference to '__CPROVER_contracts_is_fresh' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:169: warning: unable to resolve reference to '__CPROVER_contracts_write_set_havoc_get_assignable_target' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:170: warning: unable to resolve reference to '__CPROVER_contracts_write_set_havoc_object_whole' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:171: warning: unable to resolve reference to '__CPROVER_contracts_write_set_havoc_slice' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:172: warning: unable to resolve reference to '__CPROVER_contracts_is_freeable' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:173: warning: unable to resolve reference to '__CPROVER_contracts_was_freed' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md:174: warning: unable to resolve reference to '__CPROVER_contracts_check_replace_ensures_was_freed_preconditions' for \ref command
src/goto-instrument/contracts/doc/developer/contracts-dev-arch.md:50: warning: unable to resolve reference to 'cprover_contracts.c' for \ref command
src/goto-instrument/contracts/dynamic-frames/dfcc_library.h:291: warning: unable to resolve reference to '__CPROVER_contracts_write_set_create' for \ref command
src/goto-instrument/contracts/dynamic-frames/dfcc_library.h:304: warning: unable to resolve reference to '__CPROVER_contracts_write_set_release' for \ref command
src/goto-instrument/contracts/dynamic-frames/dfcc_library.h:309: warning: unable to resolve reference to '__CPROVER_contracts_write_set_add_allocated' for \ref command
src/goto-instrument/contracts/dynamic-frames/dfcc_library.h:315: warning: unable to resolve reference to '__CPROVER_contracts_write_set_add_decl' for \ref command
src/goto-instrument/contracts/dynamic-frames/dfcc_library.h:321: warning: unable to resolve reference to '__CPROVER_contracts_write_set_record_dead' for \ref command
src/goto-instrument/contracts/dynamic-frames/dfcc_library.h:328: warning: unable to resolve reference to '__CPROVER_contracts_write_set_record_deallocated' for \ref command
src/goto-instrument/contracts/dynamic-frames/dfcc_library.h:335: warning: unable to resolve reference to '__CPROVER_contracts_write_set_check_allocated_deallocated_is_empty' for \ref command
src/goto-instrument/contracts/dynamic-frames/dfcc_library.h:342: warning: unable to resolve reference to '__CPROVER_contracts_write_set_check_assignment' for \ref command
src/goto-instrument/contracts/dynamic-frames/dfcc_library.h:351: warning: unable to resolve reference to '__CPROVER_contracts_write_set_check_array_set' for \ref command
src/goto-instrument/contracts/dynamic-frames/dfcc_library.h:359: warning: unable to resolve reference to '__CPROVER_contracts_write_set_check_array_copy' for \ref command
src/goto-instrument/contracts/dynamic-frames/dfcc_library.h:367: warning: unable to resolve reference to '__CPROVER_contracts_write_set_check_array_replace' for \ref command
src/goto-instrument/contracts/dynamic-frames/dfcc_library.h:376: warning: unable to resolve reference to '__CPROVER_contracts_write_set_check_havoc_object' for \ref command
src/goto-instrument/contracts/dynamic-frames/dfcc_library.h:384: warning: unable to resolve reference to '__CPROVER_contracts_write_set_check_deallocate' for \ref command
src/goto-instrument/contracts/dynamic-frames/dfcc_library.h:392: warning: unable to resolve reference to '__CPROVER_contracts_write_set_check_assigns_clause_inclusion' for \ref command
src/goto-instrument/contracts/dynamic-frames/dfcc_library.h:400: warning: unable to resolve reference to '__CPROVER_contracts_write_set_check_frees_clause_inclusion' for \ref command
src/goto-instrument/contracts/dynamic-frames/dfcc_library.h:408: warning: unable to resolve reference to '__CPROVER_contracts_write_set_deallocate_freeable' for \ref command
src/goto-instrument/contracts/dynamic-frames/dfcc_library.h:415: warning: unable to resolve reference to '__CPROVER_contracts_link_is_fresh' for \ref command
src/goto-instrument/contracts/dynamic-frames/dfcc_library.h:422: warning: unable to resolve reference to '__CPROVER_contracts_link_allocated' for \ref command
src/goto-instrument/contracts/dynamic-frames/dfcc_library.h:429: warning: unable to resolve reference to '__CPROVER_contracts_link_deallocated' for \ref command
src/goto-instrument/contracts/dynamic-frames/dfcc_library.h:436: warning: unable to resolve reference to '__CPROVER_contracts_check_replace_ensures_was_freed_preconditions' for \ref command
src/goto-instrument/contracts/dynamic-frames/dfcc_library.h:443: warning: unable to resolve reference to '__CPROVER_contracts_obj_set_create_indexed_by_object_id' for \ref command
src/goto-instrument/contracts/dynamic-frames/dfcc_library.h:449: warning: unable to resolve reference to '__CPROVER_contracts_obj_set_release' for \ref command
src/goto-instrument/contracts/dynamic-frames/dfcc_library.h:436: warning: unable to resolve reference to '__CPROVER_contracts_check_replace_ensures_was_freed_preconditions' for \ref command
src/goto-instrument/contracts/dynamic-frames/dfcc_library.h:422: warning: unable to resolve reference to '__CPROVER_contracts_link_allocated' for \ref command
src/goto-instrument/contracts/dynamic-frames/dfcc_library.h:429: warning: unable to resolve reference to '__CPROVER_contracts_link_deallocated' for \ref command
src/goto-instrument/contracts/dynamic-frames/dfcc_library.h:415: warning: unable to resolve reference to '__CPROVER_contracts_link_is_fresh' for \ref command
src/goto-instrument/contracts/dynamic-frames/dfcc_library.h:443: warning: unable to resolve reference to '__CPROVER_contracts_obj_set_create_indexed_by_object_id' for \ref command
src/goto-instrument/contracts/dynamic-frames/dfcc_library.h:449: warning: unable to resolve reference to '__CPROVER_contracts_obj_set_release' for \ref command
src/goto-instrument/contracts/dynamic-frames/dfcc_library.h:309: warning: unable to resolve reference to '__CPROVER_contracts_write_set_add_allocated' for \ref command
src/goto-instrument/contracts/dynamic-frames/dfcc_library.h:315: warning: unable to resolve reference to '__CPROVER_contracts_write_set_add_decl' for \ref command
src/goto-instrument/contracts/dynamic-frames/dfcc_library.h:335: warning: unable to resolve reference to '__CPROVER_contracts_write_set_check_allocated_deallocated_is_empty' for \ref command
src/goto-instrument/contracts/dynamic-frames/dfcc_library.h:359: warning: unable to resolve reference to '__CPROVER_contracts_write_set_check_array_copy' for \ref command
src/goto-instrument/contracts/dynamic-frames/dfcc_library.h:367: warning: unable to resolve reference to '__CPROVER_contracts_write_set_check_array_replace' for \ref command
src/goto-instrument/contracts/dynamic-frames/dfcc_library.h:351: warning: unable to resolve reference to '__CPROVER_contracts_write_set_check_array_set' for \ref command
src/goto-instrument/contracts/dynamic-frames/dfcc_library.h:342: warning: unable to resolve reference to '__CPROVER_contracts_write_set_check_assignment' for \ref command
src/goto-instrument/contracts/dynamic-frames/dfcc_library.h:392: warning: unable to resolve reference to '__CPROVER_contracts_write_set_check_assigns_clause_inclusion' for \ref command
src/goto-instrument/contracts/dynamic-frames/dfcc_library.h:384: warning: unable to resolve reference to '__CPROVER_contracts_write_set_check_deallocate' for \ref command
src/goto-instrument/contracts/dynamic-frames/dfcc_library.h:400: warning: unable to resolve reference to '__CPROVER_contracts_write_set_check_frees_clause_inclusion' for \ref command
src/goto-instrument/contracts/dynamic-frames/dfcc_library.h:376: warning: unable to resolve reference to '__CPROVER_contracts_write_set_check_havoc_object' for \ref command
src/goto-instrument/contracts/dynamic-frames/dfcc_library.h:291: warning: unable to resolve reference to '__CPROVER_contracts_write_set_create' for \ref command
src/goto-instrument/contracts/dynamic-frames/dfcc_library.h:408: warning: unable to resolve reference to '__CPROVER_contracts_write_set_deallocate_freeable' for \ref command
src/goto-instrument/contracts/dynamic-frames/dfcc_library.h:321: warning: unable to resolve reference to '__CPROVER_contracts_write_set_record_dead' for \ref command
src/goto-instrument/contracts/dynamic-frames/dfcc_library.h:328: warning: unable to resolve reference to '__CPROVER_contracts_write_set_record_deallocated' for \ref command
src/goto-instrument/contracts/dynamic-frames/dfcc_library.h:304: warning: unable to resolve reference to '__CPROVER_contracts_write_set_release' for \ref command
doc/cprover-manual/smt2-incr.md:20: warning: unable to resolve reference to 'regression-cbmc-incr-smt2.md' for \ref command
doc/cprover-manual/test-suite.md:113: warning: unable to resolve reference to 'pid_test_suites.xml.md' for \ref command

When the documentation build system was added last year in /.github/workflows/publish.yaml and doc/doxygen-root/Makefile there was no corresponding update to the pull request jobs. Consequently the doxygen checking PR job which runs scripts/run_doxygen.sh has not been using the new build system and the broken links have been accumulating since then.

[tautschnig]

#7578 has been merged, closing.