summaryrefslogtreecommitdiff
path: root/src/InterpreterExpressions.ml (follow)
Commit message (Collapse)AuthorAgeFilesLines
* Apply small changes from the PRSidney Congard2022-07-131-4/+5
|
* Merge branch 'main' of github.com:Kachoc/aeneas into constants-v2Sidney Congard2022-06-301-58/+133
|\ | | | | | | Complete the constants extraction by making all functions fail
| * Make minor modificationsSon Ho2022-06-291-1/+24
| |
| * Update eval_operand_prepare to not give a value to the continuationSon Ho2022-06-271-51/+95
| |
* | concrete & symbolic evaluation work with new LLBC formatSidney Congard2022-06-211-64/+19
| |
* | crude generation working - missing unit tests & special constants handlingSidney Congard2022-06-131-51/+63
|/
* Treat integer casts in a general mannerSon Ho2022-05-151-0/+10
|
* Add AggregatedOptionSon Ho2022-05-151-0/+14
|
* Introduce the Abs expression and continue updating the codeSon Ho2022-04-261-1/+1
|
* Improve the generation of names for given back valuesSon Ho2022-04-211-1/+1
|
* Update the evaluation of matches for the cases where the scrutinee is aSon Ho2022-04-201-13/+22
| | | | shared loan
* Rename TypeDef...,type_def...,FunDef,fun_def to ...Decl,...declSon Ho2022-03-031-4/+4
|
* Fix some issuesSon Ho2022-02-081-4/+14
|
* Start adding more assumed types and functionsSon Ho2022-02-081-27/+23
|
* Remove the Aggregated variant from SymbolicAst.meta as it is included inSon Ho2022-01-281-6/+2
| | | | the Assignment variant
* Rename the meta-places to [mplace] and update some commentsSon Ho2022-01-271-2/+3
|
* Add meta information for the variable names in SymbolicAstSon Ho2022-01-271-6/+15
|
* Add a meta-value in SharedBorrow to carry the shared valueSon Ho2022-01-261-15/+16
|
* Finish updating the calls to the synthesis functions to generate theSon Ho2022-01-211-10/+19
| | | | symbolic AST
* Fix a minor issue in expand_symbolic_valueSon Ho2022-01-201-9/+14
|
* Make minor modificationsSon Ho2022-01-201-4/+7
|
* Make good progress on updating InterpreterStatements to use CPSSon Ho2022-01-201-1/+1
|
* Make minor modifications in InterpreterExpressionsSon Ho2022-01-201-6/+3
|
* Finish updating InterpreterExpressionsSon Ho2022-01-201-98/+107
|
* Make more progress on InterpreterExpressionsSon Ho2022-01-201-29/+41
|
* Make more progress on InterpreterExpressionsSon Ho2022-01-201-99/+116
|
* Make progress on converting InterpreterExpressions to CPSSon Ho2022-01-201-102/+140
|
* Make a minor modificationSon Ho2022-01-191-1/+1
|
* Remove ty_has_regions and use ty_has_borrows insteadSon Ho2022-01-181-2/+8
|
* Rename type_is_primitively_copyable to ty_is_...Son Ho2022-01-181-2/+2
|
* Add sv_kind ("symbolic value kind") to track the origin of the symbolicSon Ho2022-01-151-2/+6
| | | | values
* Implement greedy expansion of symbolic variables and expansion beforeSon Ho2022-01-141-17/+55
| | | | copy
* Start working on greedy symbolic value expansion and expansion beforeSon Ho2022-01-141-0/+4
| | | | assignment
* Improve logging and introduce eval_operands_prepareSon Ho2022-01-071-4/+44
|
* Make the symbolic, borrow, region and abstration counters global andSon Ho2022-01-061-4/+4
| | | | stateful
* Remove the symbolic_proj_comp def and make the set of ended regions aSon Ho2022-01-061-3/+3
| | | | field in the eval_ctx struct
* Move more definitions and do more cleanupSon Ho2022-01-061-0/+1
|
* Cleanup the dependencies a bitSon Ho2022-01-061-5/+0
|
* Move some definitionsSon Ho2022-01-061-20/+0
|
* Move some definitions inside of InterpreterExpressionsSon Ho2022-01-061-28/+28
|
* Move some functions from Interpreter to InterpreterExpressionsSon Ho2022-01-061-0/+476
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-27 10:25:02 +0000