summaryrefslogtreecommitdiff
path: root/src/SymbolicToPure.ml (follow)
Commit message (Expand)AuthorAgeFilesLines
* Apply minor changes from PR commentsSidney Congard2022-07-251-2/+10
* Address much stuff of the PR, throw exceptions at remaining placesSidney Congard2022-07-181-10/+13
* Merge branch 'main' of github.com:Kachoc/aeneas into constants-v2Sidney Congard2022-06-301-1/+1
|\
| * Take failing rvalues into account in FunsAnalysis.analyze_fun_declsSon Ho2022-06-301-1/+4
* | Traduct globals body separately (WIP)Sidney Congard2022-06-301-5/+9
* | concrete & symbolic evaluation work with new LLBC formatSidney Congard2022-06-211-12/+15
* | read globals from LLBC JSON into functionsSidney Congard2022-06-081-0/+1
|/
* Treat integer casts in a general mannerSon Ho2022-05-151-0/+6
* Update the translation so that we use a state only in the functionsSon Ho2022-05-051-21/+28
* Start implementing divergence, can_fail, statefullness analysesSon Ho2022-05-041-1/+11
* Make minor modificationsSon Ho2022-05-041-7/+5
* Make minor modificationsSon Ho2022-05-041-24/+3
* Fix more issuesSon Ho2022-05-041-17/+9
* Fix some issues when using statesSon Ho2022-05-041-70/+79
* Make progress updating the codeSon Ho2022-05-041-3/+8
* Start updating the way the function return type (with errors and states)Son Ho2022-05-041-111/+204
* Move the type-checking functions for pure AST to PureTypeCheck.mlSon Ho2022-05-011-4/+4
* Do more cleanupSon Ho2022-05-011-6/+6
* CleanupSon Ho2022-05-011-3/+1
* Perform more renamingsSon Ho2022-05-011-3/+3
* Perform some renamingsSon Ho2022-05-011-8/+8
* Rename "lvalue" to "pattern"Son Ho2022-05-011-35/+37
* Make more progress propagating the changesSon Ho2022-04-291-1/+1
* Make good progress updating the codeSon Ho2022-04-291-138/+151
* Merge the rvalues with the expressionsSon Ho2022-04-291-2/+6
* Make a minor modificationSon Ho2022-04-271-1/+3
* Fix various bugs when extracting with a state monadSon Ho2022-04-271-24/+50
* Make more progressSon Ho2022-04-271-2/+2
* Introduce the Abs expression and continue updating the codeSon Ho2022-04-261-15/+93
* Introduce the App expression, and make progress updating the codeSon Ho2022-04-261-7/+12
* Cleanup and update commentsSon Ho2022-04-211-3/+1
* Improve the generation of names for given back valuesSon Ho2022-04-211-5/+11
* Work on pretty namesSon Ho2022-04-211-25/+17
* Introduce mdplace to link meta information about the given back valuesSon Ho2022-04-201-17/+28
* In fun_id rename the variant Local to RegularSon Ho2022-03-031-2/+2
* Update SymbolicToPure and TranslateSon Ho2022-03-031-1/+1
* Make good progress on adding support for external and opaqueSon Ho2022-03-031-26/+34
* Rename CFIM to LLBCSon Ho2022-03-031-19/+19
* Add an Opaque variant to type_decl_kind and start updating the codeSon Ho2022-03-031-3/+5
* Rename TypeDef...,type_def...,FunDef,fun_def to ...Decl,...declSon Ho2022-03-031-42/+42
* Update the way function names are handledSon Ho2022-02-241-1/+1
* Finish writing the code which generates the state-error monadSon Ho2022-02-241-0/+3
* Implement filtering of useless forward functionsSon Ho2022-02-091-40/+63
* Add definitions to Primitives.fst and start on improving/fixing theSon Ho2022-02-091-5/+1
* Fix some mistakes in the type conversion to pureSon Ho2022-02-081-11/+33
* Add type checking utilities for the pure ADTSon Ho2022-02-081-61/+92
* Start adding more assumed types and functionsSon Ho2022-02-081-13/+37
* Merge the switches over integers and the matches over enumerations inSon Ho2022-02-041-7/+14
* Update SymbolicToPure so that we don't construct tuples with exactly oneSon Ho2022-02-041-24/+21
* Fix a small issue with the types of tuple values inSon Ho2022-02-041-14/+39
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-26 19:02:17 +0000