| Commit message (Expand) | Author | Files | Lines |
2023-12-05 | Print error messages when the command line arguments are invalid | Son Ho | 1 | -10/+40 |
2023-11-27 | Do not activate the sanity (invariant) checks by default | Son Ho | 1 | -4/+4 |
2023-11-21 | Reorganize the "Extract" files | Son Ho | 1 | -1/+4 |
2023-11-20 | Fix minor issues | Son Ho | 1 | -0/+1 |
2023-11-16 | Rename Driver.ml to Main.ml | Son Ho | 1 | -0/+0 |
2023-11-16 | Finish propagating the changes to the names and cleaning | Son Ho | 1 | -12/+9 |
2023-11-13 | Make minor modifications | Son Ho | 1 | -0/+1 |
2023-11-09 | Modify some options and update the Makefile | Son Ho | 1 | -7/+7 |
2023-11-09 | Fix a small issue in AssociatedTypes | Son Ho | 1 | -1/+7 |
2023-10-26 | Make minor modifications and update the array test for F* | Son Ho | 1 | -1/+3 |
2023-10-25 | Remove the warning for loops | Son Ho | 1 | -8/+0 |
2023-10-16 | Fix a small issue | Son Ho | 1 | -2/+0 |
2023-10-13 | Add sup | Son Ho | 1 | -0/+2 |
2023-09-07 | Map some globals like u32::MAX to standard definitions | Son Ho | 1 | -14/+0 |
2023-09-04 | Fix minor issues | Son Ho | 1 | -1/+3 |
2023-08-08 | Update the code following a refactor on Charon's side | Son Ho | 1 | -2/+6 |
2023-08-04 | Add an option to not override Hashmap.lean | Son Ho | 1 | -0/+6 |
2023-07-06 | Use short names for the structure fields in Lean | Son Ho | 1 | -1/+3 |
2023-07-04 | Reorganize the Lean tests | Son Ho | 1 | -0/+6 |
2023-06-04 | Make good progress on generating code for HOL4 | Son Ho | 1 | -0/+5 |
2023-06-04 | Add a sanity check in Driver.ml | Son Ho | 1 | -0/+13 |
2023-06-04 | Remove the symbolic interpreter tests | Son Ho | 1 | -5/+0 |
2023-06-04 | Automate the generation of the lakefile.lean files | Son Ho | 1 | -1/+1 |
2023-06-04 | Add a check in Driver.ml | Son Ho | 1 | -0/+12 |
2023-06-04 | Consistently use the names TerminationMeasure and DecreasesProof | Son Ho | 1 | -11/+13 |
2023-06-04 | Add more checks in Driver.ml | Son Ho | 1 | -2/+6 |
2023-06-04 | Print warnings for the Lean backend and loops | Son Ho | 1 | -8/+13 |
2023-06-04 | WIP lots of stuff | Jonathan Protzenko | 1 | -15/+19 |
2023-06-04 | Initial Lean backend, WIP | Jonathan Protzenko | 1 | -0/+2 |
2023-02-03 | Do not unfold the monadic lets for the generated F* code | Son Ho | 1 | -2/+3 |
2023-02-03 | Split InterpreterLoops into several files | Son Ho | 1 | -0/+3 |
2023-02-03 | Make minor modifications and generate code for loops | Son Ho | 1 | -24/+28 |
2023-02-03 | Remove the meta-value field from AMutBorrow | Son Ho | 1 | -16/+18 |
2022-11-16 | Generate record field projectors for Coq | Son Ho | 1 | -7/+0 |
2022-11-14 | Add a `-use-fuel` option | Son Ho | 1 | -0/+8 |
2022-11-14 | Implement a pass to decompose nested patterns in let-bindings | Son Ho | 1 | -21/+13 |
2022-11-14 | Make good progress on the Coq backend | Son Ho | 1 | -5/+31 |
2022-11-11 | Make the Nix build work | Son Ho | 1 | -3/+4 |
2022-11-10 | Implement a Config.ml file which groups all the global options in references | Son Ho | 1 | -63/+21 |
2022-11-10 | Implement the generation of stateful backward functions (controlled by an opt... | Son Ho | 1 | -2/+10 |
2022-11-07 | Add some .mli files | Son Ho | 1 | -0/+1 |
2022-10-28 | Make minor modifications | Son Ho | 1 | -1/+1 |
2022-10-28 | Make minor updates to account for Charon's changes | Son Ho | 1 | -1/+1 |
2022-10-27 | Rename driver.ml to Driver.ml | Son Ho | 1 | -0/+0 |
2022-10-27 | Reorganize a bit the project | Son Ho | 1 | -0/+0 |
2022-10-26 | Start generating documentation | Son Ho | 1 | -8/+11 |
2022-10-26 | Measure and display the execution time | Son Ho | 1 | -1/+11 |
2022-10-13 | Rename Modules to Crates | Son Ho | 1 | -1/+1 |
2022-06-23 | adapt to new LLBC (without OperandConstantValue) | Sidney Congard | 1 | -15/+15 |
2022-06-21 | concrete & symbolic evaluation work with new LLBC format | Sidney Congard | 1 | -15/+15 |