summaryrefslogtreecommitdiff
path: root/src/Values.ml (unfollow)
Commit message (Expand)AuthorFilesLines
2022-01-29Make minor cleaningSon Ho1-0/+2
2022-01-27Introduce AEndedSharedBorrow so as not to introduce ABottom whenSon Ho1-0/+4
2022-01-26Add a meta-value in SharedBorrow to carry the shared valueSon Ho1-16/+38
2022-01-26Replace other occurrences of mvalue with msymbolic_valueSon Ho1-2/+8
2022-01-25Replace another occurrence of mvalue with msymbolic_valueSon Ho1-1/+1
2022-01-25Use msymbolic_value instead of mvalue in some places in Values.aprojSon Ho1-6/+2
2022-01-25Start working on typed_avalue_to_consumedSon Ho1-1/+7
2022-01-25Make the back_id field non optional in Values.absSon Ho1-6/+7
2022-01-25Add a SynthInputGivenBack case in Values.sv_kindSon Ho1-2/+2
2022-01-25Make progress on SymbolicToPure.translate_end_abstractionSon Ho1-1/+7
2022-01-25Replace BackwardFunctionId with RegionGroupIdSon Ho1-3/+1
2022-01-25Start working on translate_end_abstractionSon Ho1-4/+6
2022-01-24Start working on printing for symbolic ASTSon Ho1-1/+15
2022-01-21Start working on the generation of the symbolic ASTSon Ho1-0/+28
2022-01-21Update AProjLoans and AEndedProjLoans to take a list of given backSon Ho1-18/+52
2022-01-19Start storing meta-values in the avalues, for synthesis purposesSon Ho1-23/+63
2022-01-19Implement the sanity checks for consumption of symbolic values bySon Ho1-0/+4
2022-01-15Introduce abs_kind, to keep track of abstractions' originsSon Ho1-0/+10
2022-01-15Add sv_kind ("symbolic value kind") to track the origin of the symbolicSon Ho1-1/+27
2022-01-15Use the new collectionsSon Ho1-5/+5
2022-01-14Improve printing of symbolic values in abstractionsSon Ho1-3/+3
2022-01-14Update aproj to make AEndedProjLoans take an `aproj option` and add theSon Ho1-13/+44
2022-01-13Make good progress on end_proj_loans_symbolicSon Ho1-0/+1
2022-01-13Update the projectors to ignore values when they don't contain regionsSon Ho1-2/+5
2022-01-13Introduce "AIgnore" for the avaluesSon Ho1-0/+1
2022-01-13Introduce ended borrow/loan projectors over symbolic valuesSon Ho1-0/+2
2022-01-12Make minor modificationsSon Ho1-1/+1
2022-01-07Factorize initialize_symbolic_context_for_fun andSon Ho1-1/+2
2022-01-07Add a high-level commentSon Ho1-0/+8
2022-01-07Add an optional borrow identifier to AIgnoredMutBorrow, introduce theSon Ho1-6/+41
2022-01-06Remove the symbolic_proj_comp def and make the set of ended regions aSon Ho1-35/+10
2022-01-06Fix some bugsSon Ho1-1/+5
2022-01-06Generate iterators for statementSon Ho1-4/+4
2022-01-05Finish implementing eval_local_function_call_symbolicSon Ho1-3/+0
2022-01-05Make good progress on eval_local_function_call_symbolicSon Ho1-1/+1
2022-01-05Update some commentsSon Ho1-0/+4
2022-01-05Add comments about symbolic valuesSon Ho1-2/+5
2022-01-04Start working on invariant checkingSon Ho1-4/+4
2022-01-04Add a sanity check to make sure symbolic values disappear afterSon Ho1-2/+10
2022-01-04Fix a few mistakes with symbolic values and their typesSon Ho1-1/+9
2022-01-04Update expand_symbolic_value_shared_borrow to reborrow also in theSon Ho1-1/+3
2022-01-04Fix a few issues with [apply_symbolic_expansion_to_avalues]Son Ho1-0/+2
2022-01-03Update the functions to activate inactivated borrowsSon Ho1-5/+20
2022-01-03Make progress on end_abstraction_borrows and start implementingSon Ho1-1/+16
2022-01-03Start implementing end_abstraction_borrowSon Ho1-1/+2
2022-01-03Replace AProjSharedLoan with AIgnoredSharedLoanSon Ho1-2/+1
2022-01-03Add detailed comments to aloan_content and aborrow_contentSon Ho1-17/+200
2021-12-17Add a commentSon Ho1-1/+2
2021-12-17Rename AIgnoredShared{Borrow,Loan} to AProjShared{Borrow,Loan}Son Ho1-4/+4
2021-12-17Implement apply_reborrowsSon Ho1-1/+2