summaryrefslogtreecommitdiff
path: root/src/InterpreterBorrows.ml (unfollow)
Commit message (Expand)AuthorFilesLines
2022-04-21Improve the generation of names for given back valuesSon Ho1-2/+2
2022-04-21Work on pretty namesSon Ho1-5/+3
2022-04-20Introduce mdplace to link meta information about the given back valuesSon Ho1-6/+8
2022-02-08Add an option to allow the presence of bottom values below borrowsSon Ho1-0/+15
2022-01-28Make a lot of small modificationsSon Ho1-0/+3
2022-01-27Introduce AEndedSharedBorrow so as not to introduce ABottom whenSon Ho1-7/+9
2022-01-27Make give_back_symbolic_value fail in case we need to reinsert inside anSon Ho1-2/+14
2022-01-27Implement the borrow_content case of end_abstraction_borrowsSon Ho1-5/+31
2022-01-26Fix a small issue in end_abstraction_loans: the loan_content case wasSon Ho1-0/+13
2022-01-26Fix a bug in the end borrows/abs loop detectionSon Ho1-4/+4
2022-01-26Fix various issuesSon Ho1-0/+1
2022-01-26Add a meta-value in SharedBorrow to carry the shared valueSon Ho1-2/+2
2022-01-26Replace other occurrences of mvalue with msymbolic_valueSon Ho1-4/+7
2022-01-25Replace another occurrence of mvalue with msymbolic_valueSon Ho1-3/+1
2022-01-25Use msymbolic_value instead of mvalue in some places in Values.aprojSon Ho1-1/+1
2022-01-25Add a SynthInputGivenBack case in Values.sv_kindSon Ho1-4/+11
2022-01-21Finish updating the calls to the synthesis functions to generate theSon Ho1-10/+20
2022-01-21Add invariant checks at the end of [end_borrow] and [end_abstraction]Son Ho1-5/+13
2022-01-21Update AProjLoans and AEndedProjLoans to take a list of given backSon Ho1-93/+126
2022-01-20Cleanup a bit InterpreterBorrowsSon Ho1-22/+14
2022-01-19Make minor updates to InterpreterBorrows and InterpreterExpansionSon Ho1-6/+10
2022-01-19Make minor modificationsSon Ho1-3/+2
2022-01-19Start updating the interpreter to make it CPSSon Ho1-115/+182
2022-01-19Start storing meta-values in the avalues, for synthesis purposesSon Ho1-153/+156
2022-01-19Implement ty_has_borrow_under_mutSon Ho1-1/+1
2022-01-19Implement the sanity checks for consumption of symbolic values bySon Ho1-6/+31
2022-01-18Update the types and deserialization following charon's updatesSon Ho1-2/+5
2022-01-15Add sv_kind ("symbolic value kind") to track the origin of the symbolicSon Ho1-4/+4
2022-01-15Use the new collectionsSon Ho1-3/+3
2022-01-14Fix give_back_symbolic_valueSon Ho1-10/+11
2022-01-14Implement greedy expansion of symbolic variables and expansion beforeSon Ho1-0/+2
2022-01-14Implement loop detection when ending borrows/abstractionsSon Ho1-39/+45
2022-01-14Fix compilation errorsSon Ho1-3/+3
2022-01-14Implement give_back_symbolic_valueSon Ho1-13/+18
2022-01-14Make a minor modificationSon Ho1-6/+5
2022-01-14Update aproj to make AEndedProjLoans take an `aproj option` and add theSon Ho1-15/+33
2022-01-14Make good progress on end_proj_loans_symbolicSon Ho1-8/+51
2022-01-13Make good progress on end_proj_loans_symbolicSon Ho1-5/+27
2022-01-13Update the projectors to ignore values when they don't contain regionsSon Ho1-1/+2
2022-01-13Introduce "AIgnore" for the avaluesSon Ho1-1/+2
2022-01-13Introduce ended borrow/loan projectors over symbolic valuesSon Ho1-38/+47
2022-01-13Start working on checking proj_loans over symbolic values when endingSon Ho1-13/+42
2022-01-12Remove the inner_outer parameter from end_borrow, etc.Son Ho1-34/+25
2022-01-12Update end_borrow to check if there are loans in borrowed valuesSon Ho1-46/+140
2022-01-07Make more modifications to loggingSon Ho1-1/+1
2022-01-07Add an optional borrow identifier to AIgnoredMutBorrow, introduce theSon Ho1-14/+86
2022-01-07Add logging information for borrowsSon Ho1-1/+28
2022-01-06CleanupSon Ho1-2/+1
2022-01-06Make the symbolic, borrow, region and abstration counters global andSon Ho1-5/+4
2022-01-06Remove the symbolic_proj_comp def and make the set of ended regions aSon Ho1-68/+12
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-26 05:15:23 +0000