summaryrefslogtreecommitdiff
path: root/src/InterpreterUtils.ml (follow)
Commit message (Collapse)AuthorAgeFilesLines
* Add a SynthInputGivenBack case in Values.sv_kindSon Ho2022-01-251-2/+3
|
* Update AProjLoans and AEndedProjLoans to take a list of given backSon Ho2022-01-211-3/+3
| | | | values
* Start storing meta-values in the avalues, for synthesis purposesSon Ho2022-01-191-1/+1
|
* Implement ty_has_borrow_under_mutSon Ho2022-01-191-1/+1
|
* Implement the sanity checks for consumption of symbolic values bySon Ho2022-01-191-0/+22
| | | | abstractions (as input or given back values)
* Remove ty_has_regions and use ty_has_borrows insteadSon Ho2022-01-181-0/+2
|
* Add sv_kind ("symbolic value kind") to track the origin of the symbolicSon Ho2022-01-151-4/+6
| | | | values
* Use the new collectionsSon Ho2022-01-151-2/+2
|
* Implement greedy expansion of symbolic variables and expansion beforeSon Ho2022-01-141-3/+0
| | | | copy
* Fix compilation errorsSon Ho2022-01-141-3/+3
|
* Implement give_back_symbolic_valueSon Ho2022-01-141-0/+8
|
* Update aproj to make AEndedProjLoans take an `aproj option` and add theSon Ho2022-01-141-39/+14
| | | | AIgnoredProjBorrows variant
* Update the projectors to ignore values when they don't contain regionsSon Ho2022-01-131-6/+12
| | | | of interest
* Introduce "AIgnore" for the avaluesSon Ho2022-01-131-0/+1
|
* Introduce ended borrow/loan projectors over symbolic valuesSon Ho2022-01-131-0/+4
|
* Start working on checking proj_loans over symbolic values when endingSon Ho2022-01-131-0/+3
| | | | abstractions
* Fix a small bug in projections_intersect and add more debugging outputSon Ho2022-01-131-43/+0
|
* Update end_borrow to check if there are loans in borrowed valuesSon Ho2022-01-121-0/+8
|
* Introduce dummy variables and update assign_to_placeSon Ho2022-01-121-1/+1
|
* remove another warningJonathan Protzenko2022-01-101-1/+0
|
* Merge remote-tracking branch 'refs/remotes/origin/main'Jonathan Protzenko2022-01-101-10/+11
|\
| * Improve logging and introduce eval_operands_prepareSon Ho2022-01-071-10/+11
| |
* | Merge remote-tracking branch 'refs/remotes/origin/main'Jonathan Protzenko2022-01-061-47/+227
|\|
| * CleanupSon Ho2022-01-061-3/+1
| |
| * Make the symbolic, borrow, region and abstration counters global andSon Ho2022-01-061-4/+3
| | | | | | | | stateful
| * Remove the symbolic_proj_comp def and make the set of ended regions aSon Ho2022-01-061-56/+22
| | | | | | | | field in the eval_ctx struct
| * Fix some bugsSon Ho2022-01-061-0/+2
| |
| * Make minor improvements to printingSon Ho2022-01-061-0/+2
| |
| * Make minor modificationsSon Ho2022-01-061-0/+7
| |
| * Make good progress on implementing utilities to test symbolic executionSon Ho2022-01-061-5/+23
| |
| * Move more definitions and do more cleanupSon Ho2022-01-061-67/+0
| |
| * Cleanup and reorganizeSon Ho2022-01-061-474/+1
| |
| * Cleanup the dependencies a bitSon Ho2022-01-061-2/+0
| |
| * Move some functions from Interpreter to InterpreterExpansionSon Ho2022-01-061-0/+17
| |
| * Move some functions from Interpreter to InterpreterProjectorsSon Ho2022-01-061-0/+160
| |
| * Make progress on eval_non_local_function_call_symbolicSon Ho2022-01-051-1/+7
| |
| * Make progress on implementing the symbolic evaluation for the non-localSon Ho2022-01-051-7/+1
| | | | | | | | function calls
| * Implement eval_unary_op_symbolicSon Ho2022-01-051-0/+5
| |
| * Start inserting calls to dummy synthesis functions in Interpreter.mlSon Ho2022-01-051-0/+7
| |
| * Move some functions from Interpreter to InterpreterUtilsSon Ho2022-01-041-0/+536
| |
* | More compiler warningsJonathan Protzenko2022-01-041-3/+0
|/
* Commit a forgotten fileSon Ho2022-01-041-0/+86
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 19:52:23 +0000