Commit d10403a3 authored by Michael Sammler's avatar Michael Sammler
Browse files

update iris

parent 476fe0a6
Pipeline #45667 passed with stage
in 30 minutes and 12 seconds
......@@ -20,7 +20,7 @@ typedef struct
"{s ≠ ∅} @ optional<&own<...>, null>")]]
[[rc::exists ("n: nat", "tail: {gmultiset nat}")]]
[[rc::size ("n")]]
[[rc::constraints("{s = {[n]} ⊎ tail}",
[[rc::constraints("{s = {[+n+]} ⊎ tail}",
"{∀ k, k ∈ tail → n ≤ k}")]]
chunk {
[[rc::field("n @ int<size_t>")]] size_t size;
......@@ -31,15 +31,15 @@ chunk {
[[rc::args ("p @ &own<s @ chunks_t>", "&own<uninit<n>>",
"n @ int<size_t>")]]
[[rc::requires ("{sizeof(struct_chunk) ≤ n}")]]
[[rc::ensures ("own p : {{[n]} ⊎ s} @ chunks_t")]]
[[rc::ensures ("own p : {{[+n+]} ⊎ s} @ chunks_t")]]
[[rc::tactics ("all: multiset_solver.")]]
void free(chunks_t* list, void* data, size_t sz) {
chunks_t* cur = list;
[[rc::exists ("cp: loc", "cs: {gmultiset nat}")]]
[[rc::inv_vars("cur: cp @ &own<cs @ chunks_t>")]]
[[rc::inv_vars("list:"
"p @ &own<wand<{cp ◁ₗ ({[n]} ⊎ cs) @ chunks_t},"
"{{[n]} ⊎ s} @ chunks_t>>")]]
"p @ &own<wand<{cp ◁ₗ ({[+n+]} ⊎ cs) @ chunks_t},"
"{{[+n+]} ⊎ s} @ chunks_t>>")]]
while(*cur != NULL) {
if(sz <= (*cur)->size) break;
cur = &(*cur)->next;
......
......@@ -23,7 +23,7 @@ Section proof_free.
arg_sz ◁ₗ (n @ (int (size_t)))
local_entry ◁ₗ uninit void*
local_cur ◁ₗ (cp @ (&own (cs @ (chunks_t))))
arg_list ◁ₗ (p @ (&own (wand (cp ◁ₗ ({[n]} cs) @ chunks_t) (({[n]} s) @ (chunks_t)))))
arg_list ◁ₗ (p @ (&own (wand (cp ◁ₗ ({[+n+]} cs) @ chunks_t) (({[+n+]} s) @ (chunks_t)))))
]> $
)%I : gmap label (iProp Σ)) ((
......
......@@ -24,7 +24,7 @@ Section spec.
(n @ (int (size_t))) ;
(guarded ("chunks_t_0") (apply_dfun self (tail)))
]) struct_chunk n) (
s = {[n]} tail
s = {[+n+]} tail
k, k tail n k
)))
)) (null)))
......@@ -48,7 +48,7 @@ Section spec.
(n @ (int (size_t))) ;
(guarded "chunks_t_0" (tail @ chunks_t))
]) struct_chunk n) (
s = {[n]} tail
s = {[+n+]} tail
k, k tail n k
)))
)) (null)))
......@@ -100,7 +100,7 @@ Section spec.
(* Specifications for function [free]. *)
Definition type_of_free :=
fn( (s, p, n) : (gmultiset nat) * loc * nat; (p @ (&own (s @ (chunks_t)))), (&own (uninit (n))), (n @ (int (size_t))); sizeof(struct_chunk) n)
() : (), (void); (p ◁ₗ (({[n]} s) @ (chunks_t))).
() : (), (void); (p ◁ₗ (({[+n+]} s) @ (chunks_t))).
End spec.
Typeclasses Opaque chunks_t_rec.
......@@ -17,7 +17,7 @@ dev-repo: "git+https://gitlab.mpi-sws.org/iris/refinedc.git"
depends: [
"coq" { (>= "8.12.0" & < "8.13~") }
"coq-iris" { (= "dev.2021-04-14.1.f4fbb6c0") | (= "dev") }
"coq-iris" { (= "dev.2021-04-22.0.dea10729") | (= "dev") }
"dune" {>= "2.7.0"}
"cerberus" {= "~dev"}
"cmdliner" {>= "1.0.4"}
......
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