summaryrefslogtreecommitdiff
path: root/compiler/Main.ml (unfollow)
Commit message (Expand)AuthorFilesLines
2023-12-05Print error messages when the command line arguments are invalidSon Ho1-10/+40
2023-11-27Do not activate the sanity (invariant) checks by defaultSon Ho1-4/+4
2023-11-21Reorganize the "Extract" filesSon Ho1-1/+4
2023-11-20Fix minor issuesSon Ho1-0/+1
2023-11-16Rename Driver.ml to Main.mlSon Ho1-0/+0
2023-11-16Finish propagating the changes to the names and cleaningSon Ho1-12/+9
2023-11-13Make minor modificationsSon Ho1-0/+1
2023-11-09Modify some options and update the MakefileSon Ho1-7/+7
2023-11-09Fix a small issue in AssociatedTypesSon Ho1-1/+7
2023-10-26Make minor modifications and update the array test for F*Son Ho1-1/+3
2023-10-25Remove the warning for loopsSon Ho1-8/+0
2023-10-16Fix a small issueSon Ho1-2/+0
2023-10-13Add supSon Ho1-0/+2
2023-09-07Map some globals like u32::MAX to standard definitionsSon Ho1-14/+0
2023-09-04Fix minor issuesSon Ho1-1/+3
2023-08-08Update the code following a refactor on Charon's sideSon Ho1-2/+6
2023-08-04Add an option to not override Hashmap.leanSon Ho1-0/+6
2023-07-06Use short names for the structure fields in LeanSon Ho1-1/+3
2023-07-04Reorganize the Lean testsSon Ho1-0/+6
2023-06-04Make good progress on generating code for HOL4Son Ho1-0/+5
2023-06-04Add a sanity check in Driver.mlSon Ho1-0/+13
2023-06-04Remove the symbolic interpreter testsSon Ho1-5/+0
2023-06-04Automate the generation of the lakefile.lean filesSon Ho1-1/+1
2023-06-04Add a check in Driver.mlSon Ho1-0/+12
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
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-19 21:40:05 +0000