summaryrefslogtreecommitdiff
path: root/tests (unfollow)
Commit message (Expand)AuthorFilesLines
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
2022-06-20Add makefiles to test the F* filesSon Ho6-2/+274
2022-06-20Remove a commentSon Ho1-189/+0
2022-05-15Regenerate the F* filesSon Ho10-194/+130
2022-05-15Treat integer casts in a general mannerSon Ho5-0/+20
2022-05-15Regenerate a test fileSon Ho1-6/+8
2022-05-09Make minor modificationsSon Ho1-4/+6
2022-05-09Update the termination proofs of the betreeSon Ho2-26/+110
2022-05-06Update the extraction to set the fuel to 1 in the Z3 optionsSon Ho16-16/+16
2022-05-06Make the betree workSon Ho3-368/+405
2022-05-06Regenerate the F* for external.rsSon Ho2-2/+2
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-19 10:36:18 +0000