Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | Update the tests for tuples | Son Ho | 2024-06-11 | 4 | -22/+85 |
| | |||||
* | 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 |
|\ | | | | | Add a `-borrow-check` option | ||||
| * | 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 |
|\ | | | | | Remove the use of `Option` from the functions synthesizing the symbolic AST | ||||
| * | 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 |
| | | | | | | | | | | Co-authored-by: Escherichia <escherichia@charlotte> Co-authored-by: Nadrieril <nadrieril+git@gmail.com> | ||||
* | | Merge pull request #228 from AeneasVerif/son/loops2 | Son HO | 2024-06-04 | 31 | -1149/+2143 |
|\ \ | | | | | | | Add support for projection markers when joining environments | ||||
| * \ | 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 |
| | | |