contract generates many calls, such as on str, iterator, and ub_checks

[zjp-CN]

#[kani::requires(a > 0)]
#[kani::ensures(|&ret| ret > 0)]
fn contract(a: u8) -> u8 {
    a
}

#[kani::proof]
fn single_contract() {
    let val = contract(1);
    assert!(val > 0);
}

This proof generates many calls that relates to str, iterator, and ub_checks:

// str calls
{
"def_id": "DefId { id: 230, name: \"<std::str::Chars<'a> as std::iter::Iterator>::next\" }",
"file": "library/core/src/str/iter.rs",
"func": "fn next(&mut self) -> Option<char> {\n        // SAFETY: `str` invariant says `self.iter` is a valid UTF-8 string and\n        // the resulting `ch` is a valid Unicode Scalar Value.\n        unsafe { next_code_point(&mut self.iter).map(|ch| char::from_u32_unchecked(ch)) }\n    }"
},
{
"def_id": "DefId { id: 100, name: \"std::str::Chars::<'a>::as_str\" }",
"file": "library/core/src/str/iter.rs",
"func": "pub fn as_str(&self) -> &'a str {\n        // SAFETY: `Chars` is only made from a str, which guarantees the iter is valid UTF-8.\n        unsafe { from_utf8_unchecked(self.iter.as_slice()) }\n    }"
},
{
"def_id": "DefId { id: 85, name: \"std::str::CharIndices::<'a>::offset\" }",
"file": "library/core/src/str/iter.rs",
"func": "pub fn offset(&self) -> usize {\n        self.front_offset\n    }"
},
{
"def_id": "DefId { id: 234, name: \"<std::str::Chars<'a> as std::iter::Iterator>::next::{closure#0}\" }",
"file": "library/core/src/str/iter.rs",
"func": "|ch| char::from_u32_unchecked(ch)"
},

// iterator calls
{
"def_id": "DefId { id: 73, name: \"<I as std::iter::IntoIterator>::into_iter\" }",
"file": "library/core/src/iter/traits/collect.rs",
"func": "fn into_iter(self) -> I {\n        self\n    }"

},
{
"def_id": "DefId { id: 73, name: \"<I as std::iter::IntoIterator>::into_iter\" }",
"file": "library/core/src/iter/traits/collect.rs",
"func": "fn into_iter(self) -> I {\n        self\n    }"
},
{
"def_id": "DefId { id: 73, name: \"<I as std::iter::IntoIterator>::into_iter\" }",
"file": "library/core/src/iter/traits/collect.rs",
"func": "fn into_iter(self) -> I {\n        self\n    }"
},


// ub_checks
{
"def_id": "DefId { id: 138, name: \"std::hint::unreachable_unchecked::precondition_check\" }",
"file": "library/core/src/ub_checks.rs",
"func": "const fn precondition_check($($name:$ty),*) {\n                if !$e {\n                    ::core::panicking::panic_nounwind(concat!(\"unsafe precondition(s) violated: \", $message,\n                        \"\\n\\nThis indicates a bug in the program. \\\n                        This Undefined Behavior check is optional, and cannot be relied on for safety.\"));\n                }\n            }"
},

{
"def_id": "DefId { id: 105, name: \"std::num::NonZero::<T>::new_unchecked::precondition_check\" }",

"file": "library/core/src/ub_checks.rs",
"func": "const fn precondition_check($($name:$ty),*) {\n                if !$e {\n                    ::core::panicking::panic_nounwind(concat!(\"unsafe precondition(s) violated: \", $message,\n                        \"\\n\\nThis indicates a bug in the program. \\\n                        This Undefined Behavior check is optional, and cannot be relied on for safety.\"));\n                }\n            }"
},