Skip to content

layout.might_permit_raw_init supports additional checks #1273

Closed
Closed
layout.might_permit_raw_init supports additional checks#1273
Assignees
adpaco

Description

@tedinski
tedinski
opened on Jun 10, 2022

Rust's layout.might_permit_raw_init went from taking true/false flag to taking:

  1. InitKind::Zero, * which corresponds to the old true (and the intrinsic assert_zero_valid)
  2. InitKind::Uninit, false which corresponds to the old false (and the instrinsic assert_uninit_valid)
  3. InitKind::Uninit, false which adds an additional strict check. Unclear if we want it for something.

Upstream PR: rust-lang/rust#97323

Activity

  1. tedinski
    assigned
    adpaco
    on Jun 10, 2022
  2. adpaco
    added this to Kani v0.6on Jun 28, 2022
  3. adpaco
    added this to Kani v0.7on Jul 12, 2022
  4. adpaco
    added this to Kani v0.8on Jul 26, 2022

  5. adpaco commented on Aug 2, 2022

    @adpaco
    adpaco
    on Aug 2, 2022
    Contributor

    In the most recent update, Rust provides two methods permits_zero_init and permits_uninit_init for the type context (where layout is the argument) instead of the method might_permit_raw_init for layouts.

    The updates to the intrinsics code in #1399 make use of them (as in the ssa and cranelift backends), so there's nothing else to do here.

  6. adpaco
    closed this as completedon Aug 2, 2022
  7. adpaco
    moved this to Done in Kani v0.8on Aug 2, 2022
  8. adpaco
    moved this to Done in Kani v0.7on Aug 2, 2022
  9. adpaco
    moved this to Done in Kani v0.6on Aug 2, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

Labels

No labels
No labels

Type

No type

Projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions