summaryrefslogtreecommitdiff
Commit message (Expand)AuthorAgeFilesLines
* Update the F* betreeSon Ho2024-06-053-144/+280
* Fix a minor issueSon Ho2024-06-051-0/+1
* Update the betreeSon Ho2024-06-051-99/+98
* Regenerate some testsSon Ho2024-06-051-14/+2
* Add some negative tests for the borrow checkerSon Ho2024-06-052-0/+105
* Update an error messageSon Ho2024-06-051-6/+10
* Add more testsSon Ho2024-06-055-0/+79
* Update the test runnerSon Ho2024-06-051-1/+4
* Relax more checks for borrow-checkingSon Ho2024-06-051-1/+2
* Relax some constraints in the symbolic execution when borrow-checkingSon Ho2024-06-054-16/+54
* Update the test runner to allow the syntax [!lean] and [borrow-check]Son Ho2024-06-0514-34/+65
* Implement a BorrowCheck.borrow_check_crateSon Ho2024-06-056-10/+54
* Add an option to run Aeneas as a borrow checkerSon Ho2024-06-0510-276/+342
* Merge pull request #227 from AeneasVerif/son/clean-synthesisSon HO2024-06-0515-423/+345
|\
| * 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
* | Merge pull request #228 from AeneasVerif/son/loops2Son HO2024-06-0431-1149/+2143
|\ \
| * \ 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 ab...Aymeric Fromherz2024-05-301-3/+4
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-28 03:05:48 +0000