Merge requests · Iris / RefinedC

More provenances

!72 · created Jun 16, 2021 by Michael Sammler
- MERGED
- 0
updated Jun 16, 2021
add valid_ptr requirement to copy alloc id

!70 · created Jun 14, 2021 by Michael Sammler
- MERGED
- 0
updated Jun 14, 2021
Disallow creation of out of bounds pointers

!69 · created Jun 14, 2021 by Michael Sammler
- MERGED
- 0
updated Jun 14, 2021
update iris

!68 · created Jun 14, 2021 by Michael Sammler
- MERGED
- 0
updated Jun 14, 2021
Reduce shifts on Z in solve goal, unfold aligned_to and Z.divide in solve_goal and simpl in solve_goal

!67 · created Jun 10, 2021 by Michael Sammler
- MERGED
- 0
updated Jun 10, 2021
Update Cerberus version.

!66 · created Jun 02, 2021 by Rodolphe Lepigre
- MERGED
- 0
updated Jun 02, 2021
Add cast in the definition of rc_copy_alloc_id.

!64 · created May 21, 2021 by Rodolphe Lepigre
- MERGED
- 0
updated May 21, 2021
Preserve different C types in the frontend.

!63 · created May 20, 2021 by Rodolphe Lepigre
- MERGED
- Approved
- 0
updated May 20, 2021
Add support for the comma operator.

!62 · created May 19, 2021 by Rodolphe Lepigre
- MERGED
- Approved
- 0
updated May 19, 2021
Example with tagged pointers.

!60 · created May 14, 2021 by Rodolphe Lepigre
- MERGED
- 10
updated Jun 10, 2021
Hide the code in RefinedC goals.

!58 · created Apr 28, 2021 by Rodolphe Lepigre
- MERGED
- 0
updated Apr 28, 2021
Refactor the [int] type to use [val_to_Z]..

!57 · created Apr 16, 2021 by Rodolphe Lepigre
- MERGED
- Approved
- 0
updated Apr 19, 2021
Progress towards tracking pointer provenance in integers

!56 · created Apr 12, 2021 by Rodolphe Lepigre
- MERGED
- 39
updated Apr 27, 2021
Refactoring around the val_[to|of]_* functions

!55 · created Apr 08, 2021 by Rodolphe Lepigre
- MERGED
- Approved
- 0
updated Apr 09, 2021
make lang.base depend on lithium.base

!52 · created Apr 08, 2021 by Michael Sammler
- MERGED
- 1
updated Apr 08, 2021
Add a [heap_state] invariant.

!50 · created Mar 03, 2021 by Rodolphe Lepigre
- MERGED
- 17
updated Mar 09, 2021
Error improvements

!49 · created Mar 02, 2021 by Michael Sammler
- MERGED
- 0
updated Mar 02, 2021
semantics and typing rule for NotIntOp

!48 · created Mar 02, 2021 by Fengmin Zhu
- MERGED
- 5
updated Mar 04, 2021
Cleaning up around [lang.v]

!47 · created Feb 26, 2021 by Rodolphe Lepigre
- MERGED
- 0
updated Mar 02, 2021
Tactic based on lia and autorewrite to solve location equality

!46 · created Feb 22, 2021 by Rodolphe Lepigre
- MERGED
- 15
updated Feb 24, 2021