| Commit message (Expand) | Author | Files | Lines |
|---|
| 2024-06-24 | Update charon | Nadrieril | 15 | -95/+103 |
| 2024-06-21 | Update charon | Nadrieril | 4 | -2/+11 |
| 2024-06-21 | `predicates` got merged into `generic_params` | Nadrieril | 8 | -73/+63 |
| 2024-06-18 | Support for renaming using the rename attribute in charon (#239) | Escherichia | 10 | -291/+484 |
| 2024-06-18 | Tiny dedup | Nadrieril | 2 | -12/+4 |
| 2024-06-17 | Deactivate some linter options for the generated Lean files | Son Ho | 1 | -0/+9 |
| 2024-06-17 | Automatically add a @[reducible] attribute to some generated functions | Son Ho | 4 | -3/+66 |
| 2024-06-12 | Update the code extraction and regenerate the tests | Son Ho | 2 | -7/+13 |
| 2024-06-12 | Revert "Update the scalar notation for the Lean backend" | Son Ho | 1 | -1/+1 |
| 2024-06-12 | Revert "Fix some mistakes" | Son Ho | 1 | -2/+0 |
| 2024-06-12 | Fix some mistakes | Son Ho | 1 | -0/+2 |
| 2024-06-12 | Update the scalar notation for the Lean backend | Son Ho | 1 | -1/+1 |
| 2024-06-11 | Deactivate the use of tuple projectors in the Lean backend | Son Ho | 2 | -5/+8 |
| 2024-06-06 | Filter out type aliases | Nadrieril | 5 | -8/+52 |
| 2024-06-05 | Fix a minor issue | Son Ho | 1 | -0/+1 |
| 2024-06-05 | Fix a minor issue | Son Ho | 1 | -0/+1 |
| 2024-06-05 | Update an error message | Son Ho | 1 | -6/+10 |
| 2024-06-05 | Relax more checks for borrow-checking | Son Ho | 1 | -1/+2 |
| 2024-06-05 | Relax some constraints in the symbolic execution when borrow-checking | Son Ho | 4 | -16/+54 |
| 2024-06-05 | Implement a BorrowCheck.borrow_check_crate | Son Ho | 6 | -10/+54 |
| 2024-06-05 | Add an option to run Aeneas as a borrow checker | Son Ho | 10 | -276/+342 |
| 2024-06-04 | Propagated changes to statement from Charon (#223) | Escherichia | 2 | -1/+2 |
| 2024-06-04 | Improve collapse_ctx | Son Ho | 1 | -1/+42 |
| 2024-06-04 | Do more cleanup | Son Ho | 1 | -40/+44 |
| 2024-06-04 | Factor out the code in collapse_ctx | Son Ho | 2 | -153/+56 |
| 2024-06-04 | Start factoring out the code of reduce_ctx and collapse_ctx | Son Ho | 1 | -91/+162 |
| 2024-06-04 | Improve merge_abstractions by splitting the markers before merging | Son Ho | 1 | -0/+75 |
| 2024-06-04 | Cleanup merge_abstractions | Son Ho | 1 | -96/+183 |
| 2024-06-03 | Fix an issue with the type of the values given back by loops | Son Ho | 3 | -157/+237 |
| 2024-06-03 | Fix a bug when composing the continuations in eval_statement | Son Ho | 4 | -122/+131 |
| 2024-06-03 | feat: basic handling for `RValue::Len`, following AeneasVerif/charon#209 | Lucas Franceschino | 4 | -2/+6 |
| 2024-06-03 | Change the order in which we merge abstractions | Son Ho | 5 | -105/+99 |
| 2024-06-03 | Cleanup a bit | Son Ho | 3 | -44/+53 |
| 2024-06-03 | Factor out some code and update some comments | Son Ho | 4 | -166/+173 |
| 2024-06-03 | Cleanup a bit | Son Ho | 4 | -91/+87 |
| 2024-06-03 | Make minor modifications | Son Ho | 4 | -19/+25 |
| 2024-06-03 | Update some comments | Son Ho | 1 | -2/+2 |
| 2024-05-31 | format | Aymeric Fromherz | 1 | -18/+18 |
| 2024-05-31 | Add documentation to collapse | Aymeric Fromherz | 1 | -1/+27 |
| 2024-05-31 | Add missing reverse when collapsing environment | Aymeric Fromherz | 1 | -2/+1 |
| 2024-05-31 | Fix unused variables warnings | Aymeric Fromherz | 2 | -13/+18 |
| 2024-05-31 | Avoid adding shared loans twice when merging environments | Aymeric Fromherz | 1 | -5/+28 |
| 2024-05-31 | Add markers when creating new abstractions because of a join with bottom | Aymeric Fromherz | 3 | -48/+63 |
| 2024-05-31 | Also fix implementation of Join-SharedBorrow | Aymeric Fromherz | 1 | -3/+3 |
| 2024-05-30 | Remove the cps.eval_result type | Son Ho | 10 | -38/+73 |
| 2024-05-30 | Remove the options from the functions synthesizing the symbolic AST | Son Ho | 10 | -385/+276 |
| 2024-05-30 | destructure_abs can be called during collapse: markers should be allowed | Aymeric Fromherz | 1 | -4/+0 |
| 2024-05-30 | Correct implementation of Join-MutBorrows: add markers when creating a new ab... | Aymeric Fromherz | 1 | -3/+4 |
| 2024-05-30 | More lisible sign for proj_right pretty-printing | Aymeric Fromherz | 1 | -1/+1 |
| 2024-05-30 | Implement two phases of loops join + collapse | Aymeric Fromherz | 4 | -383/+552 |
