summaryrefslogtreecommitdiff
path: root/src/InterpreterUtils.ml (unfollow)
Commit message (Expand)AuthorFilesLines
2022-09-22Reformat the project with duneSon Ho1-16/+2
2022-08-10Corrected translation without using functions, remaining bug in hashmap trans...Sidney Congard1-2/+2
2022-06-21concrete & symbolic evaluation work with new LLBC formatSidney Congard1-2/+0
2022-04-21Improve the generation of names for given back valuesSon Ho1-0/+10
2022-03-03Rename CFIM to LLBCSon Ho1-2/+2
2022-02-08Add an option to allow the presence of bottom values below borrowsSon Ho1-0/+2
2022-02-08Implement pre-passes to update the AST before executing the interpreterSon Ho1-2/+0
2022-02-08Fix some issuesSon Ho1-0/+2
2022-01-25Add a SynthInputGivenBack case in Values.sv_kindSon Ho1-2/+3
2022-01-21Update AProjLoans and AEndedProjLoans to take a list of given backSon Ho1-3/+3
2022-01-19Start storing meta-values in the avalues, for synthesis purposesSon Ho1-1/+1
2022-01-19Implement ty_has_borrow_under_mutSon Ho1-1/+1
2022-01-19Implement the sanity checks for consumption of symbolic values bySon Ho1-0/+22
2022-01-18Remove ty_has_regions and use ty_has_borrows insteadSon Ho1-0/+2
2022-01-15Add sv_kind ("symbolic value kind") to track the origin of the symbolicSon Ho1-4/+6
2022-01-15Use the new collectionsSon Ho1-2/+2
2022-01-14Implement greedy expansion of symbolic variables and expansion beforeSon Ho1-3/+0
2022-01-14Fix compilation errorsSon Ho1-3/+3
2022-01-14Implement give_back_symbolic_valueSon Ho1-0/+8
2022-01-14Update aproj to make AEndedProjLoans take an `aproj option` and add theSon Ho1-39/+14
2022-01-13Update the projectors to ignore values when they don't contain regionsSon Ho1-6/+12
2022-01-13Introduce "AIgnore" for the avaluesSon Ho1-0/+1
2022-01-13Introduce ended borrow/loan projectors over symbolic valuesSon Ho1-0/+4
2022-01-13Start working on checking proj_loans over symbolic values when endingSon Ho1-0/+3
2022-01-13Fix a small bug in projections_intersect and add more debugging outputSon Ho1-43/+0
2022-01-12Update end_borrow to check if there are loans in borrowed valuesSon Ho1-0/+8
2022-01-12Introduce dummy variables and update assign_to_placeSon Ho1-1/+1
2022-01-10remove another warningJonathan Protzenko1-1/+0
2022-01-07Improve logging and introduce eval_operands_prepareSon Ho1-10/+11
2022-01-06CleanupSon Ho1-3/+1
2022-01-06Make the symbolic, borrow, region and abstration counters global andSon Ho1-4/+3
2022-01-06Remove the symbolic_proj_comp def and make the set of ended regions aSon Ho1-56/+22
2022-01-06Fix some bugsSon Ho1-0/+2
2022-01-06Make minor improvements to printingSon Ho1-0/+2
2022-01-06Make minor modificationsSon Ho1-0/+7
2022-01-06Make good progress on implementing utilities to test symbolic executionSon Ho1-5/+23
2022-01-06Move more definitions and do more cleanupSon Ho1-67/+0
2022-01-06Cleanup and reorganizeSon Ho1-474/+1
2022-01-06Cleanup the dependencies a bitSon Ho1-2/+0
2022-01-06Move some functions from Interpreter to InterpreterExpansionSon Ho1-0/+17
2022-01-06Move some functions from Interpreter to InterpreterProjectorsSon Ho1-0/+160
2022-01-05Make progress on eval_non_local_function_call_symbolicSon Ho1-1/+7
2022-01-05Make progress on implementing the symbolic evaluation for the non-localSon Ho1-7/+1
2022-01-05Implement eval_unary_op_symbolicSon Ho1-0/+5
2022-01-05Start inserting calls to dummy synthesis functions in Interpreter.mlSon Ho1-0/+7
2022-01-04Move some functions from Interpreter to InterpreterUtilsSon Ho1-0/+536
2022-01-04More compiler warningsJonathan Protzenko1-3/+0
2022-01-04Commit a forgotten fileSon Ho1-0/+86