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

Add YAML witness validation by invariant checking #745

Merged
merged 26 commits into from
May 31, 2022
Merged

Add YAML witness validation by invariant checking #745

merged 26 commits into from
May 31, 2022

Commits on May 24, 2022

  1. Add yaml witness parsing prototype

    @sim642
    sim642 committed May 24, 2022
    Configuration menu
    Copy the full SHA
    cd1af7a View commit details
    Browse the repository at this point in the history

  2. Add yaml witness assert evaluation

    @sim642
    sim642 committed May 24, 2022
    Configuration menu
    Copy the full SHA
    7a85a96 View commit details
    Browse the repository at this point in the history

  3. Split conjunctions in yaml witness output to work around misparsing 

    goblint/cil#94.
    @sim642
    sim642 committed May 24, 2022
    Configuration menu
    Copy the full SHA
    d0d7558 View commit details
    Browse the repository at this point in the history

  4. Fix yaml witness validate not handling formals

    @sim642
    sim642 committed May 24, 2022
    Configuration menu
    Copy the full SHA
    f15bd32 View commit details
    Browse the repository at this point in the history

  5. Merge branch 'yaml-witness' into yaml-witness-validate

    @sim642
    sim642 committed May 24, 2022
    Configuration menu
    Copy the full SHA
    f2acf16 View commit details
    Browse the repository at this point in the history

  6. Use messages for yaml witness validation output

    @sim642
    sim642 committed May 24, 2022
    Configuration menu
    Copy the full SHA
    b6b8449 View commit details
    Browse the repository at this point in the history

  7. Validate yaml witnesses context sensitively

    @sim642
    sim642 committed May 24, 2022
    Configuration menu
    Copy the full SHA
    a3d3264 View commit details
    Browse the repository at this point in the history

Commits on May 25, 2022

  1. Check parsed yaml witness invariants to avoid downstream crashing

    @sim642
    sim642 committed May 25, 2022
    Configuration menu
    Copy the full SHA
    a92600d View commit details
    Browse the repository at this point in the history

  2. Clean up YamlWitness.Validator

    @sim642
    sim642 committed May 25, 2022
    Configuration menu
    Copy the full SHA
    7d3cd2f View commit details
    Browse the repository at this point in the history

  3. Locate yaml witness invariants efficiently and inexactly

    @sim642
    sim642 committed May 25, 2022
    Configuration menu
    Copy the full SHA
    14c5129 View commit details
    Browse the repository at this point in the history

  4. Hide mutex structure contents in base analysis

    @sim642
    sim642 committed May 25, 2022
    Configuration menu
    Copy the full SHA
    3841fe7 View commit details
    Browse the repository at this point in the history

  5. Insert explicit casts in IntDomain invariants

    @sim642
    sim642 committed May 25, 2022
    Configuration menu
    Copy the full SHA
    db1ce04 View commit details
    Browse the repository at this point in the history

  6. Use long long zero in apron invariants to match lhs

    @sim642
    sim642 committed May 25, 2022
    Configuration menu
    Copy the full SHA
    53495c1 View commit details
    Browse the repository at this point in the history

  7. Use bot instead of top for base mutex contents 

    This avoids unknown value escape warnings.
    @sim642
    sim642 committed May 25, 2022
    Configuration menu
    Copy the full SHA
    1fa8d17 View commit details
    Browse the repository at this point in the history

Commits on May 26, 2022

  1. Use Frontc to parse yaml witness invariants

    @sim642
    sim642 committed May 26, 2022
    Configuration menu
    Copy the full SHA
    4c8d769 View commit details
    Browse the repository at this point in the history

  2. Fix Cabs2cil mangling fundec locals during yaml witness invariant par… 

    …sing
    @sim642
    sim642 committed May 26, 2022
    Configuration menu
    Copy the full SHA
    4e5e10c View commit details
    Browse the repository at this point in the history

  3. Use logical operators in yaml witness invariant parsing

    @sim642
    sim642 committed May 26, 2022
    Configuration menu
    Copy the full SHA
    b42da55 View commit details
    Browse the repository at this point in the history

  4. Add Question exp handling 

    These may occur in yaml witness invariants.
    @sim642
    sim642 committed May 26, 2022
    Configuration menu
    Copy the full SHA
    4e99727 View commit details
    Browse the repository at this point in the history

  5. Expand and fix exp pattern matching

    @sim642
    sim642 committed May 26, 2022
    Configuration menu
    Copy the full SHA
    f8f3984 View commit details
    Browse the repository at this point in the history

  6. Add yaml witness certification

    @sim642
    sim642 committed May 26, 2022
    Configuration menu
    Copy the full SHA
    7407e48 View commit details
    Browse the repository at this point in the history

  7. Deduplicate yaml witness entry creation

    @sim642
    sim642 committed May 26, 2022
    Configuration menu
    Copy the full SHA
    eb371f5 View commit details
    Browse the repository at this point in the history

  8. Aggregate yaml witness invariant results over lvars

    @sim642
    sim642 committed May 26, 2022
    Configuration menu
    Copy the full SHA
    f2ff5f9 View commit details
    Browse the repository at this point in the history

Commits on May 27, 2022

  1. Merge branch 'master' into yaml-witness-validate

    @sim642
    sim642 committed May 27, 2022
    Configuration menu
    Copy the full SHA
    79d2abe View commit details
    Browse the repository at this point in the history

  2. Revert "Use bot instead of top for base mutex contents" 

    This reverts commit 1fa8d17.
    @sim642
    sim642 committed May 27, 2022
    Configuration menu
    Copy the full SHA
    a4937cf View commit details
    Browse the repository at this point in the history

  3. Revert "Hide mutex structure contents in base analysis" 

    This reverts commit 3841fe7.
    @sim642
    sim642 committed May 27, 2022
    Configuration menu
    Copy the full SHA
    4bc3f35 View commit details
    Browse the repository at this point in the history

Commits on May 30, 2022

  1. Update CIL opam pin

    @sim642
    sim642 committed May 30, 2022
    Configuration menu
    Copy the full SHA
    8b2cccf View commit details
    Browse the repository at this point in the history