summaryrefslogtreecommitdiff
path: root/compiler/LlbcAstUtils.ml (unfollow)
Commit message (Expand)AuthorFilesLines
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