Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Iris
RefinedC
Commits
7ef2bb97
Commit
7ef2bb97
authored
Mar 09, 2021
by
Michael Sammler
Browse files
remove rc_unfold in queue
parent
299fbb93
Pipeline
#43149
failed with stage
in 15 minutes and 24 seconds
Changes
3
Pipelines
1
Expand all
Hide whitespace changes
Inline
Side-by-side
examples/proofs/queue/generated_code.v
View file @
7ef2bb97
This diff is collapsed.
Click to expand it.
examples/proofs/queue/generated_spec.v
View file @
7ef2bb97
...
...
@@ -65,13 +65,12 @@ Section spec.
(* Definition of type [queue]. *)
Definition
queue_rec
:
((
list
type
)
-
d
>
typeO
)
→
((
list
type
)
-
d
>
typeO
)
:
=
(
λ
self
tys
,
(&
own
(
tyexists
(
λ
p
:
loc
,
(
tyexists
(
λ
p
,
own_constrained
(
tyown_constraint
(
p
)
(
null
))
(&
own
(
struct
struct_queue
[@{
type
}
(
tyfold
((
λ
ty
x
,
ty
@
queue_elem
x
)
<$>
tys
)
(
place
(
p
)))
;
(
p
@
(&
own
(
null
)))
]
)
))
(&
own
(
place
(
p
)))
]
))
))
)%
I
.
Typeclasses
Opaque
queue_rec
.
...
...
@@ -85,13 +84,12 @@ Section spec.
Lemma
queue_unfold
(
tys
:
(
list
type
))
:
(
tys
@
queue
)%
I
≡
@{
type
}
(
(&
own
(
tyexists
(
λ
p
:
loc
,
(
tyexists
(
λ
p
,
own_constrained
(
tyown_constraint
(
p
)
(
null
))
(&
own
(
struct
struct_queue
[@{
type
}
(
tyfold
((
λ
ty
x
,
ty
@
queue_elem
x
)
<$>
tys
)
(
place
(
p
)))
;
(
p
@
(&
own
(
null
)))
]
)
))
(&
own
(
place
(
p
)))
]
))
))
)%
I
.
Proof
.
by
rewrite
{
1
}/
with_refinement
/=
fixp_unfold
.
Qed
.
...
...
examples/queue.c
View file @
7ef2bb97
...
...
@@ -13,12 +13,11 @@ queue_elem {
}
*
queue_elem_t
;
typedef
struct
[[
rc
::
refined_by
(
"tys: {list type}"
)]]
[[
rc
::
ptr_type
(
"queue : &own<...>"
)]]
[[
rc
::
exists
(
"p : loc"
)]]
[[
rc
::
ptr_type
(
"queue : ∃ p. own_constrained<tyown_constraint<p, null>, &own<...>>"
)]]
queue
{
[[
rc
::
field
(
"tyfold<{(λ ty x, ty @ queue_elem x) <$> tys}, place<p>>"
)]]
queue_elem_t
head
;
[[
rc
::
field
(
"
p @
&own<
null
>"
)]]
[[
rc
::
field
(
"&own<
place<p>
>"
)]]
queue_elem_t
*
tail
;
}
*
queue_t
;
...
...
@@ -36,7 +35,6 @@ queue_t init_queue() {
[[
rc
::
returns
(
"{bool_decide (tys ≠ [])} @ boolean<bool_it>"
)]]
[[
rc
::
ensures
(
"own p : {tys} @ queue"
)]]
bool
is_empty
(
queue_t
*
q
)
{
rc_unfold
(
*
(
*
q
)
->
tail
);
return
(
*
q
)
->
head
!=
NULL
;
}
...
...
@@ -58,7 +56,6 @@ void enqueue(queue_t *q, void *v) {
[[
rc
::
returns
(
"{maybe2 cons tys} @ optionalO<λ (ty, _). &own<ty>>"
)]]
[[
rc
::
ensures
(
"own p : {tail tys} @ queue"
)]]
void
*
dequeue
(
queue_t
*
q
)
{
rc_unfold
(
*
(
*
q
)
->
tail
);
if
((
*
q
)
->
head
==
NULL
)
{
return
NULL
;
}
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment