summaryrefslogtreecommitdiff
path: root/src/InterpreterExpansion.ml (follow)
Commit message (Collapse)AuthorAgeFilesLines
* Implement greedy expansion of symbolic variables and expansion beforeSon Ho2022-01-141-30/+1
| | | | copy
* Start working on greedy symbolic value expansion and expansion beforeSon Ho2022-01-141-14/+118
| | | | assignment
* Update aproj to make AEndedProjLoans take an `aproj option` and add theSon Ho2022-01-141-7/+46
| | | | AIgnoredProjBorrows variant
* Introduce ended borrow/loan projectors over symbolic valuesSon Ho2022-01-131-0/+2
|
* Add an optional borrow identifier to AIgnoredMutBorrow, introduce theSon Ho2022-01-071-10/+12
| | | | AEndedIgnoredMutBorrow variant and fix a couple of bugs
* Improve logging and introduce eval_operands_prepareSon Ho2022-01-071-0/+13
|
* CleanupSon Ho2022-01-061-2/+1
|
* Make the symbolic, borrow, region and abstration counters global andSon Ho2022-01-061-37/+28
| | | | stateful
* Remove the symbolic_proj_comp def and make the set of ended regions aSon Ho2022-01-061-45/+32
| | | | field in the eval_ctx struct
* Fix some issues when evaluating assertionsSon Ho2022-01-061-0/+2
|
* Cleanup a bit more the dependencies and activate more warnings/errorsSon Ho2022-01-061-1/+0
|
* Cleanup the dependencies a bitSon Ho2022-01-061-3/+0
|
* Move some functions from Interpreter to InterpreterExpansionSon Ho2022-01-061-0/+490