summaryrefslogtreecommitdiff
path: root/tests (unfollow)
Commit message (Expand)AuthorFilesLines
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
2022-05-06Regenerate the F* files for the betreeSon Ho1-38/+73
2022-05-06Regenerate the F* files for external.rsSon Ho1-2/+14
2022-05-06Generate F* files for the betreeSon Ho6-0/+2230
2022-05-05Update the hashmap_on_disk exampleSon Ho4-771/+240
2022-05-05Regenerate the F* files for external.rsSon Ho1-2/+17
2022-05-04Regenerate the F* files for hashmap_main.rsSon Ho1-180/+241
2022-05-04Regenerate the F* files for the external.rs testSon Ho2-7/+46
2022-05-01Regenerate some of the test filesSon Ho2-9/+8
2022-04-21Regenerate the test filesSon Ho6-86/+93
2022-04-20Regenerate the test filesSon Ho4-148/+149
2022-04-20Update the evaluation of matches for the cases where the scrutinee is aSon Ho1-0/+14
2022-04-20Regenerate a test fileSon Ho1-0/+20
2022-03-05Regenerate Paper.fstSon Ho1-0/+16
2022-03-05Make an update in the hash mapSon Ho2-9/+4
2022-03-04Make a minor modificationSon Ho1-1/+1
2022-03-04Make minor modifications to hashmap_on_diskSon Ho1-9/+14
2022-03-04Make minor modificationsSon Ho1-5/+5
2022-03-04Do the proofs about hashmap_on_diskSon Ho1-0/+300
2022-03-04Generate hashmap_on_diskSon Ho8-0/+1733
2022-03-04Make minor modifications to the variable names generationSon Ho1-1/+1
2022-03-04Commit the translation of external.rsSon Ho3-0/+88
2022-03-03Change the extension of the serialized files to .llbcSon Ho1-25/+25
2022-02-26Add the betree_nll.rs testSon Ho1-0/+41
2022-02-24Update the way function names are handledSon Ho1-25/+25
2022-02-23Improve variable name generationSon Ho2-47/+48
2022-02-23Inline more let-bindings and improve formattingSon Ho3-107/+92
2022-02-23Track the generated F* files from tests/miscSon Ho2-0/+666
2022-02-23Improve the code generation by inlining more let-bindingsSon Ho1-108/+90
2022-02-17More stuff for the paper + interactive mode makefileJonathan Protzenko1-0/+2
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 14:03:11 +0000