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

Witness invariants for arrays and principled handling of unknown indices #1045

Merged
merged 13 commits into from
May 18, 2023
Merged

Witness invariants for arrays and principled handling of unknown indices #1045

merged 13 commits into from
May 18, 2023

Commits on May 11, 2023

  1. Add invariant function to array domains

    @sim642
    sim642 committed May 11, 2023
    Configuration menu
    Copy the full SHA
    681e883 View commit details
    Browse the repository at this point in the history

  2. Add witness invariant to trivial array domain

    @sim642
    sim642 committed May 11, 2023
    Configuration menu
    Copy the full SHA
    edeb2cf View commit details
    Browse the repository at this point in the history

  3. Add witness invariant to unrolled array domain

    @sim642
    sim642 committed May 11, 2023
    Configuration menu
    Copy the full SHA
    0d1b161 View commit details
    Browse the repository at this point in the history

  4. Add witness invariant to partitioned array domain

    @sim642
    sim642 committed May 11, 2023
    Configuration menu
    Copy the full SHA
    d08a86f View commit details
    Browse the repository at this point in the history

  5. Add array unassume test

    @sim642
    sim642 committed May 11, 2023
    Configuration menu
    Copy the full SHA
    f41529f View commit details
    Browse the repository at this point in the history

  6. Add strong_all_array_index_exp

    @sim642
    sim642 committed May 11, 2023
    Configuration menu
    Copy the full SHA
    1d5be76 View commit details
    Browse the repository at this point in the history

  7. Pass lval_raw to base invariant

    @sim642
    sim642 committed May 11, 2023
    Configuration menu
    Copy the full SHA
    94ce23f View commit details
    Browse the repository at this point in the history

  8. Handle strong_all_array_index_exp in trivial array domain

    @sim642
    sim642 committed May 11, 2023
    Configuration menu
    Copy the full SHA
    1413f12 View commit details
    Browse the repository at this point in the history

  9. Handle strong_all_array_index_exp in unroll and partitioned array domain 

    Doesn't actually work for some reason
    @sim642
    sim642 committed May 11, 2023
    Configuration menu
    Copy the full SHA
    c72b96f View commit details
    Browse the repository at this point in the history

Commits on May 12, 2023

  1. Move special array index expressions to ArrayDomain

    @sim642
    sim642 committed May 12, 2023
    Configuration menu
    Copy the full SHA
    334f235 View commit details
    Browse the repository at this point in the history

  2. Add option witness.invariant.goblint

    @sim642
    sim642 committed May 12, 2023
    Configuration menu
    Copy the full SHA
    f3ae350 View commit details
    Browse the repository at this point in the history

  3. Replace unknown_exp and "unknown" indices also with any_index_exp

    @sim642
    sim642 committed May 12, 2023
    Configuration menu
    Copy the full SHA
    2f93630 View commit details
    Browse the repository at this point in the history

Commits on May 18, 2023

  1. Add TODOs for non-working array invariant unassumes

    @sim642
    sim642 committed May 18, 2023
    Configuration menu
    Copy the full SHA
    8bb9e09 View commit details
    Browse the repository at this point in the history