summaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAgeFilesLines
* Merge branch 'main' into son/clean-synthesisSon Ho2024-06-0562-1437/+2425
|\
| * Merge pull request #231 from Nadrieril/bump-haxGuillaume Boisseau2024-06-0529-291/+282
| |\
| | * Update charonNadrieril2024-06-0529-291/+282
| |/
| * Propagated changes to statement from Charon (#223)Escherichia2024-06-044-5/+6
| | | | | | | | | | Co-authored-by: Escherichia <escherichia@charlotte> Co-authored-by: Nadrieril <nadrieril+git@gmail.com>
| * Merge pull request #228 from AeneasVerif/son/loops2Son HO2024-06-0431-1149/+2143
| |\ | | | | | | Add support for projection markers when joining environments
| | * Merge branch 'main' into son/loops2Son Ho2024-06-04188-5984/+2764
| | |\ | | |/ | |/|
| * | Merge pull request #230 from W95Psp/follow-up-charon-pr-209Guillaume Boisseau2024-06-047-6/+12
| |\ \
| | * | Fix the CI pin checkNadrieril2024-06-041-0/+2
| | | |
| | * | Update charon pinNadrieril2024-06-042-4/+4
| | | |
| | * | feat: basic handling for `RValue::Len`, following AeneasVerif/charon#209Lucas Franceschino2024-06-034-2/+6
| |/ /
| | * 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
| | |
| | * Add a testSon Ho2024-06-034-103/+123
| | |
| | * 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
| | |
| | * Regenerate testsAymeric Fromherz2024-05-3113-35/+35
| | |
| | * Add missing reverse when collapsing environmentAymeric Fromherz2024-05-311-2/+1
| | |
| | * Fix unused variables warningsAymeric Fromherz2024-05-312-13/+18
| | |
| | * Regenerate test outputAymeric Fromherz2024-05-3119-108/+2588
| | |
| | * 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-3023-2971/+660
| | |
| | * Compute marker information for borrow/loan mapsAymeric Fromherz2024-05-283-50/+73
| | |
| | * Add type and set/map for marker and borrow idAymeric Fromherz2024-05-284-10/+22
| | |
| | * 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
| | |
| | * Downgrade the version of duneSon Ho2024-05-241-1/+1
| | |
* | | Remove the cps.eval_result typeSon Ho2024-05-3010-38/+73
| | |
* | | Remove the options from the functions synthesizing the symbolic ASTSon Ho2024-05-3011-391/+282
|/ /
* | Merge pull request #226 from AeneasVerif/remove-rust-scriptsGuillaume Boisseau2024-05-302-157/+0
|\ \
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 06:09:03 +0000