summaryrefslogtreecommitdiff
path: root/compiler (unfollow)
Commit message (Expand)AuthorFilesLines
2024-06-04Propagated changes to statement from Charon (#223)Escherichia2-1/+2
2024-06-04Improve collapse_ctxSon Ho1-1/+42
2024-06-04Do more cleanupSon Ho1-40/+44
2024-06-04Factor out the code in collapse_ctxSon Ho2-153/+56
2024-06-04Start factoring out the code of reduce_ctx and collapse_ctxSon Ho1-91/+162
2024-06-04Improve merge_abstractions by splitting the markers before mergingSon Ho1-0/+75
2024-06-04Cleanup merge_abstractionsSon Ho1-96/+183
2024-06-03Fix an issue with the type of the values given back by loopsSon Ho3-157/+237
2024-06-03Fix a bug when composing the continuations in eval_statementSon Ho4-122/+131
2024-06-03feat: basic handling for `RValue::Len`, following AeneasVerif/charon#209Lucas Franceschino4-2/+6
2024-06-03Change the order in which we merge abstractionsSon Ho5-105/+99
2024-06-03Cleanup a bitSon Ho3-44/+53
2024-06-03Factor out some code and update some commentsSon Ho4-166/+173
2024-06-03Cleanup a bitSon Ho4-91/+87
2024-06-03Make minor modificationsSon Ho4-19/+25
2024-06-03Update some commentsSon Ho1-2/+2
2024-05-31formatAymeric Fromherz1-18/+18
2024-05-31Add documentation to collapseAymeric Fromherz1-1/+27
2024-05-31Add missing reverse when collapsing environmentAymeric Fromherz1-2/+1
2024-05-31Fix unused variables warningsAymeric Fromherz2-13/+18
2024-05-31Avoid adding shared loans twice when merging environmentsAymeric Fromherz1-5/+28
2024-05-31Add markers when creating new abstractions because of a join with bottomAymeric Fromherz3-48/+63
2024-05-31Also fix implementation of Join-SharedBorrowAymeric Fromherz1-3/+3
2024-05-30destructure_abs can be called during collapse: markers should be allowedAymeric Fromherz1-4/+0
2024-05-30Correct implementation of Join-MutBorrows: add markers when creating a new ab...Aymeric Fromherz1-3/+4
2024-05-30More lisible sign for proj_right pretty-printingAymeric Fromherz1-1/+1
2024-05-30Implement two phases of loops join + collapseAymeric Fromherz4-383/+552
2024-05-29Factor out code in ExtractBuiltin.mlSon Ho2-163/+124
2024-05-28Fix an issue with some names being ignored when generating unique variable namesSon Ho1-21/+19
2024-05-28Fix a bug in SymbolicToPure.translate_loopSon Ho1-4/+1
2024-05-28Compute marker information for borrow/loan mapsAymeric Fromherz3-50/+73
2024-05-28Add type and set/map for marker and borrow idAymeric Fromherz3-9/+21
2024-05-27Simplify collapse_ctxAymeric Fromherz1-6/+5
2024-05-27Simplify reduce_ctxAymeric Fromherz1-21/+6
2024-05-27Split collapse into collapse and reduce, rename accordinglyAymeric Fromherz4-13/+185
2024-05-27Add projection markers when joining environmentsAymeric Fromherz1-0/+59
2024-05-27Add markers everywhere, do not use them yetAymeric Fromherz10-139/+302
2024-05-24Factor out the code for Lean and CoqSon Ho1-143/+41
2024-05-24Start adding markersSon Ho6-50/+94
2024-05-24Expand debug output in loops fixed pointsAymeric Fromherz1-1/+16
2024-05-24Rename meta into spanAymeric Fromherz51-2939/+2943
2024-05-24Rename span into raw_spanAymeric Fromherz4-20/+20
2024-05-24Update charon pinNadrieril2-2/+3
2024-05-24Fix a crash which happens when type definitions are ignoredSon Ho1-2/+5
2024-05-24Print the name patterns of the definitions which fail to extractSon Ho2-15/+24
2024-05-23Update the interpreter so that it is not written in CPS style (#120)Escherichia19-2294/+2116
2024-05-23Add simp, reducible attributes to generated Lean projectorsAymeric Fromherz1-0/+10
2024-05-23Do not expand field projector for recursive structs to a let binding in LeanAymeric Fromherz1-5/+0
2024-05-23Improve formatting of Lean struct projectorsAymeric Fromherz1-2/+6
2024-05-23Add printing of projectors for recursive structs in Lean backendAymeric Fromherz1-3/+130
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-21 05:42:57 +0000