summaryrefslogtreecommitdiff
path: root/tests (follow)
Commit message (Expand)AuthorAgeFilesLines
* Add a nix derivation for the Coq proofsSon Ho2022-11-162-2/+7
* Do not introduce match on the fuel for non-recursive functionsSon Ho2022-11-163-667/+477
* Automatically generate the Makefile and _CoqProject files in the tests subdir...Son Ho2022-11-1616-15/+51
* Add the aeneas-verify-fstar derivationSon Ho2022-11-165-5/+10
* Generate record field projectors for CoqSon Ho2022-11-1610-695/+612
* Change the name of the generated Coq modulesSon Ho2022-11-1611-42/+42
* Improve formattingSon Ho2022-11-1617-583/+587
* Remove some comments from Hashmap.Properties.fstSon Ho2022-11-161-60/+0
* Make minor modifications to the extractionSon Ho2022-11-169-58/+70
* Extract the Polonius examples in CoqSon Ho2022-11-148-1/+2105
* Generate Coq code for `hashmap` and `hashmap_on_disk`Son Ho2022-11-1411-0/+2264
* Add a `-use-fuel` optionSon Ho2022-11-147-3/+56
* Regenerate the files and fix the proofsSon Ho2022-11-1421-1088/+1159
* Improve the formatting of [if then else] expressionsSon Ho2022-11-142-86/+70
* Reactivate the option -test-trans-unis for CoqSon Ho2022-11-141-0/+3
* Improve the formatting of the generated codeSon Ho2022-11-145-36/+51
* Implement a pass to decompose nested patterns in let-bindingsSon Ho2022-11-141-2/+3
* Make minor modificationsSon Ho2022-11-141-2/+1
* Make good progress on the Coq backendSon Ho2022-11-1412-53/+1431
* Reorganize the project to prepare for new backendsSon Ho2022-11-1441-0/+0
* Make minor modifications to the tests and regenerate the .fst filesSon Ho2022-11-112-15/+15
* Make a minor cleanupSon Ho2022-11-105-15/+20
* Implement the generation of stateful backward functions (controlled by an opt...Son Ho2022-11-109-25/+2870
* Regenerate the filesSon Ho2022-10-2010-10/+10
* Use "polonius" in the names instead of "nll"Son Ho2022-10-131-5/+5
* Fix MakefilesJonathan Protzenko2022-09-275-55/+50
* Regenerate the translated filesSon Ho2022-09-224-4/+4
* Correct last PR remarksSidney Congard2022-08-111-3/+3
* Correct assertion for stateless globalsSidney Congard2022-08-116-15/+29
* Corrected translation without using functions, remaining bug in hashmap trans...Sidney Congard2022-08-104-11/+139
* Register global names, one error remainingSidney Congard2022-08-081-0/+10
* Create global declaration group, address PR changes but introduce bugsSidney Congard2022-07-291-135/+0
* Remove last prints, adapt JSONSidney Congard2022-07-054-195/+203
* Merge branch 'main' of github.com:Kachoc/aeneas into constants-v2Sidney Congard2022-06-3013-225/+439
|\
| * Update the MakefilesSon Ho2022-06-275-20/+5
| * Add makefiles to test the F* filesSon Ho2022-06-206-2/+274
| * Remove a commentSon Ho2022-06-201-189/+0
* | Traduct globals body separately (WIP)Sidney Congard2022-06-302-128/+4
* | adapt to new LLBC (without OperandConstantValue)Sidney Congard2022-06-231-0/+19
* | concrete & symbolic evaluation work with new LLBC formatSidney Congard2022-06-211-0/+119
|/
* Regenerate the F* filesSon Ho2022-05-1510-194/+130
* Treat integer casts in a general mannerSon Ho2022-05-155-0/+20
* Regenerate a test fileSon Ho2022-05-151-6/+8
* Make minor modificationsSon Ho2022-05-091-4/+6
* Update the termination proofs of the betreeSon Ho2022-05-092-26/+110
* Update the extraction to set the fuel to 1 in the Z3 optionsSon Ho2022-05-0616-16/+16
* Make the betree workSon Ho2022-05-063-368/+405
* Regenerate the F* for external.rsSon Ho2022-05-062-2/+2
* Regenerate the F* files for the betreeSon Ho2022-05-061-38/+73
* Regenerate the F* files for external.rsSon Ho2022-05-061-2/+14
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-05 15:24:10 +0000