summaryrefslogtreecommitdiff
path: root/compiler/Driver.ml (unfollow)
Commit message (Expand)AuthorFilesLines
2023-06-04Consistently use the names TerminationMeasure and DecreasesProofSon Ho1-11/+13
2023-06-04Add more checks in Driver.mlSon Ho1-2/+6
2023-06-04Print warnings for the Lean backend and loopsSon Ho1-8/+13
2023-06-04WIP lots of stuffJonathan Protzenko1-15/+19
2023-06-04Initial Lean backend, WIPJonathan Protzenko1-0/+2
2023-02-03Do not unfold the monadic lets for the generated F* codeSon Ho1-2/+3
2023-02-03Split InterpreterLoops into several filesSon Ho1-0/+3
2023-02-03Make minor modifications and generate code for loopsSon Ho1-24/+28
2023-02-03Remove the meta-value field from AMutBorrowSon Ho1-16/+18
2022-11-16Generate record field projectors for CoqSon Ho1-7/+0
2022-11-14Add a `-use-fuel` optionSon Ho1-0/+8
2022-11-14Implement a pass to decompose nested patterns in let-bindingsSon Ho1-21/+13
2022-11-14Make good progress on the Coq backendSon Ho1-5/+31
2022-11-11Make the Nix build workSon Ho1-3/+4
2022-11-10Implement a Config.ml file which groups all the global options in referencesSon Ho1-63/+21
2022-11-10Implement the generation of stateful backward functions (controlled by an opt...Son Ho1-2/+10
2022-11-07Add some .mli filesSon Ho1-0/+1
2022-10-28Make minor modificationsSon Ho1-1/+1
2022-10-28Make minor updates to account for Charon's changesSon Ho1-1/+1
2022-10-27Rename driver.ml to Driver.mlSon Ho1-0/+0
2022-10-27Reorganize a bit the projectSon Ho1-0/+0
2022-10-26Start generating documentationSon Ho1-8/+11
2022-10-26Measure and display the execution timeSon Ho1-1/+11
2022-10-13Rename Modules to CratesSon Ho1-1/+1
2022-06-23adapt to new LLBC (without OperandConstantValue)Sidney Congard1-15/+15
2022-06-21concrete & symbolic evaluation work with new LLBC formatSidney Congard1-15/+15
2022-05-06Add an option to eagerly end abstractions if a function has return typeSon Ho1-0/+1
2022-05-04Make minor modificationsSon Ho1-1/+1
2022-05-04Fix some issues when using statesSon Ho1-1/+2
2022-05-04Make progress updating the codeSon Ho1-6/+1
2022-04-27Make minor updatesSon Ho1-1/+0
2022-04-21Cleanup and update commentsSon Ho1-16/+16
2022-04-21Work on pretty namesSon Ho1-16/+16
2022-03-03Change the extension of the serialized files to .llbcSon Ho1-1/+1
2022-03-03In fun_id rename the variant Local to RegularSon Ho1-1/+2
2022-03-03Rename CfimOfJson to LlbcOfJsonSon Ho1-1/+1
2022-03-03Rename CFIM to LLBCSon Ho1-4/+4
2022-03-03Update a commentSon Ho1-1/+1
2022-02-23Start working on generating code which uses a state-error monadSon Ho1-1/+6
2022-02-23Add an option to control the translation to error monad or state-errorSon Ho1-4/+9
2022-02-23Improve pretty-printing of environments by filtering and grouping valuesSon Ho1-1/+1
2022-02-22Make the interpreter pop the frame after executing a function body (forSon Ho1-1/+1
2022-02-10Add an option to deactivate the invariant checksSon Ho1-6/+10
2022-02-10Make minor updates to deserializationSon Ho1-0/+1
2022-02-09Cleanup a bitSon Ho1-10/+10
2022-02-09Implement extration to different filesSon Ho1-0/+6
2022-02-09Add more command line arguments for the decrease clausesSon Ho1-0/+16
2022-02-09Add logging informationSon Ho1-16/+17
2022-02-09Introduce a translation config in Translate.mlSon Ho1-5/+11
2022-02-09Update the Makefile so as not to generate and check traces anymoreSon Ho1-14/+14
generated by cgit v1.2.3 (git 2.25.1) at 2025-03-16 13:28:29 +0000