| Commit message (Collapse) | Author | Files | Lines | ||
|---|---|---|---|---|---|
| 2024-06-29 | had some fun writing an IsabelleHOL backend | stuebinm | 9 | -132/+440 | |
| (do not actually use this, most things are broken, and the primitives lib barely exists and is simply incorrect. But it is enough to create syntax-correct Isabelle code for relatively simply rust code, as long as it does not contain any uses of traits) | |||||
| 2024-06-28 | Remove redundant `llbc_name` field | Nadrieril | 8 | -71/+59 | |
| It's redundant with `item_meta.name` | |||||
| 2024-06-25 | Update charon | Nadrieril | 1 | -3/+1 | |
| 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 | |
| * support for renaming using the rename attribute in charon * support for global decl * add support for renaming field * applied suggested changes and began adding support for variant * finished support for renaming variant * applied suggested changes * add tests * fixed variant and field renaming * update charon-pin * update flake.lock * Update the charon pin * Fix an issue with renaming trait method implementations * Fix an issue with the renaming of trait implementations * Fix an issue when renaming enumerations * Update the Charon pin * Fix the F* tests * Fix an issue with the spans for the loops * Fix the tests * Update a comment * Use fuel in the coq tests * Generate the template decreases clauses by default --------- Co-authored-by: Escherichia <escherichia@charlotte> Co-authored-by: Son Ho <hosonmarc@gmail.com> | |||||
| 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 | |
| This reverts commit c8272aeea205ca9cb36e22757473ca2a931a4933. | |||||
| 2024-06-12 | Revert "Fix some mistakes" | Son Ho | 1 | -2/+0 | |
| This reverts commit f05a0faf14fdd558039da52624d57028eb64f9fd. | |||||
| 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 | |
| Co-authored-by: Escherichia <escherichia@charlotte> Co-authored-by: Nadrieril <nadrieril+git@gmail.com> | |||||
| 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 | |
 |
index : aeneas | |
| aeneas rust verifier with a hacky Isabelle backend |
| summaryrefslogtreecommitdiff |