Commit 064c6d90 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Mark size arguments as ghost for open and close functions.

parent b8193421
......@@ -19,7 +19,7 @@ module Alias
/\ min p1 = min p2 /\ max p1 = max p2 /\ zone p1 = zone p2
val open_sep (r x:ptr limb) (sx:int32) (y:ptr limb) (sy:int32) :
val open_sep (r x:ptr limb) (ghost sx:int32) (y:ptr limb) (ghost sy:int32) :
(nr:ptr limb, nx:ptr limb, ny:ptr limb, ghost m:mem)
requires { valid r sx /\ valid x sx /\ valid y sy }
requires { writable r }
......@@ -47,7 +47,7 @@ module Alias
alias { nr.data with ny.data }
alias { nx.data with ny.data }
val close_sep (r x:ptr limb) (sx:int32) (y:ptr limb) (sy:int32)
val close_sep (r x:ptr limb) (ghost sx:int32) (y:ptr limb) (ghost sy:int32)
(nr nx ny:ptr limb) (ghost m:mem) : unit
alias { nr.data with nx.data }
alias { nr.data with ny.data }
......@@ -78,7 +78,7 @@ module Alias
writes { nr, nx, ny, nr.data, nx.data, ny.data,
r.data, r.max, x.data, x.max, y.data, y.max, m.ok }
val open_rx (x:ptr limb) (sx:int32) (y:ptr limb) (sy:int32) :
val open_rx (x:ptr limb) (ghost sx:int32) (y:ptr limb) (ghost sy:int32) :
(nr:ptr limb, nx:ptr limb, ny:ptr limb, ghost m:mem)
requires { valid x sx /\ valid y sy }
requires { 0 <= sy <= sx }
......@@ -104,7 +104,7 @@ module Alias
alias { nr.data with ny.data }
alias { nx.data with ny.data }
val close_rx (x:ptr limb) (sx:int32) (y:ptr limb) (sy:int32)
val close_rx (x:ptr limb) (ghost sx:int32) (y:ptr limb) (ghost sy:int32)
(nr nx ny:ptr limb) (ghost m:mem) : unit
alias { nr.data with nx.data }
alias { nr.data with ny.data }
......@@ -131,7 +131,7 @@ module Alias
writes { nr, nx, ny, nr.data, nx.data, ny.data,
x.data, x.max, y.data, y.max, m.ok }
val open_shift_sep (r x:ptr limb) (sz:int32) :
val open_shift_sep (r x:ptr limb) (ghost sz:int32) :
(nr:ptr limb, nx:ptr limb, ghost m:mem)
requires { valid r sz /\ valid x sz }
requires { 0 <= sz }
......@@ -153,7 +153,7 @@ module Alias
writes { r, x }
alias { nr.data with nx.data }
val close_shift_sep (r x:ptr limb) (sz:int32) (nr nx:ptr limb) (ghost m:mem)
val close_shift_sep (r x:ptr limb) (ghost sz:int32) (nr nx:ptr limb) (ghost m:mem)
: unit
alias { nr.data with nx.data }
requires { writable r /\ writable nr }
......
......@@ -84,7 +84,7 @@ module ptralias.Alias
\n};\
\n\
\nstatic inline struct __open_sep_result\
\nopen_sep (uint64_t *r, uint64_t *x, int32_t sx, uint64_t *y, int32_t sy)\
\nopen_sep (uint64_t *r, uint64_t *x, uint64_t *y)\
\n{\
\n struct __open_sep_result result;\
\n result.__field_0 = r;\
......@@ -94,7 +94,7 @@ module ptralias.Alias
\n}\
\n\
\nstatic inline struct __open_rx_result\
\nopen_rx (uint64_t *x, int32_t sx, uint64_t *y, int32_t sy)\
\nopen_rx (uint64_t *x, uint64_t *y)\
\n{\
\n struct __open_rx_result result;\
\n result.__field_0 = x;\
......@@ -104,7 +104,7 @@ module ptralias.Alias
\n}\
\n\
\nstatic inline struct __open_shift_sep_result\
\nopen_shift_sep (uint64_t *r, uint64_t *x, int32_t sz)\
\nopen_shift_sep (uint64_t *r, uint64_t *x)\
\n{\
\n struct __open_shift_sep_result result;\
\n result.__field_0 = r;\
......@@ -116,9 +116,9 @@ module ptralias.Alias
syntax val open_sep "open_sep"
syntax val open_rx "open_rx"
syntax val open_shift_sep "open_shift_sep"
syntax val close_sep "IGNORE3(%1,%2,%4)" prec 1 15 15 15
syntax val close_rx "IGNORE3(%1,%2,%4)" prec 1 15 15 15
syntax val close_shift_sep "IGNORE2(%1,%2)" prec 1 15 15
syntax val close_sep "IGNORE3(%1, %2, %3)" prec 1 15 15 15
syntax val close_rx "IGNORE2(%1, %2)" prec 1 15 15
syntax val close_shift_sep "IGNORE2(%1, %2)" prec 1 15 15
end
......
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