summaryrefslogtreecommitdiff
path: root/src/Values.ml (follow)
Commit message (Expand)AuthorAgeFilesLines
* Reorganize a bit the projectSon Ho2022-10-271-844/+0
* Update the code documentation to fix links and syntax issuesSon Ho2022-10-261-196/+198
* Reformat the project with duneSon Ho2022-09-221-1/+1
* Corrected translation without using functions, remaining bug in hashmap trans...Sidney Congard2022-08-101-0/+1
* Add `can_end` in `abs` and use it for the return abs when generating theSon Ho2022-06-271-16/+11
* Add an option to eagerly end abstractions if a function has return typeSon Ho2022-05-061-1/+1
* Cleanup and update commentsSon Ho2022-04-211-0/+10
* Improve the generation of names for given back valuesSon Ho2022-04-211-1/+5
* Work on pretty namesSon Ho2022-04-211-15/+5
* Add commentsSon Ho2022-04-201-0/+7
* Introduce mdplace to link meta information about the given back valuesSon Ho2022-04-201-5/+9
* Make minor cleaningSon Ho2022-01-291-0/+2
* Introduce AEndedSharedBorrow so as not to introduce ABottom whenSon Ho2022-01-271-0/+4
* Add a meta-value in SharedBorrow to carry the shared valueSon Ho2022-01-261-16/+38
* Replace other occurrences of mvalue with msymbolic_valueSon Ho2022-01-261-2/+8
* Replace another occurrence of mvalue with msymbolic_valueSon Ho2022-01-251-1/+1
* Use msymbolic_value instead of mvalue in some places in Values.aprojSon Ho2022-01-251-6/+2
* Start working on typed_avalue_to_consumedSon Ho2022-01-251-1/+7
* Make the back_id field non optional in Values.absSon Ho2022-01-251-6/+7
* Add a SynthInputGivenBack case in Values.sv_kindSon Ho2022-01-251-2/+2
* Make progress on SymbolicToPure.translate_end_abstractionSon Ho2022-01-251-1/+7
* Replace BackwardFunctionId with RegionGroupIdSon Ho2022-01-251-3/+1
* Start working on translate_end_abstractionSon Ho2022-01-251-4/+6
* Start working on printing for symbolic ASTSon Ho2022-01-241-1/+15
* Start working on the generation of the symbolic ASTSon Ho2022-01-211-0/+28
* Update AProjLoans and AEndedProjLoans to take a list of given backSon Ho2022-01-211-18/+52
* Start storing meta-values in the avalues, for synthesis purposesSon Ho2022-01-191-23/+63
* Implement the sanity checks for consumption of symbolic values bySon Ho2022-01-191-0/+4
* Introduce abs_kind, to keep track of abstractions' originsSon Ho2022-01-151-0/+10
* Add sv_kind ("symbolic value kind") to track the origin of the symbolicSon Ho2022-01-151-1/+27
* Use the new collectionsSon Ho2022-01-151-5/+5
* Improve printing of symbolic values in abstractionsSon Ho2022-01-141-3/+3
* Update aproj to make AEndedProjLoans take an `aproj option` and add theSon Ho2022-01-141-13/+44
* Make good progress on end_proj_loans_symbolicSon Ho2022-01-131-0/+1
* Update the projectors to ignore values when they don't contain regionsSon Ho2022-01-131-2/+5
* Introduce "AIgnore" for the avaluesSon Ho2022-01-131-0/+1
* Introduce ended borrow/loan projectors over symbolic valuesSon Ho2022-01-131-0/+2
* Make minor modificationsSon Ho2022-01-121-1/+1
* Factorize initialize_symbolic_context_for_fun andSon Ho2022-01-071-1/+2
* Add a high-level commentSon Ho2022-01-071-0/+8
* Add an optional borrow identifier to AIgnoredMutBorrow, introduce theSon Ho2022-01-071-6/+41
* Remove the symbolic_proj_comp def and make the set of ended regions aSon Ho2022-01-061-35/+10
* Fix some bugsSon Ho2022-01-061-1/+5
* Generate iterators for statementSon Ho2022-01-061-4/+4
* Finish implementing eval_local_function_call_symbolicSon Ho2022-01-051-3/+0
* Make good progress on eval_local_function_call_symbolicSon Ho2022-01-051-1/+1
* Update some commentsSon Ho2022-01-051-0/+4
* Add comments about symbolic valuesSon Ho2022-01-051-2/+5
* Start working on invariant checkingSon Ho2022-01-041-4/+4
* Add a sanity check to make sure symbolic values disappear afterSon Ho2022-01-041-2/+10