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