summaryrefslogtreecommitdiff
path: root/compiler/LlbcAstUtils.ml (unfollow)
Commit message (Expand)AuthorFilesLines
2023-10-23Remove some assumed types and add more support for builtin definitionsSon Ho1-4/+4
2023-09-17Fix more issues with the extractionSon Ho1-4/+13
2023-09-07Map some globals like u32::MAX to standard definitionsSon Ho1-0/+20
2022-10-28Move some files to the Charon projectSon Ho1-60/+1
2022-10-27Reorganize a bit the projectSon Ho1-0/+0
2022-10-26Update the code documentation to fix links and syntax issuesSon Ho1-3/+3
2022-06-27Add `can_end` in `abs` and use it for the return abs when generating theSon Ho1-1/+2
2022-06-21concrete & symbolic evaluation work with new LLBC formatSidney Congard1-1/+0
2022-06-08read globals from LLBC JSON into functionsSidney Congard1-0/+1
2022-03-03In fun_id rename the variant Local to RegularSon Ho1-2/+2
2022-03-03Make good progress on adding support for external and opaqueSon Ho1-4/+7
2022-03-03Rename CFIM to LLBCSon Ho1-1/+1
2022-03-03Move the names from Identifiers to NamesSon Ho1-1/+1
2022-03-03Rename TypeDef...,type_def...,FunDef,fun_def to ...Decl,...declSon Ho1-7/+7
2022-02-24Update the way function names are handledSon Ho1-1/+1
2022-02-09Add definitions to Primitives.fst and start on improving/fixing theSon Ho1-10/+2
2022-01-29Make progress on PureToExtractSon Ho1-0/+10
2022-01-28Make minor modificationsSon Ho1-0/+10
2022-01-27Fix some issues with the naming of input variablesSon Ho1-0/+4
2022-01-27Fix a small issue in translate_back_tySon Ho1-0/+2
2022-01-26Make progress on translationSon Ho1-0/+32
2022-01-06Make good progress on implementing utilities to test symbolic executionSon Ho1-1/+4
2022-01-06Implement statement_has_loops and make minor modificationsSon Ho1-0/+16
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-29 15:19:18 +0000