| Commit message (Expand) | Author | Age | Files | Lines |
... | |
* | Improve the order of the loop input parameters | Son Ho | 2023-02-03 | 13 | -62/+62 |
* | Improve the heuristic to find pretty names for the variables in the loops | Son Ho | 2023-02-03 | 9 | -377/+387 |
* | Improve PureMicroPasses.filter_useless and regenerate the betree code | Son Ho | 2023-02-03 | 3 | -85/+56 |
* | Regenerate the hashmap code and update the proofs | Son Ho | 2023-02-03 | 10 | -380/+681 |
* | Fix some issues with the values given back by loop backward translations | Son Ho | 2023-02-03 | 4 | -0/+160 |
* | Fix an issue with the translation of loops::clear | Son Ho | 2023-02-03 | 2 | -16/+6 |
* | Add more loop examples and fix issues | Son Ho | 2023-02-03 | 4 | -0/+312 |
* | Implement support for nested borrows in loops, and add loop tests | Son Ho | 2023-02-03 | 4 | -18/+820 |
* | Regenerate the tests | Son Ho | 2023-02-03 | 4 | -0/+394 |
* | Improve the loops' numbering | Son Ho | 2023-02-03 | 2 | -19/+18 |
* | Make another loop example work | Son Ho | 2023-02-03 | 4 | -0/+44 |
* | Regenerate the files | Son Ho | 2023-02-03 | 19 | -863/+245 |
* | Make minor modifications and generate code for loops | Son Ho | 2023-02-03 | 6 | -0/+176 |
* | Add a nix derivation for the Coq proofs | Son Ho | 2022-11-16 | 2 | -2/+7 |
* | Do not introduce match on the fuel for non-recursive functions | Son Ho | 2022-11-16 | 3 | -667/+477 |
* | Automatically generate the Makefile and _CoqProject files in the tests subdir... | Son Ho | 2022-11-16 | 16 | -15/+51 |
* | Add the aeneas-verify-fstar derivation | Son Ho | 2022-11-16 | 5 | -5/+10 |
* | Generate record field projectors for Coq | Son Ho | 2022-11-16 | 10 | -695/+612 |
* | Change the name of the generated Coq modules | Son Ho | 2022-11-16 | 11 | -42/+42 |
* | Improve formatting | Son Ho | 2022-11-16 | 17 | -583/+587 |
* | Remove some comments from Hashmap.Properties.fst | Son Ho | 2022-11-16 | 1 | -60/+0 |
* | Make minor modifications to the extraction | Son Ho | 2022-11-16 | 9 | -58/+70 |
* | Extract the Polonius examples in Coq | Son Ho | 2022-11-14 | 8 | -1/+2105 |
* | Generate Coq code for `hashmap` and `hashmap_on_disk` | Son Ho | 2022-11-14 | 11 | -0/+2264 |
* | Add a `-use-fuel` option | Son Ho | 2022-11-14 | 7 | -3/+56 |
* | Regenerate the files and fix the proofs | Son Ho | 2022-11-14 | 21 | -1088/+1159 |
* | Improve the formatting of [if then else] expressions | Son Ho | 2022-11-14 | 2 | -86/+70 |
* | Reactivate the option -test-trans-unis for Coq | Son Ho | 2022-11-14 | 1 | -0/+3 |
* | Improve the formatting of the generated code | Son Ho | 2022-11-14 | 5 | -36/+51 |
* | Implement a pass to decompose nested patterns in let-bindings | Son Ho | 2022-11-14 | 1 | -2/+3 |
* | Make minor modifications | Son Ho | 2022-11-14 | 1 | -2/+1 |
* | Make good progress on the Coq backend | Son Ho | 2022-11-14 | 12 | -53/+1431 |
* | Reorganize the project to prepare for new backends | Son Ho | 2022-11-14 | 41 | -0/+0 |
* | Make minor modifications to the tests and regenerate the .fst files | Son Ho | 2022-11-11 | 2 | -15/+15 |
* | Make a minor cleanup | Son Ho | 2022-11-10 | 5 | -15/+20 |
* | Implement the generation of stateful backward functions (controlled by an opt... | Son Ho | 2022-11-10 | 9 | -25/+2870 |
* | Regenerate the files | Son Ho | 2022-10-20 | 10 | -10/+10 |
* | Use "polonius" in the names instead of "nll" | Son Ho | 2022-10-13 | 1 | -5/+5 |
* | Fix Makefiles | Jonathan Protzenko | 2022-09-27 | 5 | -55/+50 |
* | Regenerate the translated files | Son Ho | 2022-09-22 | 4 | -4/+4 |
* | Correct last PR remarks | Sidney Congard | 2022-08-11 | 1 | -3/+3 |
* | Correct assertion for stateless globals | Sidney Congard | 2022-08-11 | 6 | -15/+29 |
* | Corrected translation without using functions, remaining bug in hashmap trans... | Sidney Congard | 2022-08-10 | 4 | -11/+139 |
* | Register global names, one error remaining | Sidney Congard | 2022-08-08 | 1 | -0/+10 |
* | Create global declaration group, address PR changes but introduce bugs | Sidney Congard | 2022-07-29 | 1 | -135/+0 |
* | Remove last prints, adapt JSON | Sidney Congard | 2022-07-05 | 4 | -195/+203 |
* | Merge branch 'main' of github.com:Kachoc/aeneas into constants-v2 | Sidney Congard | 2022-06-30 | 13 | -225/+439 |
|\ |
|
| * | Update the Makefiles | Son Ho | 2022-06-27 | 5 | -20/+5 |
| * | Add makefiles to test the F* files | Son Ho | 2022-06-20 | 6 | -2/+274 |
| * | Remove a comment | Son Ho | 2022-06-20 | 1 | -189/+0 |