summaryrefslogtreecommitdiff
path: root/tests (follow)
Commit message (Collapse)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 ↵Son Ho2022-11-1616-15/+51
| | | | subdirectories
* 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 ↵Son Ho2022-11-109-25/+2870
| | | | option)
* 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 ↵Sidney Congard2022-08-104-11/+139
| | | | translation
* 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
|\ | | | | | | Complete the constants extraction by making all functions fail
| * 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-06 03:22:55 +0000