summaryrefslogtreecommitdiff
path: root/src/main.ml (unfollow)
Commit message (Expand)AuthorFilesLines
2022-02-03Cleanup a bitSon Ho1-3/+0
2022-02-02Start generating code for type definitionsSon Ho1-3/+1
2022-01-29Rename ExtractToFstar to ExtractToFStarSon Ho1-1/+1
2022-01-29Start working on extraction to F*Son Ho1-0/+1
2022-01-28Start working on ExtractAstSon Ho1-0/+1
2022-01-28Make a lot of small modificationsSon Ho1-0/+1
2022-01-27Move some definitions from SymbolicToPure to PureToExtractSon Ho1-1/+1
2022-01-27Add more printing facilities and fix minor bugsSon Ho1-1/+3
2022-01-27Make minor modifications and add commentsSon Ho1-1/+4
2022-01-27Start testing translation to pureSon Ho1-3/+7
2022-01-27Cleanup a bit by removing useless `open`Son Ho1-2/+0
2022-01-27Implement Translate.translate_functionSon Ho1-0/+1
2022-01-27Implement the borrow_content case of end_abstraction_borrowsSon Ho1-1/+1
2022-01-26Fix various issuesSon Ho1-2/+2
2022-01-26Test the generation of the symbolic ASTSon Ho1-1/+1
2022-01-26Start working on signatures for the assumed functionsSon Ho1-1/+1
2022-01-26Fix a typoSon Ho1-1/+1
2022-01-26Remove SymbolicAstUtils.mlSon Ho1-1/+0
2022-01-25Implement SymbolicToPure.translate_fun_sigSon Ho1-1/+2
2022-01-24Start working on name generation for the synthesisSon Ho1-0/+1
2022-01-24Start working on printing for symbolic ASTSon Ho1-0/+2
2022-01-21Add invariant checks at the end of [end_borrow] and [end_abstraction]Son Ho1-1/+1
2022-01-19Start working on Pure.mlSon Ho1-0/+1
2022-01-18Start working on TypesAnalysisSon Ho1-0/+1
2022-01-14Implement greedy expansion of symbolic variables and expansion beforeSon Ho1-1/+2
2022-01-14Start working on greedy symbolic value expansion and expansion beforeSon Ho1-2/+10
2022-01-12Update end_borrow to check if there are loans in borrowed valuesSon Ho1-1/+1
2022-01-07Make more modifications to loggingSon Ho1-2/+5
2022-01-07Add logging information for borrowsSon Ho1-1/+2
2022-01-07Make more improvements to loggingSon Ho1-0/+1
2022-01-07Improve logging and introduce eval_operands_prepareSon Ho1-0/+8
2022-01-06Make minor modificationsSon Ho1-1/+1
2022-01-06Implement tests for the symbolic interpreterSon Ho1-2/+5
2022-01-06Make good progress on implementing utilities to test symbolic executionSon Ho1-1/+1
2022-01-05Cleanup a bitSon Ho1-6/+0
2022-01-05Introduce the type_context definitionSon Ho1-17/+23
2022-01-04one remarkJonathan Protzenko1-1/+2
2021-12-15Parsing of command-line argumentsJonathan Protzenko1-1/+25
2021-12-01Cleanup a bitSon Ho1-1/+1
2021-11-29Start deriving formatters for debuggingSon Ho1-0/+4
2021-11-29Improve formattingSon Ho1-1/+1
2021-11-29Test the unit functionsSon Ho1-1/+5
2021-11-29Debug pretty-printingSon Ho1-1/+1
2021-11-29Fix some issues and start printing modulesSon Ho1-4/+4
2021-11-29Move some definitions from CfimOfJson.ml to a new Modules.mlSon Ho1-0/+4
2021-11-29Start working logging and make progress on printing ASTsSon Ho1-1/+1
2021-11-26Update the env definition to make the frames easier to manipulateSon Ho1-0/+1
2021-11-25Make a minor modificationSon Ho1-1/+0
2021-11-23Activate exception backtraceSon Ho1-0/+5
2021-11-22Implement end_borrow_get_borrow_in_envSon Ho1-3/+1