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

Enable concrete playback for contract and stubs #3389

Merged
merged 13 commits into from
Jul 31, 2024
Merged

Enable concrete playback for contract and stubs #3389

merged 13 commits into from
Jul 31, 2024

Commits on Jul 26, 2024

  1. Add kind to harness metadata 

    This allow us to get more information in the Kani driver about which
kind of proof it is. For proof_for_contract, we can now check which
function is the target.
    @celinval
    celinval committed Jul 26, 2024
    Configuration menu
    Copy the full SHA
    2a95fe2 View commit details
    Browse the repository at this point in the history

  2. Enable concrete playback for stubs / contract

    @celinval
    celinval committed Jul 26, 2024
    Configuration menu
    Copy the full SHA
    a060b80 View commit details
    Browse the repository at this point in the history

  3. Fix concrete playback for array and add test

    @celinval
    celinval committed Jul 26, 2024
    Configuration menu
    Copy the full SHA
    33188d1 View commit details
    Browse the repository at this point in the history

Commits on Jul 27, 2024

  1. Fix clippy

    @celinval
    celinval authored Jul 27, 2024
    Configuration menu
    Copy the full SHA
    a143747 View commit details
    Browse the repository at this point in the history

Commits on Jul 29, 2024

  1. Fix unit tests and apply changes to kani_core

    @celinval
    celinval committed Jul 29, 2024
    Configuration menu
    Copy the full SHA
    5922fdb View commit details
    Browse the repository at this point in the history

  2. Add missing test configuration file

    @celinval
    celinval committed Jul 29, 2024
    Configuration menu
    Copy the full SHA
    e2a2e4a View commit details
    Browse the repository at this point in the history

Commits on Jul 30, 2024

  1. Update library/kani_core/src/arbitrary.rs 

    Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>
    @celinval @zhassan-aws
    celinval and zhassan-aws authored Jul 30, 2024
    Configuration menu
    Copy the full SHA
    eb67857 View commit details
    Browse the repository at this point in the history

  2. Update kani_metadata/src/harness.rs 

    Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>
    @celinval @zhassan-aws
    celinval and zhassan-aws authored Jul 30, 2024
    Configuration menu
    Copy the full SHA
    3b75f2c View commit details
    Browse the repository at this point in the history

Commits on Jul 31, 2024

  1. Add more tests and fix typo in kani_core

    @celinval
    celinval committed Jul 31, 2024
    Configuration menu
    Copy the full SHA
    a25f1a4 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'main' into issue-3383-contract-playback

    @celinval
    celinval authored Jul 31, 2024
    Configuration menu
    Copy the full SHA
    b75cf24 View commit details
    Browse the repository at this point in the history

  3. Apply suggestions from code review 

    Co-authored-by: Felipe R. Monteiro <rms.felipe@gmail.com>
    @celinval @feliperodri
    celinval and feliperodri authored Jul 31, 2024
    Configuration menu
    Copy the full SHA
    5fab514 View commit details
    Browse the repository at this point in the history

  4. Address PR comments

    @celinval
    celinval committed Jul 31, 2024
    Configuration menu
    Copy the full SHA
    f4260e0 View commit details
    Browse the repository at this point in the history

  5. Merge branch 'main' into issue-3383-contract-playback

    @celinval
    celinval authored Jul 31, 2024
    Configuration menu
    Copy the full SHA
    224f35d View commit details
    Browse the repository at this point in the history