Merge Requests · Iris

add better lemmas for working with mask-changing fupd, and rearrange names a bit

iris!637 · opened Feb 13, 2021 by Ralf Jung Iris 3.4
- MERGED
- 15
updated Mar 03, 2021
Progress on the verification of [early_alloc.c].

refinedc!35 · opened Feb 12, 2021 by Rodolphe Lepigre
- MERGED
- 0
updated Feb 12, 2021
Check generated files on CI

refinedc!34 · opened Feb 12, 2021 by Michael Sammler
- MERGED
- 0
updated Feb 12, 2021
Case study: quick sort

refinedc!33 · opened Feb 12, 2021 by Fengmin Zhu
- MERGED
- Approved
- 16
updated Feb 26, 2021
Progress on the verification of [early_alloc.c].

refinedc!32 · opened Feb 12, 2021 by Rodolphe Lepigre
- MERGED
- 0
updated Feb 12, 2021
page_alloc

refinedc!31 · opened Feb 12, 2021 by Michael Sammler
- MERGED
- 0
updated Feb 12, 2021
try new version of unification

refinedc!30 · opened Feb 12, 2021 by Michael Sammler
- MERGED
- 0
updated Feb 12, 2021
adapt to coq/coq#13840

iris!635 · opened Feb 11, 2021 by Enrico Tassi
- MERGED
- 4
updated Feb 12, 2021
Avoid relying on buggy simpl never behavior

stdpp!228 · opened Feb 11, 2021 by Tej Chajed
- MERGED
- 1
- 1
updated Feb 12, 2021
Add a size to the [ptr] type.

refinedc!29 · opened Feb 11, 2021 by Rodolphe Lepigre
- MERGED
- 0
updated Feb 12, 2021
Refactor mpool

refinedc!28 · opened Feb 11, 2021 by Michael Sammler
- MERGED
- 0
updated Feb 11, 2021
Refactor rule for arithmetic operators.

refinedc!27 · opened Feb 10, 2021 by Rodolphe Lepigre
- MERGED
- Approved
- 0
updated Feb 12, 2021
More [loc_in_bounds] infrastructure.

refinedc!26 · opened Feb 10, 2021 by Rodolphe Lepigre
- MERGED
- 0
updated Feb 10, 2021
add Nat_iter_mul

stdpp!227 · opened Feb 09, 2021 by Ralf Jung
- MERGED
- 1
updated Feb 09, 2021
Make more functions simpl never

refinedc!25 · opened Feb 08, 2021 by Michael Sammler
- MERGED
- 0
updated Feb 08, 2021
small steps towards improving subsume_list

refinedc!24 · opened Feb 04, 2021 by Michael Sammler
- MERGED
- 0
updated Feb 04, 2021
Unfold more definitions in the side condition solver.

refinedc!23 · opened Feb 02, 2021 by Rodolphe Lepigre
- MERGED
- Approved
- 0
updated Feb 03, 2021
Add tests for wp_load and wp_store failures

iris!634 · opened Feb 02, 2021 by Tej Chajed
- MERGED
- 3
updated Feb 02, 2021
Fix wp_bind's error message

iris!633 · opened Feb 02, 2021 by Tej Chajed
- MERGED
- 14
updated Feb 02, 2021
Strengthen the [LocInBounds] infrastructure.

refinedc!22 · opened Feb 01, 2021 by Rodolphe Lepigre
- MERGED
- Approved
- 11
updated Feb 02, 2021