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

Fix codegen_atomic_binop for atomic_ptr #3047

Merged
merged 5 commits into from
Feb 29, 2024

Commits on Feb 28, 2024

  1. Fix codegen_atomic_binop for atomic_ptr

    Fetch functions of atomic_ptr calls atomic intrinsics functions with pointer-type arguments (invalid_mut), which will cause typecheck failures.
    The change in this commit add support of pointer-type arguments into codegen_atomic_binop to fix the issue.
    The new codegen_atomic_binop will cast pointer arguments to size_t, apply op on them, and then cast the op result back to the pointer type.
    
    Fix the issue model-checking#3042.
    qinheping committed Feb 28, 2024
    Configuration menu
    Copy the full SHA
    7fa9cce View commit details
    Browse the repository at this point in the history
  2. Configuration menu
    Copy the full SHA
    33cab5f View commit details
    Browse the repository at this point in the history

Commits on Feb 29, 2024

  1. Configuration menu
    Copy the full SHA
    fc1e55b View commit details
    Browse the repository at this point in the history
  2. Configuration menu
    Copy the full SHA
    3cbb542 View commit details
    Browse the repository at this point in the history
  3. Update tests/kani/Intrinsics/Atomic/Stable/AtomicPtr/main.rs

    Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>
    adpaco-aws and zhassan-aws authored Feb 29, 2024
    Configuration menu
    Copy the full SHA
    650f422 View commit details
    Browse the repository at this point in the history