summaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAgeFilesLines
* 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
|
* Merge pull request #202 from AeneasVerif/afromher_debugAymeric Fromherz2024-05-241-1/+16
|\ | | | | Expand debug output in loops fixed points
| * Merge remote-tracking branch 'origin/main' into afromher_debugAymeric Fromherz2024-05-2491-3550/+5686
| |\ | |/ |/|
* | Merge pull request #197 from AeneasVerif/test-harness3Guillaume Boisseau2024-05-2491-3550/+5686
|\ \
| * | runner: Use full path and use an enum for crate vs fileNadrieril2024-05-242-43/+55
| | |
| * | runner: Do both steps of generation at onceNadrieril2024-05-242-24/+25
| | |
| * | Auto-detect test casesNadrieril2024-05-244-33/+39
| | |
| * | Use runner to generate llbcNadrieril2024-05-243-84/+126
| | |
| * | Tweak a pathNadrieril2024-05-2452-1221/+1220
| | |
| * | Import test suite from charonNadrieril2024-05-2427-56/+4148
| | |
| * | Remove secondary betree testNadrieril2024-05-2410-2101/+4
| | | | | | | | | | | | | | | Opened https://github.com/AeneasVerif/aeneas/issues/196 to remember to add a more adequate replacement test.
| * | Let the runner choose which backends to useNadrieril2024-05-242-43/+28
| | |
| * | Cleanup test runnerNadrieril2024-05-241-99/+124
| | |
| * | Set all options in the test runnerNadrieril2024-05-242-51/+58
| | |
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 05:26:58 +0000