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
8e901d81
Commit
8e901d81
authored
May 31, 2021
by
Michael Sammler
Browse files
update talk demo
parent
5c50af1e
Pipeline
#47900
passed with stage
in 31 minutes and 1 second
Changes
4
Pipelines
3
Hide whitespace changes
Inline
Side-by-side
examples/proofs/talk_demo3/generated_proof_append.v
View file @
8e901d81
...
...
@@ -13,7 +13,7 @@ Section proof_append.
typed_function
(
impl_append
global_append
)
type_of_append
.
Proof
.
Open
Scope
printing_sugar
.
start_function
"append"
(
[[
p
xs
]
ys
]
)
=>
arg_l
arg_k
.
start_function
"append"
(
p
)
=>
arg_l
arg_k
.
split_blocks
((
∅
)%
I
:
gmap
label
(
iProp
Σ
))
((
...
...
examples/proofs/talk_demo3/generated_proof_test.v
View file @
8e901d81
From
refinedc
.
typing
Require
Import
typing
.
From
refinedc
.
examples
.
talk_demo3
Require
Import
generated_code
.
From
refinedc
.
examples
.
talk_demo3
Require
Import
generated_spec
.
Set
Default
Proof
Using
"Type"
.
(* Generated from [examples/talk_demo3.c]. *)
Section
proof_test
.
Context
`
{!
typeG
Σ
}
`
{!
globalG
Σ
}.
(* Typing proof for [test]. *)
Lemma
type_test
(
global_alloc
global_append
:
loc
)
:
global_alloc
◁ᵥ
global_alloc
@
function_ptr
type_of_alloc
-
∗
global_append
◁ᵥ
global_append
@
function_ptr
type_of_append
-
∗
typed_function
(
impl_test
global_alloc
global_append
)
type_of_test
.
Proof
.
Open
Scope
printing_sugar
.
start_function
"test"
([])
=>
local_node1
local_node2
.
split_blocks
((
∅
)%
I
:
gmap
label
(
iProp
Σ
))
((
∅
)%
I
:
gmap
label
(
iProp
Σ
)).
-
repeat
liRStep
;
liShow
.
all
:
print_typesystem_goal
"test"
"#0"
.
Unshelve
.
all
:
sidecond_hook
;
prepare_sideconditions
;
normalize_and_simpl_goal
;
try
solve_goal
;
unsolved_sidecond_hook
.
all
:
print_sidecondition_goal
"test"
.
Qed
.
End
proof_test
.
(* You were too lazy to even write a spec for this function. *)
examples/proofs/talk_demo3/generated_spec.v
View file @
8e901d81
...
...
@@ -93,12 +93,10 @@ Section spec.
(* Specifications for function [append]. *)
Definition
type_of_append
:
=
fn
(
∀
(
p
,
xs
,
ys
)
:
loc
*
(
list
Z
)
*
(
list
Z
)
;
(
p
@
(&
own
(
xs
@
(
list_t
)))
)
,
(
ys
@
(
list_t
)
)
;
True
)
→
∃
()
:
(),
(
void
)
;
(
p
◁ₗ
((
xs
++
ys
)
@
(
list_t
))
)
.
fn
(
∀
p
:
loc
;
(
p
@
(&
own
(
list_t
))),
(
list_t
)
;
True
)
→
∃
()
:
(),
(
void
)
;
(
p
◁ₗ
(
list_t
)).
(* Specifications for function [test]. *)
Definition
type_of_test
:
=
fn
(
∀
()
:
()
;
(
alloc_initialized
))
→
∃
()
:
(),
(
void
)
;
True
.
(* Function [test] has been skipped. *)
End
spec
.
Typeclasses
Opaque
list_t_rec
.
examples/talk_demo3.c
View file @
8e901d81
...
...
@@ -14,9 +14,9 @@ list_node {
}
*
list_t
;
[[
rc
::
parameters
(
"p : loc"
,
"xs : {list Z}"
,
"ys : {list Z}"
)]]
[[
rc
::
args
(
"p @ &own<
xs @
list_t>"
,
"
ys @
list_t"
)]]
[[
rc
::
ensures
(
"own p :
{xs ++ ys} @
list_t"
)]]
[[
rc
::
parameters
(
"p : loc"
)]]
[[
rc
::
args
(
"p @ &own<list_t>"
,
"list_t"
)]]
[[
rc
::
ensures
(
"own p : list_t"
)]]
void
append
(
list_t
*
l
,
list_t
k
)
{
if
(
*
l
==
NULL
)
{
*
l
=
k
;
...
...
@@ -25,7 +25,7 @@ void append(list_t *l, list_t k) {
}
}
[[
rc
::
requires
(
"[alloc_initialized]"
)]]
/*
[[rc::requires("[alloc_initialized]")]]
*/
void
test
()
{
struct
list_node
*
node1
=
alloc
(
sizeof
(
struct
list_node
));
node1
->
val
=
1
;
node1
->
next
=
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