Merge requests · Iris / RefinedC

Check generated files on CI

!34 · created Feb 12, 2021 by Michael Sammler
- Merged
updated Feb 12, 2021
Progress on the verification of [early_alloc.c].

!32 · created Feb 12, 2021 by Rodolphe Lepigre
- Merged
updated Feb 12, 2021
page_alloc

!31 · created Feb 12, 2021 by Michael Sammler
- Merged
updated Feb 12, 2021
Refactor rule for arithmetic operators.

!27 · created Feb 10, 2021 by Rodolphe Lepigre
- Merged
- Approved
updated Feb 12, 2021
try new version of unification

!30 · created Feb 12, 2021 by Michael Sammler
- Merged
updated Feb 12, 2021
Add a size to the [ptr] type.

!29 · created Feb 11, 2021 by Rodolphe Lepigre
updated Feb 12, 2021
Refactor mpool

!28 · created Feb 11, 2021 by Michael Sammler
- Merged
updated Feb 11, 2021
More [loc_in_bounds] infrastructure.

!26 · created Feb 10, 2021 by Rodolphe Lepigre
- Merged
updated Feb 10, 2021
Make more functions simpl never

!25 · created Feb 08, 2021 by Michael Sammler
- Merged
updated Feb 08, 2021
small steps towards improving subsume_list

!24 · created Feb 04, 2021 by Michael Sammler
- Merged
updated Feb 04, 2021
Unfold more definitions in the side condition solver.

!23 · created Feb 02, 2021 by Rodolphe Lepigre
- Merged
- Approved
updated Feb 03, 2021
Strengthen the [LocInBounds] infrastructure.

!22 · created Feb 01, 2021 by Rodolphe Lepigre
- Merged
- 11
- Approved
updated Feb 02, 2021
Infrastructure for [SimpleSubsumeVal].

!21 · created Jan 29, 2021 by Rodolphe Lepigre
- Merged
- Approved
updated Feb 01, 2021
Fix inversion of signedness for [uintptr_t] and [intptr_t].

!20 · created Jan 28, 2021 by Rodolphe Lepigre
- Merged
updated Jan 28, 2021
Performance improvements?

!19 · created Jan 27, 2021 by Michael Sammler
- Merged
updated Jan 27, 2021
Make caesium an ectxi language

!18 · created Jan 26, 2021 by Michael Sammler
- Merged
updated Jan 26, 2021
Sugar in the front end + Coq pretty printing

!16 · created Jan 13, 2021 by Rodolphe Lepigre
- Merged
- 17
- Approved
updated Jan 15, 2021
Encode the constrained type into own_constrained.

!14 · created Dec 18, 2020 by Rodolphe Lepigre
- Merged
- 3
updated Jan 14, 2021
Unfold instantiated evars on each liRStep.

!15 · created Jan 12, 2021 by Rodolphe Lepigre
- Merged
- 1
updated Jan 12, 2021
Add infrastructure to destruct products in function parameters.

!13 · created Dec 15, 2020 by Rodolphe Lepigre
- Merged
- Approved
updated Dec 17, 2020