summaryrefslogtreecommitdiff
path: root/src/InterpreterStatements.ml (follow)
Commit message (Collapse)AuthorAgeFilesLines
* Cleanup a bitSon Ho2022-01-261-7/+6
|
* Use the signatures in Assumed.ml in InterpreterStatements and remove theSon Ho2022-01-261-68/+13
| | | | functions which return instantiated signatures for the assumed functions
* Start working on signatures for the assumed functionsSon Ho2022-01-261-1/+2
|
* Make the back_id field non optional in Values.absSon Ho2022-01-251-1/+0
|
* Make progress on SymbolicToPure.translate_end_abstractionSon Ho2022-01-251-1/+5
|
* Replace BackwardFunctionId with RegionGroupIdSon Ho2022-01-251-2/+2
|
* Finish updating the calls to the synthesis functions to generate theSon Ho2022-01-211-11/+9
| | | | symbolic AST
* Start working on the generation of the symbolic ASTSon Ho2022-01-211-3/+17
|
* Make minor modifications for the invariants checksSon Ho2022-01-211-10/+2
|
* Cleanup a bit InterpreterStatements following compiler warningsSon Ho2022-01-201-6/+4
|
* Finish updating InterpreterStatementsSon Ho2022-01-201-85/+101
|
* Make various style modificationsSon Ho2022-01-201-7/+11
|
* Make good progress on updating InterpreterStatements to use CPSSon Ho2022-01-201-443/+546
|
* Implement the sanity checks for consumption of symbolic values bySon Ho2022-01-191-1/+5
| | | | abstractions (as input or given back values)
* Remove ty_has_regions and use ty_has_borrows insteadSon Ho2022-01-181-1/+4
|
* Update the types and deserialization following charon's updatesSon Ho2022-01-181-12/+19
|
* Introduce abs_kind, to keep track of abstractions' originsSon Ho2022-01-151-3/+4
|
* Add sv_kind ("symbolic value kind") to track the origin of the symbolicSon Ho2022-01-151-1/+1
| | | | values
* Use the new collectionsSon Ho2022-01-151-1/+1
|
* Start working on Collections.mlSon Ho2022-01-151-1/+1
|
* Implement greedy expansion of symbolic variables and expansion beforeSon Ho2022-01-141-3/+4
| | | | copy
* Update the TODOsSon Ho2022-01-141-2/+0
|
* Start working on greedy symbolic value expansion and expansion beforeSon Ho2022-01-141-0/+8
| | | | assignment
* Update aproj to make AEndedProjLoans take an `aproj option` and add theSon Ho2022-01-141-1/+3
| | | | AIgnoredProjBorrows variant
* Update the projectors to ignore values when they don't contain regionsSon Ho2022-01-131-2/+2
| | | | of interest
* Make more updates to assignment and update ctx_pop_frameSon Ho2022-01-131-4/+38
|
* Start updating the assignment semanticsSon Ho2022-01-131-4/+8
|
* Update ctx_pop_frame to not drop the local variablesSon Ho2022-01-121-33/+7
|
* Update end_borrow to check if there are loans in borrowed valuesSon Ho2022-01-121-1/+1
|
* Update some commentsSon Ho2022-01-121-4/+7
|
* Introduce dummy variables and update assign_to_placeSon Ho2022-01-121-3/+12
|
* Make minor modificationsSon Ho2022-01-121-0/+4
|
* Factorize initialize_symbolic_context_for_fun andSon Ho2022-01-071-29/+58
| | | | eval_function_call_symbolic_from_inst_sig and make minor modifications
* Make more modifications to loggingSon Ho2022-01-071-6/+9
|
* Add an optional borrow identifier to AIgnoredMutBorrow, introduce theSon Ho2022-01-071-2/+15
| | | | AEndedIgnoredMutBorrow variant and fix a couple of bugs
* Make the symbolic, borrow, region and abstration counters global andSon Ho2022-01-061-7/+5
| | | | stateful
* Remove the symbolic_proj_comp def and make the set of ended regions aSon Ho2022-01-061-19/+10
| | | | field in the eval_ctx struct
* Make a minor modificationSon Ho2022-01-061-1/+3
|
* Fix some issues when evaluating assertionsSon Ho2022-01-061-6/+48
|
* Make minor modificationsSon Ho2022-01-061-6/+7
|
* Implement tests for the symbolic interpreterSon Ho2022-01-061-1/+1
|
* Make good progress on implementing utilities to test symbolic executionSon Ho2022-01-061-45/+56
|
* Cleanup the dependencies a bitSon Ho2022-01-061-4/+0
|
* Move some definitionsSon Ho2022-01-061-0/+20
|
* Move some definitions from Interpreter to InterpreterStatementsSon Ho2022-01-061-0/+894
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 16:02:37 +0000