summaryrefslogtreecommitdiff
path: root/src/InterpreterBorrows.ml (follow)
Commit message (Collapse)AuthorAgeFilesLines
* 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
| | | | to the information about the input arguments
* 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
| | | | ending shared aborrows
* Make give_back_symbolic_value fail in case we need to reinsert inside anSon Ho2022-01-271-2/+14
| | | | AProjLoans: there is something wrong
* 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
| | | | not implemented
* 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
| | | | symbolic AST
* 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
| | | | values
* 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
| | | | abstractions (as input or given back values)
* 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
| | | | values
* 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
| | | | copy
* 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
| | | | AIgnoredProjBorrows variant
* 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
| | | | of interest
* 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
| | | | abstractions
* 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
| | | | AEndedIgnoredMutBorrow variant and fix a couple of bugs
* 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
| | | | stateful
* Remove the symbolic_proj_comp def and make the set of ended regions aSon Ho2022-01-061-68/+12
| | | | field in the eval_ctx struct
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-26 04:10:12 +0000