summaryrefslogtreecommitdiff
path: root/src/InterpreterStatements.ml (follow)
Commit message (Collapse)AuthorAgeFilesLines
* Corrected translation without using functions, remaining bug in hashmap ↵Sidney Congard2022-08-101-13/+4
| | | | translation
* Register global names, one error remainingSidney Congard2022-08-081-2/+6
|
* Create global declaration group, address PR changes but introduce bugsSidney Congard2022-07-291-1/+6
|
* Always put can_fail to true, specialize global traduction to concrete ↵Sidney Congard2022-07-281-9/+16
| | | | function call and symbolic fresh value
* Address much stuff of the PR, throw exceptions at remaining placesSidney Congard2022-07-181-1/+2
|
* Merge branch 'main' of github.com:Kachoc/aeneas into constants-v2Sidney Congard2022-06-301-44/+48
|\ | | | | | | Complete the constants extraction by making all functions fail
| * Add `can_end` in `abs` and use it for the return abs when generating theSon Ho2022-06-271-2/+14
| | | | | | | | backward functions
| * Update eval_operand_prepare to not give a value to the continuationSon Ho2022-06-271-42/+34
| |
* | concrete & symbolic evaluation work with new LLBC formatSidney Congard2022-06-211-4/+12
| |
* | read globals from LLBC JSON into functionsSidney Congard2022-06-081-3/+4
|/
* Add an option to eagerly end abstractions if a function has return typeSon Ho2022-05-061-1/+48
| | | | unit and the abstractions don't contain loans
* Perform some renamingsSon Ho2022-05-011-31/+29
|
* Improve the generation of names for given back valuesSon Ho2022-04-211-5/+8
|
* Fix minor issuesSon Ho2022-03-031-1/+5
|
* In fun_id rename the variant Local to RegularSon Ho2022-03-031-2/+2
|
* Make good progress on adding support for external and opaqueSon Ho2022-03-031-7/+16
| | | | declarations
* Rename CFIM to LLBCSon Ho2022-03-031-1/+1
|
* Rename TypeDef...,type_def...,FunDef,fun_def to ...Decl,...declSon Ho2022-03-031-8/+8
|
* Add support for "fused" match branchesSon Ho2022-02-221-1/+13
|
* Make minor modifications in InterpreterStatementsSon Ho2022-02-091-4/+11
|
* Fix another issue in set_discriminantSon Ho2022-02-081-3/+17
|
* Add an option to allow the presence of bottom values below borrowsSon Ho2022-02-081-0/+17
|
* Fix more issuesSon Ho2022-02-081-23/+36
|
* Make a minor modification to `drop_value`Son Ho2022-02-081-2/+5
|
* Make progress on implementing support for types and functions likeSon Ho2022-02-081-14/+14
| | | | Option and Vec
* Start adding more assumed types and functionsSon Ho2022-02-081-5/+17
|
* Generate meta-information for the assignmentsSon Ho2022-01-281-4/+15
|
* Generate meta-information for assignments in the symbolic ASTSon Ho2022-01-271-17/+21
|
* Rename the meta-places to [mplace] and update some commentsSon Ho2022-01-271-1/+1
|
* Add meta information for the variable names in SymbolicAstSon Ho2022-01-271-8/+19
|
* Implement Translate.translate_functionSon Ho2022-01-271-0/+3
|
* Make good progress on generating the symbolic AST for the backwardSon Ho2022-01-261-18/+56
| | | | functions
* 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
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-19 17:37:14 +0000