Merge requests · Iris / RefinedC

Add CheckOwnInContext

!92 · created Jul 12, 2021 by Michael Sammler
- MERGED
- 0
updated Jul 12, 2021
try removing pinning of conf-mpfr

!93 · created Jul 14, 2021 by Michael Sammler
- MERGED
- 0
updated Jul 14, 2021
Bitblast: tactics for solving integer equality with bits

!94 · created Jul 15, 2021 by Fengmin Zhu
- MERGED
- 17
updated Jul 16, 2021
Remove generated files and associated CI checks.

!95 · created Jul 15, 2021 by Rodolphe Lepigre
- MERGED
- 0
updated Jul 16, 2021
cleanup base.v

!96 · created Jul 16, 2021 by Michael Sammler
- MERGED
- 0
updated Jul 16, 2021
Implement && and || using IfE.

!97 · created Jul 16, 2021 by Rodolphe Lepigre
- MERGED
- Approved
- 3
updated Jul 16, 2021
parameterise operators with boolean result by the result integer type

!99 · created Jul 20, 2021 by Lennard Gäher
- MERGED
- Approved
- 9
updated Jul 27, 2021
More support comparing pointers with 0 in the front end + rules for if and assert on pointers.

!100 · created Jul 21, 2021 by Rodolphe Lepigre
- MERGED
- 11
updated Aug 03, 2021
update to coq 8.13.2

!101 · created Jul 27, 2021 by Michael Sammler
- MERGED
- 0
updated Jul 27, 2021
allow opening invariants around typed_read_end and typed_write_end

!103 · created Jul 28, 2021 by Michael Sammler
- MERGED
- 0
updated Jul 30, 2021
Generate [return 0] for main + small refactoring.

!104 · created Aug 03, 2021 by Rodolphe Lepigre
- MERGED
- 1
- 0
updated Aug 03, 2021
split out heap_loc_eq

!105 · created Aug 03, 2021 by Michael Sammler
- MERGED
- 0
updated Aug 03, 2021
add via_vm_compute

!106 · created Aug 05, 2021 by Michael Sammler
- MERGED
- 0
updated Aug 05, 2021
Use multisuccess of typeclasses eauto to get rid of n parameter in FindInContext

!107 · created Aug 05, 2021 by Michael Sammler
- MERGED
- 0
updated Aug 05, 2021
Control better which sideconditions get shelved

!108 · created Aug 17, 2021 by Michael Sammler
- MERGED
- 0
updated Aug 19, 2021
Bit-wise reasoning

!109 · created Aug 19, 2021 by Fengmin Zhu
- MERGED
- 85
updated Aug 27, 2021
change implementation of via_vm_compute and add negb simpl instances

!110 · created Aug 25, 2021 by Michael Sammler
- MERGED
- 0
updated Aug 25, 2021
Add [cast_to_bool] and factorise "if" rules.

!111 · created Sep 13, 2021 by Rodolphe Lepigre
- MERGED
- Approved
- 3
updated Sep 13, 2021
Generalize the [boolean] type.

!112 · created Sep 15, 2021 by Rodolphe Lepigre
- MERGED
- 10
updated Sep 16, 2021
Better handling of Coq paths in the frontend.

!113 · created Sep 16, 2021 by Rodolphe Lepigre
- MERGED
- Approved
- 2
updated Sep 20, 2021