-
Notifications
You must be signed in to change notification settings - Fork 277
Open
Labels
KaniBugs or features of importance to Kani Rust VerifierBugs or features of importance to Kani Rust VerifierawsBugs or features of importance to AWS CBMC usersBugs or features of importance to AWS CBMC users
Description
Function calls are currently supported in function contracts, however they are not allowed in quantifiers. This is inconsistent and unintuitive, since the logical restrictions for function calls in contracts apply the same way in quantifiers.
Having the capability to call functions in quantifiers is important for the implementation of model-checking/kani#2546. This is for two reasons
- The code generation in that implementation turns the body of Rust-level quantifiers into a function and then calls that function from the goto-C-level quantifier. This could be worked around but
- Small functions (especially methods) are very common in Rust, e.g. the
std::ops::Eq::eq
function which overloads==
orstd::ops::Ord::cmp
which overloads comparison. As a result these are likely to be used by users of kani's function contracts.
I would ask that CBMC should lift the arbitrary restriction on function calls in quantifiers and enforce side-effect freedom the same way it does in function contracts otherwise.
Metadata
Metadata
Assignees
Labels
KaniBugs or features of importance to Kani Rust VerifierBugs or features of importance to Kani Rust VerifierawsBugs or features of importance to AWS CBMC usersBugs or features of importance to AWS CBMC users