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.

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

Use llvm_points_to_bitfield in SAW proofs #3155

Merged
merged 5 commits into from
Jan 29, 2022

Commits on Jan 27, 2022

  1. Use llvm_points_to_bitfield in SAW proofs

    This uses SAW's new `llvm_points_to_bitfield` command (introduced in
    GaloisInc/saw-script#1539) to simplify specifications that involve the
    bitfields in `s2n_config` and `s2n_connection`. In particular, there is no
    longer any need to manually compute the size of the bitfields or the indices of
    the fields within the bitfields, as these details are handled automatically
    by `llvm_points_to_bitfield`. The positions of the fields within bitfields are
    also no longer important.
    
    This addresses a review comment in
    aws#3079 (comment).
    RyanGlScott committed Jan 27, 2022
    Configuration menu
    Copy the full SHA
    1270e70 View commit details
    Browse the repository at this point in the history
  2. Remove obsolete comments about bitfield flag ordering

    These comments are no longer relevant now that the SAW proofs use the
    `llvm_bitfield_points_to` command, which is insensitive to the order of fields
    within a bitfield.
    RyanGlScott committed Jan 27, 2022
    Configuration menu
    Copy the full SHA
    6a10dbc View commit details
    Browse the repository at this point in the history
  3. Configuration menu
    Copy the full SHA
    bbc1356 View commit details
    Browse the repository at this point in the history
  4. Configuration menu
    Copy the full SHA
    63572d5 View commit details
    Browse the repository at this point in the history

Commits on Jan 28, 2022

  1. Configuration menu
    Copy the full SHA
    26402ee View commit details
    Browse the repository at this point in the history