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

CHERI: invariants proofs finished #577

Merged
merged 12 commits into from
Sep 15, 2024
Merged

CHERI: invariants proofs finished #577

merged 12 commits into from
Sep 15, 2024

Commits on Sep 15, 2024

  1. CHERI: strengthen fetch_bytes_add_neq_o

    @zoickx @vzaliva
    zoickx authored and vzaliva committed Sep 15, 2024
    Configuration menu
    Copy the full SHA
    0c63ad9 View commit details
    Browse the repository at this point in the history

  2. CHERI: add some generic alignment arithmetic facts

    @zoickx @vzaliva
    zoickx authored and vzaliva committed Sep 15, 2024
    Configuration menu
    Copy the full SHA
    d152df4 View commit details
    Browse the repository at this point in the history

  3. CHERI: add bounds check to memcpy_copy_data_PreservesInvariant

    @zoickx @vzaliva
    zoickx authored and vzaliva committed Sep 15, 2024
    Configuration menu
    Copy the full SHA
    0d7bab4 View commit details
    Browse the repository at this point in the history

  4. CHERI: fix subgoals changed by 3876699

    @zoickx @vzaliva
    zoickx authored and vzaliva committed Sep 15, 2024
    Configuration menu
    Copy the full SHA
    78e0c26 View commit details
    Browse the repository at this point in the history

  5. CHERI: prove memcpy_copy_data_PreservesInvariant

    @zoickx @vzaliva
    zoickx authored and vzaliva committed Sep 15, 2024
    Configuration menu
    Copy the full SHA
    ce2b8f9 View commit details
    Browse the repository at this point in the history

  6. Assertion per rems-project#229

    @vzaliva
    vzaliva committed Sep 15, 2024
    Configuration menu
    Copy the full SHA
    5ba9748 View commit details
    Browse the repository at this point in the history

  7. CHERI: unused argument to abst removed

    @vzaliva
    vzaliva committed Sep 15, 2024
    Configuration menu
    Copy the full SHA
    d24a454 View commit details
    Browse the repository at this point in the history

  8. CHERI: tag check in find_cap_allocation

    @vzaliva
    vzaliva committed Sep 15, 2024
    Configuration menu
    Copy the full SHA
    4a4ed09 View commit details
    Browse the repository at this point in the history

  9. adjustements for new interface on coq-cheri-capabilties

    @vzaliva
    vzaliva committed Sep 15, 2024
    Configuration menu
    Copy the full SHA
    f83a79e View commit details
    Browse the repository at this point in the history

  10. attempting to use new coq-cheri-capabilities lemmas

    @vzaliva
    vzaliva committed Sep 15, 2024
    Configuration menu
    Copy the full SHA
    dd572c6 View commit details
    Browse the repository at this point in the history

  11. tied up pointers and cap sizes in imp. QED capability_gs_encode_size

    @vzaliva
    vzaliva committed Sep 15, 2024
    Configuration menu
    Copy the full SHA
    c1417c3 View commit details
    Browse the repository at this point in the history

  12. new UB: CHERI_UB_ZeroLength. flagged in cheri_bounds_set intrinsic

    @vzaliva
    vzaliva committed Sep 15, 2024
    Configuration menu
    Copy the full SHA
    e798415 View commit details
    Browse the repository at this point in the history