Commit message (Expand) | Author | Age | Files | Lines | ||
---|---|---|---|---|---|---|
... | ||||||
* | Merge pull request #232 from Nadrieril/type-alias | Guillaume Boisseau | 2024-06-06 | 7 | -12/+56 | |
|\ | ||||||
| * | Filter out type aliases | Nadrieril | 2024-06-06 | 7 | -12/+56 | |
|/ | ||||||
* | Merge pull request #233 from AeneasVerif/son/borrow-check | Son HO | 2024-06-06 | 45 | -759/+1500 | |
|\ | ||||||
| * | Regenerate the Coq and Lean betrees | Son Ho | 2024-06-05 | 2 | -178/+423 | |
| * | Fix a minor issue | Son Ho | 2024-06-05 | 1 | -0/+1 | |
| * | Update the F* betree | Son Ho | 2024-06-05 | 3 | -144/+280 | |
| * | Fix a minor issue | Son Ho | 2024-06-05 | 1 | -0/+1 | |
| * | Update the betree | Son Ho | 2024-06-05 | 1 | -99/+98 | |
| * | Regenerate some tests | Son Ho | 2024-06-05 | 1 | -14/+2 | |
| * | Add some negative tests for the borrow checker | Son Ho | 2024-06-05 | 2 | -0/+105 | |
| * | Update an error message | Son Ho | 2024-06-05 | 1 | -6/+10 | |
| * | Add more tests | Son Ho | 2024-06-05 | 5 | -0/+79 | |
| * | Update the test runner | Son Ho | 2024-06-05 | 1 | -1/+4 | |
| * | Relax more checks for borrow-checking | Son Ho | 2024-06-05 | 1 | -1/+2 | |
| * | Relax some constraints in the symbolic execution when borrow-checking | Son Ho | 2024-06-05 | 4 | -16/+54 | |
| * | Update the test runner to allow the syntax [!lean] and [borrow-check] | Son Ho | 2024-06-05 | 14 | -34/+65 | |
| * | Implement a BorrowCheck.borrow_check_crate | Son Ho | 2024-06-05 | 6 | -10/+54 | |
| * | Add an option to run Aeneas as a borrow checker | Son Ho | 2024-06-05 | 10 | -276/+342 | |
|/ | ||||||
* | Merge pull request #227 from AeneasVerif/son/clean-synthesis | Son HO | 2024-06-05 | 15 | -423/+345 | |
|\ | ||||||
| * | Merge branch 'main' into son/clean-synthesis | Son Ho | 2024-06-05 | 62 | -1437/+2425 | |
| |\ | |/ |/| | ||||||
* | | Merge pull request #231 from Nadrieril/bump-hax | Guillaume Boisseau | 2024-06-05 | 29 | -291/+282 | |
|\ \ | ||||||
| * | | Update charon | Nadrieril | 2024-06-05 | 29 | -291/+282 | |
|/ / | ||||||
* | | Propagated changes to statement from Charon (#223) | Escherichia | 2024-06-04 | 4 | -5/+6 | |
* | | Merge pull request #228 from AeneasVerif/son/loops2 | Son HO | 2024-06-04 | 31 | -1149/+2143 | |
|\ \ | ||||||
| * \ | Merge branch 'main' into son/loops2 | Son Ho | 2024-06-04 | 188 | -5984/+2764 | |
| |\ \ | |/ / |/| | | ||||||
* | | | Merge pull request #230 from W95Psp/follow-up-charon-pr-209 | Guillaume Boisseau | 2024-06-04 | 7 | -6/+12 | |
|\ \ \ | ||||||
| * | | | Fix the CI pin check | Nadrieril | 2024-06-04 | 1 | -0/+2 | |
| * | | | Update charon pin | Nadrieril | 2024-06-04 | 2 | -4/+4 | |
| * | | | feat: basic handling for `RValue::Len`, following AeneasVerif/charon#209 | Lucas Franceschino | 2024-06-03 | 4 | -2/+6 | |
|/ / / | ||||||
| * | | Improve collapse_ctx | Son Ho | 2024-06-04 | 1 | -1/+42 | |
| * | | Do more cleanup | Son Ho | 2024-06-04 | 1 | -40/+44 | |
| * | | Factor out the code in collapse_ctx | Son Ho | 2024-06-04 | 2 | -153/+56 | |
| * | | Start factoring out the code of reduce_ctx and collapse_ctx | Son Ho | 2024-06-04 | 1 | -91/+162 | |
| * | | Improve merge_abstractions by splitting the markers before merging | Son Ho | 2024-06-04 | 1 | -0/+75 | |
| * | | Cleanup merge_abstractions | Son Ho | 2024-06-04 | 1 | -96/+183 | |
| * | | Add a test | Son Ho | 2024-06-03 | 4 | -103/+123 | |
| * | | Fix an issue with the type of the values given back by loops | Son Ho | 2024-06-03 | 3 | -157/+237 | |
| * | | Fix a bug when composing the continuations in eval_statement | Son Ho | 2024-06-03 | 4 | -122/+131 | |
| * | | Change the order in which we merge abstractions | Son Ho | 2024-06-03 | 5 | -105/+99 | |
| * | | Cleanup a bit | Son Ho | 2024-06-03 | 3 | -44/+53 | |
| * | | Factor out some code and update some comments | Son Ho | 2024-06-03 | 4 | -166/+173 | |
| * | | Cleanup a bit | Son Ho | 2024-06-03 | 4 | -91/+87 | |
| * | | Make minor modifications | Son Ho | 2024-06-03 | 4 | -19/+25 | |
| * | | Update some comments | Son Ho | 2024-06-03 | 1 | -2/+2 | |
| * | | format | Aymeric Fromherz | 2024-05-31 | 1 | -18/+18 | |
| * | | Add documentation to collapse | Aymeric Fromherz | 2024-05-31 | 1 | -1/+27 | |
| * | | Regenerate tests | Aymeric Fromherz | 2024-05-31 | 13 | -35/+35 | |
| * | | Add missing reverse when collapsing environment | Aymeric Fromherz | 2024-05-31 | 1 | -2/+1 | |
| * | | Fix unused variables warnings | Aymeric Fromherz | 2024-05-31 | 2 | -13/+18 | |
| * | | Regenerate test output | Aymeric Fromherz | 2024-05-31 | 19 | -108/+2588 |