summaryrefslogtreecommitdiff
path: root/src/main.ml (follow)
Commit message (Collapse)AuthorAgeFilesLines
* adapt to new LLBC (without OperandConstantValue)Sidney Congard2022-06-231-15/+15
|
* concrete & symbolic evaluation work with new LLBC formatSidney Congard2022-06-211-15/+15
|
* Add an option to eagerly end abstractions if a function has return typeSon Ho2022-05-061-0/+1
| | | | unit and the abstractions don't contain loans
* Make minor modificationsSon Ho2022-05-041-1/+1
|
* Fix some issues when using statesSon Ho2022-05-041-1/+2
|
* Make progress updating the codeSon Ho2022-05-041-6/+1
|
* Make minor updatesSon Ho2022-04-271-1/+0
|
* Cleanup and update commentsSon Ho2022-04-211-16/+16
|
* Work on pretty namesSon Ho2022-04-211-16/+16
|
* Change the extension of the serialized files to .llbcSon Ho2022-03-031-1/+1
|
* In fun_id rename the variant Local to RegularSon Ho2022-03-031-1/+2
|
* Rename CfimOfJson to LlbcOfJsonSon Ho2022-03-031-1/+1
|
* Rename CFIM to LLBCSon Ho2022-03-031-4/+4
|
* Update a commentSon Ho2022-03-031-1/+1
|
* Start working on generating code which uses a state-error monadSon Ho2022-02-231-1/+6
|
* Add an option to control the translation to error monad or state-errorSon Ho2022-02-231-4/+9
| | | | monad
* Improve pretty-printing of environments by filtering and grouping valuesSon Ho2022-02-231-1/+1
| | | | which don't need to be printed
* Make the interpreter pop the frame after executing a function body (forSon Ho2022-02-221-1/+1
| | | | testing or synthesis purposes)
* Add an option to deactivate the invariant checksSon Ho2022-02-101-6/+10
|
* Make minor updates to deserializationSon Ho2022-02-101-0/+1
|
* Cleanup a bitSon Ho2022-02-091-10/+10
|
* Implement extration to different filesSon Ho2022-02-091-0/+6
|
* Add more command line arguments for the decrease clausesSon Ho2022-02-091-0/+16
|
* Add logging informationSon Ho2022-02-091-16/+17
|
* Introduce a translation config in Translate.mlSon Ho2022-02-091-5/+11
|
* Update the Makefile so as not to generate and check traces anymoreSon Ho2022-02-091-14/+14
|
* Make minor modificationsSon Ho2022-02-091-5/+5
|
* Implement filtering of useless forward functionsSon Ho2022-02-091-0/+5
|
* Add definitions to Primitives.fst and start on improving/fixing theSon Ho2022-02-091-0/+1
| | | | generated F* file
* Fix some mistakes in the type conversion to pureSon Ho2022-02-081-0/+2
|
* Add an option to allow the presence of bottom values below borrowsSon Ho2022-02-081-1/+2
|
* Fix more issuesSon Ho2022-02-081-4/+4
|
* Implement pre-passes to update the AST before executing the interpreterSon Ho2022-02-081-0/+3
|
* Make a minor modifications to Makefile and main.mlSon Ho2022-02-081-2/+2
|
* Fix some issuesSon Ho2022-02-081-1/+1
|
* Make progress on implementing support for types and functions likeSon Ho2022-02-081-2/+11
| | | | Option and Vec
* Improve the command line argumentsSon Ho2022-02-041-21/+57
|
* Work on decomposition of monadic let-bindings for F*Son Ho2022-02-041-1/+2
|
* Make the micro passes config a parameter of Translate.translate_moduleSon Ho2022-02-041-1/+9
|
* Add generation of unit tests for the synthesized functionsSon Ho2022-02-041-1/+2
|
* Make minor modifications with regards to loggingSon Ho2022-02-041-0/+1
|
* Deactivate some logsSon Ho2022-02-041-4/+4
|
* Cleanup a bitSon Ho2022-02-031-3/+0
|
* Start generating code for type definitionsSon Ho2022-02-021-3/+1
|
* Rename ExtractToFstar to ExtractToFStarSon Ho2022-01-291-1/+1
|
* Start working on extraction to F*Son Ho2022-01-291-0/+1
|
* Start working on ExtractAstSon Ho2022-01-281-0/+1
|
* Make a lot of small modificationsSon Ho2022-01-281-0/+1
|
* Move some definitions from SymbolicToPure to PureToExtractSon Ho2022-01-271-1/+1
|
* Add more printing facilities and fix minor bugsSon Ho2022-01-271-1/+3
|
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-27 09:02:39 +0000