summaryrefslogtreecommitdiff
path: root/compiler (follow)
Commit message (Collapse)AuthorAgeFilesLines
* Propagated changes to statement from Charon (#223)Escherichia2024-06-042-1/+2
| | | | | Co-authored-by: Escherichia <escherichia@charlotte> Co-authored-by: Nadrieril <nadrieril+git@gmail.com>
* Merge branch 'main' into son/loops2Son Ho2024-06-048-211/+206
|\
| * feat: basic handling for `RValue::Len`, following AeneasVerif/charon#209Lucas Franceschino2024-06-034-2/+6
| |
| * Factor out code in ExtractBuiltin.mlSon Ho2024-05-292-163/+124
| |
| * Fix an issue with some names being ignored when generating unique variable namesSon Ho2024-05-281-21/+19
| |
| * Fix a bug in SymbolicToPure.translate_loopSon Ho2024-05-281-4/+1
| |
| * Factor out the code for Lean and CoqSon Ho2024-05-241-143/+41
| |
| * Merge branch 'main' into afromher/recursive_projectorsSon Ho2024-05-2451-4933/+4787
| |\
| * | Add simp, reducible attributes to generated Lean projectorsAymeric Fromherz2024-05-231-0/+10
| | |
| * | Do not expand field projector for recursive structs to a let binding in LeanAymeric Fromherz2024-05-231-5/+0
| | |
| * | Improve formatting of Lean struct projectorsAymeric Fromherz2024-05-231-2/+6
| | |
| * | Add printing of projectors for recursive structs in Lean backendAymeric Fromherz2024-05-231-3/+130
| | |
* | | Improve collapse_ctxSon Ho2024-06-041-1/+42
| | |
* | | Do more cleanupSon Ho2024-06-041-40/+44
| | |
* | | Factor out the code in collapse_ctxSon Ho2024-06-042-153/+56
| | |
* | | Start factoring out the code of reduce_ctx and collapse_ctxSon Ho2024-06-041-91/+162
| | |
* | | Improve merge_abstractions by splitting the markers before mergingSon Ho2024-06-041-0/+75
| | |
* | | Cleanup merge_abstractionsSon Ho2024-06-041-96/+183
| | |
* | | Fix an issue with the type of the values given back by loopsSon Ho2024-06-033-157/+237
| | |
* | | Fix a bug when composing the continuations in eval_statementSon Ho2024-06-034-122/+131
| | |
* | | Change the order in which we merge abstractionsSon Ho2024-06-035-105/+99
| | |
* | | Cleanup a bitSon Ho2024-06-033-44/+53
| | |
* | | Factor out some code and update some commentsSon Ho2024-06-034-166/+173
| | |
* | | Cleanup a bitSon Ho2024-06-034-91/+87
| | |
* | | Make minor modificationsSon Ho2024-06-034-19/+25
| | |
* | | Update some commentsSon Ho2024-06-031-2/+2
| | |
* | | formatAymeric Fromherz2024-05-311-18/+18
| | |
* | | Add documentation to collapseAymeric Fromherz2024-05-311-1/+27
| | |
* | | Add missing reverse when collapsing environmentAymeric Fromherz2024-05-311-2/+1
| | |
* | | Fix unused variables warningsAymeric Fromherz2024-05-312-13/+18
| | |
* | | Avoid adding shared loans twice when merging environmentsAymeric Fromherz2024-05-311-5/+28
| | |
* | | Add markers when creating new abstractions because of a join with bottomAymeric Fromherz2024-05-313-48/+63
| | |
* | | Also fix implementation of Join-SharedBorrowAymeric Fromherz2024-05-311-3/+3
| | |
* | | destructure_abs can be called during collapse: markers should be allowedAymeric Fromherz2024-05-301-4/+0
| | |
* | | Correct implementation of Join-MutBorrows: add markers when creating a new ↵Aymeric Fromherz2024-05-301-3/+4
| | | | | | | | | | | | abstraction
* | | More lisible sign for proj_right pretty-printingAymeric Fromherz2024-05-301-1/+1
| | |
* | | Implement two phases of loops join + collapseAymeric Fromherz2024-05-304-383/+552
| | |
* | | Compute marker information for borrow/loan mapsAymeric Fromherz2024-05-283-50/+73
| | |
* | | Add type and set/map for marker and borrow idAymeric Fromherz2024-05-283-9/+21
| | |
* | | Simplify collapse_ctxAymeric Fromherz2024-05-271-6/+5
| | |
* | | Simplify reduce_ctxAymeric Fromherz2024-05-271-21/+6
| | |
* | | Split collapse into collapse and reduce, rename accordinglyAymeric Fromherz2024-05-274-13/+185
| | |
* | | Add projection markers when joining environmentsAymeric Fromherz2024-05-271-0/+59
| | |
* | | Add markers everywhere, do not use them yetAymeric Fromherz2024-05-2710-139/+302
| | |
* | | Start adding markersSon Ho2024-05-246-50/+94
| |/ |/|
* | Expand debug output in loops fixed pointsAymeric Fromherz2024-05-241-1/+16
| |
* | Rename meta into spanAymeric Fromherz2024-05-2451-2939/+2943
| |
* | Rename span into raw_spanAymeric Fromherz2024-05-244-20/+20
| |
* | Update charon pinNadrieril2024-05-242-2/+3
| |
* | Fix a crash which happens when type definitions are ignoredSon Ho2024-05-241-2/+5
| |
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 02:46:11 +0000