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

Run VeriFast proofs in CI #845

Open
wants to merge 10 commits into
base: main
Choose a base branch
from
Open

Run VeriFast proofs in CI #845

wants to merge 10 commits into from

Commits on Sep 7, 2022

  1. Undo syntax changes preventing VeriFast parsing

    @nchong-at-aws @karkhaz
    nchong-at-aws authored and karkhaz committed Sep 7, 2022
    Configuration menu
    Copy the full SHA
    e512b80 View commit details
    Browse the repository at this point in the history

  2. Update proofs inline with source changes 

    Outstanding:
  - xQueueGenericReset return code
  - Not using prvIncrementQueueTxLock or prvIncrementQueueRxLock macros
    @nchong-at-aws @karkhaz
    nchong-at-aws authored and karkhaz committed Sep 7, 2022
    Configuration menu
    Copy the full SHA
    4bd03ca View commit details
    Browse the repository at this point in the history

  3. Remove git hash check

    @nchong-at-aws @karkhaz
    nchong-at-aws authored and karkhaz committed Sep 7, 2022
    Configuration menu
    Copy the full SHA
    34e4370 View commit details
    Browse the repository at this point in the history

  4. Document new changes between proven code and implementation

    @nchong-at-aws @karkhaz
    nchong-at-aws authored and karkhaz committed Sep 7, 2022
    Configuration menu
    Copy the full SHA
    49322a1 View commit details
    Browse the repository at this point in the history

  5. Update copyright header

    @nchong-at-aws @karkhaz
    nchong-at-aws authored and karkhaz committed Sep 7, 2022
    Configuration menu
    Copy the full SHA
    b9011d5 View commit details
    Browse the repository at this point in the history

  6. VeriFast proofs: turn off uncrustify checks 

    Uncrustify requires formatting of comments that is at odds with VeriFast's
proof annotations, which are contained within comments.
    @nchong-at-aws @karkhaz
    nchong-at-aws authored and karkhaz committed Sep 7, 2022
    Configuration menu
    Copy the full SHA
    d6f2225 View commit details
    Browse the repository at this point in the history

  7. Ignore proof output files

    @karkhaz
    karkhaz committed Sep 7, 2022
    Configuration menu
    Copy the full SHA
    3648075 View commit details
    Browse the repository at this point in the history

  8. Run VeriFast proofs together with CBMC proofs 

    This commit changes the run-cbmc-proofs.py script so that it also adds
Litani jobs for each of the VeriFast proofs. The result of the VeriFast
proofs is presented on the Litani dashboard alongside the existing CBMC
proofs.
    @karkhaz
    karkhaz committed Sep 7, 2022
    Configuration menu
    Copy the full SHA
    851d02b View commit details
    Browse the repository at this point in the history

  9. Add documentation and flag for VeriFast regression 

    This commit removes the old Makefile for running VeriFast, and updates
the documentation for how to run all proofs in parallel. It also adds an
option to the run script to allow running only the VeriFast proofs.
    @karkhaz
    karkhaz committed Sep 7, 2022
    Configuration menu
    Copy the full SHA
    45e0660 View commit details
    Browse the repository at this point in the history

Commits on Sep 9, 2022

  1. Fix spell check and formatting check

    @AniruddhaKanhere
    AniruddhaKanhere committed Sep 9, 2022
    Configuration menu
    Copy the full SHA
    03f6357 View commit details
    Browse the repository at this point in the history