| Commit message (Expand) | Author | Age | Files | Lines |
... | |
| * | Finish propagating the changes to the names and cleaning | Son Ho | 2023-11-16 | 1 | -3/+3 |
| * | Start updating the name type, cleanup the names and the module abbrevs | Son Ho | 2023-11-15 | 1 | -107/+107 |
| * | Add RegionsHierarchy.ml | Son Ho | 2023-11-13 | 1 | -7/+18 |
| * | Add the "V" prefix to most variants related to values | Son Ho | 2023-11-12 | 1 | -10/+10 |
| * | Prefix variants related to types with "T" | Son Ho | 2023-11-12 | 1 | -53/+51 |
| * | Rename some variants | Son Ho | 2023-11-12 | 1 | -2/+2 |
| * | Remove the 'r type variable from the ty type definition | Son Ho | 2023-11-12 | 1 | -106/+113 |
| * | Update the normalization of associated types | Son Ho | 2023-11-07 | 1 | -0/+3 |
| * | Update following some changes in Charon | Son Ho | 2023-11-06 | 1 | -0/+3 |
| * | Make minor updates following changes in Charon | Son Ho | 2023-10-30 | 1 | -5/+2 |
| * | Fix some issues to make the array test succeed again | Son Ho | 2023-10-25 | 1 | -9/+12 |
| * | Update following the addition of raw pointers | Son Ho | 2023-10-25 | 1 | -0/+13 |
| * | Remove some assumed types and add more support for builtin definitions | Son Ho | 2023-10-23 | 1 | -24/+7 |
| * | Start updating to handle function pointers | Son Ho | 2023-10-20 | 1 | -22/+28 |
| * | Normalize the function signatures before translation to pure | Son Ho | 2023-09-17 | 1 | -0/+27 |
| * | Make minor modifications | Son Ho | 2023-09-17 | 1 | -11/+8 |
| * | Fix more issues | Son Ho | 2023-09-13 | 1 | -34/+43 |
| * | Make minor modifications | Son Ho | 2023-09-13 | 1 | -37/+0 |
| * | Make progress on correctly handling trait method calls in the symbolic execution | Son Ho | 2023-09-11 | 1 | -12/+61 |
| * | Add support for the trait associated constants | Son Ho | 2023-09-10 | 1 | -2/+10 |
| * | Fix minor issues | Son Ho | 2023-09-04 | 1 | -2/+12 |
| * | Make progress on the extraction | Son Ho | 2023-09-03 | 1 | -2/+108 |
| * | Make progress on the extraction | Son Ho | 2023-09-03 | 1 | -6/+21 |
| * | Finish updating SymbolicToPure.ml | Son Ho | 2023-08-31 | 1 | -110/+196 |
| * | Start adding support for traits | Son Ho | 2023-08-31 | 1 | -8/+15 |
| * | Update following the introduction of ConstantExpr | Son Ho | 2023-08-18 | 1 | -23/+26 |
* | | Allow bitshifts with any pair of integer types | Aymeric Fromherz | 2023-09-22 | 1 | -1/+5 |
|/ |
|
* | Fix an issue with the extraction of aggregated arrays | Son Ho | 2023-08-03 | 1 | -4/+19 |
* | Make progress | Son Ho | 2023-08-02 | 1 | -13/+0 |
* | Make progress | Son Ho | 2023-08-02 | 1 | -5/+12 |
* | Make progress | Son Ho | 2023-08-02 | 1 | -106/+143 |
* | Make progress proapagating the changes | Son Ho | 2023-08-02 | 1 | -17/+29 |
* | Make good progress on generating code for HOL4 | Son Ho | 2023-06-04 | 1 | -1/+1 |
* | Add a special expression for structure creation/update | Son Ho | 2023-06-04 | 1 | -117/+144 |
* | Add more checks in Driver.ml | Son Ho | 2023-06-04 | 1 | -1/+2 |
* | Initial Lean backend, WIP | Jonathan Protzenko | 2023-06-04 | 1 | -0/+2 |
* | Improve the pretty names generation for loops | Son Ho | 2023-02-03 | 1 | -16/+54 |
* | Implement a pass to filter the unused input arguments in the loop functions | Son Ho | 2023-02-03 | 1 | -7/+8 |
* | Improve the heuristic to find pretty names for the variables in the loops | Son Ho | 2023-02-03 | 1 | -2/+31 |
* | Improve PureMicroPasses.filter_useless and regenerate the betree code | Son Ho | 2023-02-03 | 1 | -0/+2 |
* | Fix a minor issue | Son Ho | 2023-02-03 | 1 | -1/+6 |
* | Fix some issues with the values given back by loop backward translations | Son Ho | 2023-02-03 | 1 | -16/+132 |
* | Fix an issue in translate_forward_end | Son Ho | 2023-02-03 | 1 | -1/+2 |
* | Fix a minor issue in decompose_let_bindings | Son Ho | 2023-02-03 | 1 | -1/+6 |
* | Add more loop examples and fix issues | Son Ho | 2023-02-03 | 1 | -5/+52 |
* | Implement support for nested borrows in loops, and add loop tests | Son Ho | 2023-02-03 | 1 | -0/+15 |
* | Fix various issues with the generation of code for the loops | Son Ho | 2023-02-03 | 1 | -5/+18 |
* | Fix a small issue with SymbolicToPure.translate_loop | Son Ho | 2023-02-03 | 1 | -27/+8 |
* | Fix a minor issue with [translate_end_abstraction_loop] | Son Ho | 2023-02-03 | 1 | -3/+7 |
* | Fix another bug | Son Ho | 2023-02-03 | 1 | -1/+2 |