summaryrefslogtreecommitdiff
Commit message (Expand)AuthorAgeFilesLines
...
| * | 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 ab...Aymeric Fromherz2024-05-301-3/+4
| * | 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
|\ \
| * | Remove unused `rust-scripts`Nadrieril2024-05-302-157/+0
|/ /
* | Merge pull request #225 from AeneasVerif/update-charon-pinGuillaume Boisseau2024-05-302-8/+14
|\ \
| * | Update charon pin to local commit when developingNadrieril2024-05-302-8/+14
|/ /
* | Merge pull request #217 from AeneasVerif/document-testsGuillaume Boisseau2024-05-307-197/+284
|\ \
| * | Improve the tests READMENadrieril2024-05-302-14/+22
| * | runner: Factor out backend-specific optionsNadrieril2024-05-302-49/+56
| * | runner: Split up into multiple filesNadrieril2024-05-306-198/+191
| * | runner: make the backend map a submodule of `Backend`Nadrieril2024-05-301-36/+48
| * | tests: Add a READMENadrieril2024-05-301-0/+67
|/ /
* | Merge pull request #149 from RaitoBezarius/reexport-our-charonGuillaume Boisseau2024-05-292-0/+20
|\ \
| * | chore: explain a Nix-powered workflowRyan Lahfa2024-05-292-0/+20
|/ /
* | Merge pull request #218 from AeneasVerif/ci-check-pinGuillaume Boisseau2024-05-295-2/+31
|\ \
| * | ci: Check correctness of the charon pinned commitNadrieril2024-05-295-2/+31
|/ /
* | Merge pull request #222 from AeneasVerif/son/readmeSon HO2024-05-291-6/+7
|\ \
| * | Update the READMESon Ho2024-05-291-6/+7
|/ /
* | Merge pull request #221 from AeneasVerif/son/builtinsSon HO2024-05-292-163/+124
|\ \
| * \ Merge branch 'main' into son/builtinsSon HO2024-05-290-0/+0
| |\ \ | |/ / |/| |
* | | Merge pull request #220 from AeneasVerif/son/collisionsSon HO2024-05-293-25/+23
|\ \ \
| * \ \ Merge branch 'main' into son/collisionsSon HO2024-05-290-0/+0
| |\ \ \ | |/ / / |/| | |
* | | | Merge pull request #219 from AeneasVerif/son/infiniteSon HO2024-05-285-5/+77
|\ \ \ \
| | | * | 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-283-25/+23
| |/ /
| * | Reactivate the infinite-loop.rs testSon Ho2024-05-284-1/+76
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 07:40:07 +0000