summaryrefslogtreecommitdiff
path: root/compiler (unfollow)
Commit message (Expand)AuthorFilesLines
2024-06-29had some fun writing an IsabelleHOL backendstuebinm9-132/+440
2024-06-28Remove redundant `llbc_name` fieldNadrieril8-71/+59
2024-06-25Update charonNadrieril1-3/+1
2024-06-24Update charonNadrieril15-95/+103
2024-06-21Update charonNadrieril4-2/+11
2024-06-21`predicates` got merged into `generic_params`Nadrieril8-73/+63
2024-06-18Support for renaming using the rename attribute in charon (#239)Escherichia10-291/+484
2024-06-18Tiny dedupNadrieril2-12/+4
2024-06-17Deactivate some linter options for the generated Lean filesSon Ho1-0/+9
2024-06-17Automatically add a @[reducible] attribute to some generated functionsSon Ho4-3/+66
2024-06-12Update the code extraction and regenerate the testsSon Ho2-7/+13
2024-06-12Revert "Update the scalar notation for the Lean backend"Son Ho1-1/+1
2024-06-12Revert "Fix some mistakes"Son Ho1-2/+0
2024-06-12Fix some mistakesSon Ho1-0/+2
2024-06-12Update the scalar notation for the Lean backendSon Ho1-1/+1
2024-06-11Deactivate the use of tuple projectors in the Lean backendSon Ho2-5/+8
2024-06-06Filter out type aliasesNadrieril5-8/+52
2024-06-05Fix a minor issueSon Ho1-0/+1
2024-06-05Fix a minor issueSon Ho1-0/+1
2024-06-05Update an error messageSon Ho1-6/+10
2024-06-05Relax more checks for borrow-checkingSon Ho1-1/+2
2024-06-05Relax some constraints in the symbolic execution when borrow-checkingSon Ho4-16/+54
2024-06-05Implement a BorrowCheck.borrow_check_crateSon Ho6-10/+54
2024-06-05Add an option to run Aeneas as a borrow checkerSon Ho10-276/+342
2024-06-04Propagated changes to statement from Charon (#223)Escherichia2-1/+2
2024-06-04Improve collapse_ctxSon Ho1-1/+42
2024-06-04Do more cleanupSon Ho1-40/+44
2024-06-04Factor out the code in collapse_ctxSon Ho2-153/+56
2024-06-04Start factoring out the code of reduce_ctx and collapse_ctxSon Ho1-91/+162
2024-06-04Improve merge_abstractions by splitting the markers before mergingSon Ho1-0/+75
2024-06-04Cleanup merge_abstractionsSon Ho1-96/+183
2024-06-03Fix an issue with the type of the values given back by loopsSon Ho3-157/+237
2024-06-03Fix a bug when composing the continuations in eval_statementSon Ho4-122/+131
2024-06-03feat: basic handling for `RValue::Len`, following AeneasVerif/charon#209Lucas Franceschino4-2/+6
2024-06-03Change the order in which we merge abstractionsSon Ho5-105/+99
2024-06-03Cleanup a bitSon Ho3-44/+53
2024-06-03Factor out some code and update some commentsSon Ho4-166/+173
2024-06-03Cleanup a bitSon Ho4-91/+87
2024-06-03Make minor modificationsSon Ho4-19/+25
2024-06-03Update some commentsSon Ho1-2/+2
2024-05-31formatAymeric Fromherz1-18/+18
2024-05-31Add documentation to collapseAymeric Fromherz1-1/+27
2024-05-31Add missing reverse when collapsing environmentAymeric Fromherz1-2/+1
2024-05-31Fix unused variables warningsAymeric Fromherz2-13/+18
2024-05-31Avoid adding shared loans twice when merging environmentsAymeric Fromherz1-5/+28
2024-05-31Add markers when creating new abstractions because of a join with bottomAymeric Fromherz3-48/+63
2024-05-31Also fix implementation of Join-SharedBorrowAymeric Fromherz1-3/+3
2024-05-30Remove the cps.eval_result typeSon Ho10-38/+73
2024-05-30Remove the options from the functions synthesizing the symbolic ASTSon Ho10-385/+276
2024-05-30destructure_abs can be called during collapse: markers should be allowedAymeric Fromherz1-4/+0
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-22 10:40:30 +0000