summaryrefslogtreecommitdiff
path: root/tests (unfollow)
Commit message (Expand)AuthorFilesLines
2023-02-03Improve the order of the loop input parametersSon Ho13-62/+62
2023-02-03Improve the heuristic to find pretty names for the variables in the loopsSon Ho9-377/+387
2023-02-03Improve PureMicroPasses.filter_useless and regenerate the betree codeSon Ho3-85/+56
2023-02-03Regenerate the hashmap code and update the proofsSon Ho10-380/+681
2023-02-03Fix some issues with the values given back by loop backward translationsSon Ho4-0/+160
2023-02-03Fix an issue with the translation of loops::clearSon Ho2-16/+6
2023-02-03Add more loop examples and fix issuesSon Ho4-0/+312
2023-02-03Implement support for nested borrows in loops, and add loop testsSon Ho4-18/+820
2023-02-03Regenerate the testsSon Ho4-0/+394
2023-02-03Improve the loops' numberingSon Ho2-19/+18
2023-02-03Make another loop example workSon Ho4-0/+44
2023-02-03Regenerate the filesSon Ho19-863/+245
2023-02-03Make minor modifications and generate code for loopsSon Ho6-0/+176
2022-11-16Add a nix derivation for the Coq proofsSon Ho2-2/+7
2022-11-16Do not introduce match on the fuel for non-recursive functionsSon Ho3-667/+477
2022-11-16Automatically generate the Makefile and _CoqProject files in the tests subdir...Son Ho16-15/+51
2022-11-16Add the aeneas-verify-fstar derivationSon Ho5-5/+10
2022-11-16Generate record field projectors for CoqSon Ho10-695/+612
2022-11-16Change the name of the generated Coq modulesSon Ho11-42/+42
2022-11-16Improve formattingSon Ho17-583/+587
2022-11-16Remove some comments from Hashmap.Properties.fstSon Ho1-60/+0
2022-11-16Make minor modifications to the extractionSon Ho9-58/+70
2022-11-14Extract the Polonius examples in CoqSon Ho8-1/+2105
2022-11-14Generate Coq code for `hashmap` and `hashmap_on_disk`Son Ho11-0/+2264
2022-11-14Add a `-use-fuel` optionSon Ho7-3/+56
2022-11-14Regenerate the files and fix the proofsSon Ho21-1088/+1159
2022-11-14Improve the formatting of [if then else] expressionsSon Ho2-86/+70
2022-11-14Reactivate the option -test-trans-unis for CoqSon Ho1-0/+3
2022-11-14Improve the formatting of the generated codeSon Ho5-36/+51
2022-11-14Implement a pass to decompose nested patterns in let-bindingsSon Ho1-2/+3
2022-11-14Make minor modificationsSon Ho1-2/+1
2022-11-14Make good progress on the Coq backendSon Ho12-53/+1431
2022-11-14Reorganize the project to prepare for new backendsSon Ho41-0/+0
2022-11-11Make minor modifications to the tests and regenerate the .fst filesSon Ho2-15/+15
2022-11-10Make a minor cleanupSon Ho5-15/+20
2022-11-10Implement the generation of stateful backward functions (controlled by an opt...Son Ho9-25/+2870
2022-10-20Regenerate the filesSon Ho10-10/+10
2022-10-13Use "polonius" in the names instead of "nll"Son Ho1-5/+5
2022-09-27Fix MakefilesJonathan Protzenko5-55/+50
2022-09-22Regenerate the translated filesSon Ho4-4/+4
2022-08-11Correct last PR remarksSidney Congard1-3/+3
2022-08-11Correct assertion for stateless globalsSidney Congard6-15/+29
2022-08-10Corrected translation without using functions, remaining bug in hashmap trans...Sidney Congard4-11/+139
2022-08-08Register global names, one error remainingSidney Congard1-0/+10
2022-07-29Create global declaration group, address PR changes but introduce bugsSidney Congard1-135/+0
2022-07-05Remove last prints, adapt JSONSidney Congard4-195/+203
2022-06-30Traduct globals body separately (WIP)Sidney Congard2-128/+4
2022-06-27Update the MakefilesSon Ho5-20/+5
2022-06-23adapt to new LLBC (without OperandConstantValue)Sidney Congard1-0/+19
2022-06-21concrete & symbolic evaluation work with new LLBC formatSidney Congard1-0/+119
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 23:30:51 +0000