Verified Function doesn't exist in some cases

[zjp-CN]

https://github.com/model-checking/verify-rust-std/blob/ca495357a162029276f9a4c7161bedc60e1b10c7/library/alloc/src/collections/vec_deque/mod.rs#L3309

Harness Name: 
collections::vec_deque::verify::check_vecdeque_swap
Harness File: alloc/src/collections/vec_deque/mod.rs
Harness Hash: 1767766264421952135714692912618106014787
Proof Kind: Standard
Total Properties: 484
Execution Time: 11786ms

Verified Function: 
collections::vec_deque::vecdeque_swap 👈 there is no such function in source code, maybe computed from harness name?
Function File: alloc/src/collections/vec_deque/mod.rs

[zjp-CN]

Harness Name: 
vec::verify::verify_swap_remove
Crate: alloc
Harness File: alloc/src/vec/mod.rs

Verified Function: 
vec::swap_remove
Function File: alloc/src/vec/mod.rs

For this, vec::swap_remove is incomplete, because Vec carries generics.