Commit 7a47be1b authored by Rodolphe Lepigre's avatar Rodolphe Lepigre
Browse files

Fix inversion of signedness for [uintptr_t] and [intptr_t].

parent 17bf873b
Pipeline #41127 failed with stage
in 19 minutes and 57 seconds
......@@ -285,8 +285,8 @@ Section loc_in_bounds.
iPureIntro. lia.
Qed.
Lemma loc_in_bounds_in_range_size_t l n:
loc_in_bounds l n - l.2 size_t.
Lemma loc_in_bounds_in_range_uintptr_t l n:
loc_in_bounds l n - l.2 uintptr_t.
Proof.
etrans; first by apply loc_in_bounds_ptr_in_range. iPureIntro.
rewrite /min_alloc_start /max_alloc_end /bytes_per_addr /bytes_per_addr_log /=.
......
......@@ -213,11 +213,11 @@ Section IntType.
Definition bytes_per_addr_log : nat := 3%nat.
Definition bytes_per_addr : nat := (2 ^ bytes_per_addr_log)%nat.
Definition intptr_t := IntType bytes_per_addr_log false.
Definition uintptr_t := IntType bytes_per_addr_log true.
Definition intptr_t := IntType bytes_per_addr_log true.
Definition uintptr_t := IntType bytes_per_addr_log false.
Definition size_t := intptr_t.
Definition ssize_t := uintptr_t.
Definition size_t := uintptr_t.
Definition ssize_t := intptr_t.
Definition bool_it := u8.
End IntType.
......
......@@ -198,18 +198,18 @@ Section own.
(* Allow direct casts to other integer types. *)
Lemma type_cast_ptr_int (p : loc) β ty T:
((p ◁ₗ{β} ty - loc_in_bounds p 0 True) (p ◁ₗ{β} ty - T (i2v p.2 size_t) (t2mt (p.2 @ int size_t)))) -
typed_un_op p (p ◁ₗ{β} ty) (CastOp (IntOp size_t)) PtrOp T.
typed_un_op p (p ◁ₗ{β} ty) (CastOp (IntOp uintptr_t)) PtrOp T.
Proof.
iIntros "HT Hp" (Φ) "HΦ".
iAssert (p.2 size_t)%I as %[? Heq]%val_of_int_is_some.
{ iDestruct "HT" as "[HT _]". iDestruct ("HT" with "Hp") as "[Hlib _]".
by iApply loc_in_bounds_in_range_size_t. }
by iApply loc_in_bounds_in_range_uintptr_t. }
iDestruct "HT" as "[_ HT]". rewrite /i2v Heq.
iApply wp_cast_ptr_int => //=; first by rewrite val_to_of_loc.
iApply ("HΦ" with "[] [HT Hp]"); last by iApply "HT". done.
Qed.
Global Instance type_cast_ptr_int_inst (p : loc) β ty:
TypedUnOp p (p ◁ₗ{β} ty)%I (CastOp (IntOp size_t)) PtrOp :=
TypedUnOp p (p ◁ₗ{β} ty)%I (CastOp (IntOp uintptr_t)) PtrOp :=
λ T, i2p (type_cast_ptr_int p β ty T).
Lemma type_cast_int_ptr n v it T:
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment