Commit 90eabd9c authored by Michael Sammler's avatar Michael Sammler
Browse files

add pointer to integer casts for function pointers

parent 5de58fd1
Pipeline #49454 passed with stage
in 16 minutes and 19 seconds
......@@ -376,6 +376,12 @@ Inductive eval_un_op : un_op → op_type → state → val → val → Prop :=
val_of_Z l.2 it p = Some vt
block_alive l σ.(st_heap)
eval_un_op (CastOp (IntOp it)) PtrOp σ vs vt
| CastOpPIFn it σ vs vt l:
val_to_loc vs = Some l
l.1 = ProvFnPtr
val_of_Z l.2 it None = Some vt
is_Some (σ.(st_fntbl) !! l.2)
eval_un_op (CastOp (IntOp it)) PtrOp σ vs vt
| CastOpPINull it σ vs vt:
vs = NULL
val_of_Z 0 it None = Some vt
......@@ -385,7 +391,11 @@ Inductive eval_un_op : un_op → op_type → state → val → val → Prop :=
l = (ProvAlloc (val_to_byte_prov vs), a)
(** This is using that the address 0 is never alive. *)
l' = (if bool_decide (valid_ptr l σ.(st_heap)) then l else
(if bool_decide (a = 0) then NULL_loc else (ProvAlloc None, a)))
(if bool_decide (a = 0) then NULL_loc else
if bool_decide (is_Some (σ.(st_fntbl) !! l.2)) then
(ProvFnPtr, a)
else
(ProvAlloc None, a)))
val_of_loc l' = vt
eval_un_op (CastOp PtrOp) (IntOp it) σ vs vt
| NegOpI it σ vs vt n:
......
......@@ -370,8 +370,10 @@ Proof.
iIntros (Hv) "HΦ".
iApply wp_unop_det. iSplit; [|done].
iIntros (σ ?) "Hctx". iPureIntro. split.
- inversion 1; simplify_eq => //. revert select (block_alive _ _) => -[?[??]].
have ? := val_to_of_loc NULL_loc. unfold NULL in *; by simplify_eq.
- inversion 1; simplify_eq => //.
all: destruct l; simplify_eq/=.
all: have ? := val_to_of_loc NULL_loc.
all: unfold NULL in *; by simplify_eq.
- move => ->. by econstructor.
Qed.
......@@ -386,6 +388,7 @@ Proof.
iIntros "!>" (v' Hv'). iFrame.
inversion Hv'; simplify_eq.
case_bool_decide; [ iApply "HΦ"|].
case_bool_decide; simplify_eq; [ iApply "HΦ"|].
case_bool_decide; simplify_eq; iApply "HΦ".
Qed.
......
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