Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Stubbing with Contracts #2621

Closed
JustusAdam opened this issue Jul 24, 2023 · 1 comment · Fixed by #2746
Closed

Stubbing with Contracts #2621

JustusAdam opened this issue Jul 24, 2023 · 1 comment · Fixed by #2746
Assignees
@JustusAdam
Labels
[C] Feature / Enhancement A new feature request or enhancement to an existing feature.
Milestone
Function Contracts

Comments

@JustusAdam
Copy link
Contributor

No description provided.

@JustusAdam JustusAdam self-assigned this Jul 24, 2023
@JustusAdam JustusAdam added this to the Function Contracts MVP milestone Jul 24, 2023
@JustusAdam
Copy link
Contributor Author

This works now since we changed the contract implementation to use stubbing under the hood.

@JustusAdam JustusAdam mentioned this issue Sep 7, 2023
Merged
4 tasks
@tautschnig tautschnig added the [C] Feature / Enhancement A new feature request or enhancement to an existing feature. label Sep 22, 2023
JustusAdam added a commit that referenced this issue Sep 27, 2023
@JustusAdam @celinval @feliperodri
Simple Stubbing with Contracts (#2746)
dba1674 
### Description of changes: 

Expands the contract features introduced in #2655 by completing the
checking with stubbing/replacement capabilities.

### Resolved issues:

Resolves #2621 

### Related RFC: [0009 Function
Contracts](https://model-checking.github.io/kani/rfc/rfcs/0009-function-contracts.html)

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

---------

Co-authored-by: Celina G. Val <celinval@amazon.com>
Co-authored-by: Felipe R. Monteiro <rms.felipe@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@JustusAdam JustusAdam

Labels
[C] Feature / Enhancement A new feature request or enhancement to an existing feature.
Projects
No open projects
Kani 2023-08-01
Status: Done
Milestone
Function Contracts
Development

Successfully merging a pull request may close this issue.

Simple Stubbing with Contracts JustusAdam/kani
2 participants
@tautschnig @JustusAdam