summaryrefslogtreecommitdiff
path: root/compiler/SymbolicToPure.ml (unfollow)
Commit message (Expand)AuthorFilesLines
2024-06-28Remove redundant `llbc_name` fieldNadrieril1-14/+4
2024-06-24Update charonNadrieril1-26/+21
2024-06-21`predicates` got merged into `generic_params`Nadrieril1-39/+29
2024-06-18Support for renaming using the rename attribute in charon (#239)Escherichia1-7/+9
2024-06-17Automatically add a @[reducible] attribute to some generated functionsSon Ho1-2/+4
2024-06-11Deactivate the use of tuple projectors in the Lean backendSon Ho1-1/+1
2024-06-06Filter out type aliasesNadrieril1-0/+3
2024-06-05Add an option to run Aeneas as a borrow checkerSon Ho1-1/+1
2024-05-28Fix a bug in SymbolicToPure.translate_loopSon Ho1-4/+1
2024-05-27Add markers everywhere, do not use them yetAymeric Fromherz1-8/+8
2024-05-24Rename meta into spanAymeric Fromherz1-274/+274
2024-05-24Update charon pinNadrieril1-0/+1
2024-05-24Print the name patterns of the definitions which fail to extractSon Ho1-4/+5
2024-05-23Do not expand field projector for recursive structs to a let binding in LeanAymeric Fromherz1-5/+0
2024-04-22Fix an issue when joining a symbolic value with bottomSon Ho1-2/+2
2024-04-22Reformat some filesSon Ho1-6/+18
2024-04-18item_metaNadrieril1-33/+33
2024-04-11Update a commentSon Ho1-2/+2
2024-04-07Cleanup a bit and improve the error messagesSon Ho1-5/+3
2024-04-05Resolved comments and added the name of the not translated elementEscherichia1-1/+4
2024-04-05resolved commentsEscherichia1-1/+4
2024-04-05error catching should now be able to tell when code couldn't be generatedEscherichia1-1/+6
2024-04-04Add field mk_return, mk_panic in SymbolicToPure.bs_ctxSon Ho1-90/+150
2024-04-04Update the extractionSon Ho1-4/+3
2024-04-04Make a minor update in SymbolicToPureSon Ho1-8/+7
2024-04-04Improve the name of the backward functions furtherSon Ho1-2/+11
2024-04-04Update the names of the synthesized backward functionsSon Ho1-0/+9
2024-04-03resolved requested changesEscherichia1-2/+2
2024-04-03added Error and EError to expressions and propagated related changesEscherichia1-0/+4
2024-03-29Cleanup and fix a mistakeSon Ho1-122/+99
2024-03-29Add some error messagesSon Ho1-6/+7
2024-03-29Cleanup a bitSon Ho1-2/+1
2024-03-29formatting and changed save_error condition for failing from b to not bEscherichia1-15/+40
2024-03-29added file and line arg to craise and cassertEscherichia1-74/+74
2024-03-28formattingEscherichia1-101/+174
2024-03-28changes after git rebase mainEscherichia1-7/+7
2024-03-28Should answer all comments, there are still some TODO: error message leftEscherichia1-34/+34
2024-03-28Added sanity_check and sanity_check_opt_meta helpers and changed sanity check...Escherichia1-8/+8
2024-03-28added a meta option field to norm_ctx and changed the meta used by some asser...Escherichia1-1/+1
2024-03-28Still need to fill the TODO: error message and check some meta but it buildsEscherichia1-5/+5
2024-03-28WIP: translate.ml and extract.ml do not compile. Some assert left to do and w...Escherichia1-294/+297
2024-03-28WIP Beginning working on better errors: began replacing raise (Failure) and a...Escherichia1-306/+307
2024-03-20Improve the generation of pretty name and the micro passesSon Ho1-9/+59
2024-03-18Make good progress on adding generics to global constantsSon Ho1-4/+43
2024-03-17Update following changes in CharonSon Ho1-17/+11
2024-03-08Fix some issuesSon Ho1-9/+9
2024-03-08Add some commentsSon Ho1-2/+5
2024-03-08Fix a last issueSon Ho1-51/+107
2024-03-08Fix an issue with the loopsSon Ho1-1/+7
2024-03-08Make progress on fixing the loopsSon Ho1-16/+23
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-22 19:39:57 +0000