Commit e7805765 authored by Ralf Jung's avatar Ralf Jung

more comments on retag Default vs FnEntry

parent 31da8ade
......@@ -13,7 +13,8 @@ Definition ex1_down_unopt : function :=
let: "x" := new_place (&mut int) "i" in
(* retag_place reborrows the pointer value stored in "x" (which is "i"),
then updates "x" with the new pointer value *)
then updates "x" with the new pointer value. This relies on protectors,
hence [FnEntry]. *)
retag_place "x" (RefPtr Mutable) int FnEntry ;;
(* Read the value "v" from the cell pointed to by the pointer in "x" *)
......
......@@ -12,7 +12,8 @@ Definition ex2_unopt : function :=
let: "x" := new_place (& int) "i" in
(* retag_place reborrows the pointer value stored in "x" (which is "i"),
then updates "x" with the new pointer value *)
then updates "x" with the new pointer value. A [Default] retag is
sufficient for this, we don't need the protector. *)
retag_place "x" (RefPtr Immutable) int Default ;;
(* The unknown code is represented by a call to an unknown function "f",
......
......@@ -13,7 +13,8 @@ Definition ex2_down_unopt : function :=
let: "x" := new_place (& int) "i" in
(* retag_place reborrows the pointer value stored in "x" (which is "i"),
then updates "x" with the new pointer value *)
then updates "x" with the new pointer value. This relies on protectors,
hence [FnEntry]. *)
retag_place "x" (RefPtr Immutable) int FnEntry ;;
(* Read the value "v" from the cell pointed to by the pointer in "x" *)
......
......@@ -13,7 +13,8 @@ Definition ex3_unopt : function :=
let: "x" := new_place (&mut int) "i" in
(* retag_place reborrows the pointer value stored in "x" (which is "i"),
then updates "x" with the new pointer value *)
then updates "x" with the new pointer value. This relies on protectors,
hence [FnEntry]. *)
retag_place "x" (RefPtr Mutable) int FnEntry ;;
(* Write 42 to the cell pointed to by the pointer in "x" *)
......
......@@ -13,7 +13,8 @@ Definition ex3_down_unopt : function :=
let: "x" := new_place (&mut int) "i" in
(* retag_place reborrows the pointer value stored in "x" (which is "i"),
then updates "x" with the new pointer value *)
then updates "x" with the new pointer value. This relies on protectors,
hence [FnEntry]. *)
retag_place "x" (RefPtr Mutable) int FnEntry ;;
(* Write 42 to the cell pointed to by the pointer in "x" *)
......
Markdown is supported
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