summaryrefslogtreecommitdiff
path: root/src/InterpreterBorrows.ml (follow)
Commit message (Collapse)AuthorAgeFilesLines
* 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
* Fix more bugsSon Ho2022-01-061-2/+8
|
* Move more definitions and do more cleanupSon Ho2022-01-061-0/+1
|
* Cleanup and reorganizeSon Ho2022-01-061-0/+1
|
* Cleanup a bit more the dependencies and activate more warnings/errorsSon Ho2022-01-061-4/+0
|
* Cleanup the dependencies a bitSon Ho2022-01-061-4/+0
|
* Move some functions from Interpreter to InterpreterBorrowsSon Ho2022-01-061-0/+1115
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 19:50:45 +0000