summaryrefslogtreecommitdiff
path: root/compiler (follow)
Commit message (Collapse)AuthorAgeFilesLines
* had some fun writing an IsabelleHOL backendstuebinm2024-06-299-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)
* Remove redundant `llbc_name` fieldNadrieril2024-06-288-71/+59
| | | | It's redundant with `item_meta.name`
* Update charonNadrieril2024-06-251-3/+1
|
* Update charonNadrieril2024-06-2415-95/+103
|
* Update charonNadrieril2024-06-214-2/+11
|
* `predicates` got merged into `generic_params`Nadrieril2024-06-218-73/+63
|
* Support for renaming using the rename attribute in charon (#239)Escherichia2024-06-1810-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>
* Tiny dedupNadrieril2024-06-182-12/+4
|
* Deactivate some linter options for the generated Lean filesSon Ho2024-06-171-0/+9
|
* Automatically add a @[reducible] attribute to some generated functionsSon Ho2024-06-174-3/+66
|
* Update the code extraction and regenerate the testsSon Ho2024-06-122-7/+13
|
* Revert "Update the scalar notation for the Lean backend"Son Ho2024-06-121-1/+1
| | | | This reverts commit c8272aeea205ca9cb36e22757473ca2a931a4933.
* Revert "Fix some mistakes"Son Ho2024-06-121-2/+0
| | | | This reverts commit f05a0faf14fdd558039da52624d57028eb64f9fd.
* Fix some mistakesSon Ho2024-06-121-0/+2
|
* Update the scalar notation for the Lean backendSon Ho2024-06-121-1/+1
|
* Deactivate the use of tuple projectors in the Lean backendSon Ho2024-06-112-5/+8
|
* Filter out type aliasesNadrieril2024-06-065-8/+52
|
* Fix a minor issueSon Ho2024-06-051-0/+1
|
* Fix a minor issueSon Ho2024-06-051-0/+1
|
* Update an error messageSon Ho2024-06-051-6/+10
|
* Relax more checks for borrow-checkingSon Ho2024-06-051-1/+2
|
* Relax some constraints in the symbolic execution when borrow-checkingSon Ho2024-06-054-16/+54
|
* Implement a BorrowCheck.borrow_check_crateSon Ho2024-06-056-10/+54
|
* Add an option to run Aeneas as a borrow checkerSon Ho2024-06-0510-276/+342
|
* Merge branch 'main' into son/clean-synthesisSon Ho2024-06-0526-1026/+2001
|\
| * Propagated changes to statement from Charon (#223)Escherichia2024-06-042-1/+2
| | | | | | | | | | Co-authored-by: Escherichia <escherichia@charlotte> Co-authored-by: Nadrieril <nadrieril+git@gmail.com>
| * Merge branch 'main' into son/loops2Son Ho2024-06-048-211/+206
| |\
| | * feat: basic handling for `RValue::Len`, following AeneasVerif/charon#209Lucas Franceschino2024-06-034-2/+6
| | |
| * | 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
| | |
| * | 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
| | |
| * | Add missing reverse when collapsing environmentAymeric Fromherz2024-05-311-2/+1
| | |
| * | Fix unused variables warningsAymeric Fromherz2024-05-312-13/+18
| | |
| * | 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
| | |
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-22 10:13:45 +0000