summaryrefslogtreecommitdiff
path: root/compiler/Values.ml (unfollow)
Commit message (Expand)AuthorFilesLines
2023-02-03Make good progress on updating SymbolicToPureSon Ho1-1/+10
2023-02-03Make progress on Interpreter.mlSon Ho1-1/+4
2023-02-03Merge loop abs so that there is one abs per function input region groupSon Ho1-5/+25
2023-02-03Update the comments in Values and make minor modificationsSon Ho1-88/+134
2023-02-03Remove the meta-value field from AMutBorrowSon Ho1-12/+1
2023-02-03Update a commentSon Ho1-1/+4
2023-02-03Remove the APrimitive variant from the avaluesSon Ho1-13/+0
2023-02-03Remove the meta-values from the shared and reserved borrow valuesSon Ho1-27/+6
2023-02-03Improve the value visitors and some substitution functionsSon Ho1-12/+46
2023-02-03Make progress on the environment matchesSon Ho1-5/+24
2023-02-03Make progress on environment matches and joinsSon Ho1-0/+2
2023-02-03Make progress on environments matches and joinsSon Ho1-22/+66
2023-02-03Start implementing support for loopsSon Ho1-73/+137
2022-11-14Make good progress on the Coq backendSon Ho1-0/+1
2022-11-07Update some commentsSon Ho1-13/+13
2022-11-07Rename "inactivated borrows" to "reserved borrows"Son Ho1-11/+11
2022-10-28Move some files to the Charon projectSon Ho1-1/+1
2022-10-27Move constant_value to PrimitiveValues.mlSon Ho1-37/+12
2022-10-27Reorganize a bit the projectSon Ho1-0/+0
2022-10-26Update the code documentation to fix links and syntax issuesSon Ho1-196/+198
2022-09-22Reformat the project with duneSon Ho1-1/+1
2022-08-10Corrected translation without using functions, remaining bug in hashmap trans...Sidney Congard1-0/+1
2022-06-27Add `can_end` in `abs` and use it for the return abs when generating theSon Ho1-16/+11
2022-05-06Add an option to eagerly end abstractions if a function has return typeSon Ho1-1/+1
2022-04-21Cleanup and update commentsSon Ho1-0/+10
2022-04-21Improve the generation of names for given back valuesSon Ho1-1/+5
2022-04-21Work on pretty namesSon Ho1-15/+5
2022-04-20Add commentsSon Ho1-0/+7
2022-04-20Introduce mdplace to link meta information about the given back valuesSon Ho1-5/+9
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
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-28 13:42:41 +0000