Add support for uninterpreted function stub #3112
Labels
[C] Feature / Enhancement
A new feature request or enhancement to an existing feature.
T-User
Tag user issues / requests
Requested feature: Stubs that behave like an uninterpreted function.
Use case: Generating stubs that return the same arbitrary value for multiple invocations if the inputs are the same.
Link to relevant documentation (Rust reference, Nomicon, RFC): http://www.cprover.org/cprover-manual/modeling/nondeterminism/ and https://model-checking.github.io/kani/rfc/rfcs/0002-function-stubbing.html#future-possibilities
Example:
Note: We will have to figure out the best mechanism to only return valid values.
The text was updated successfully, but these errors were encountered: