summaryrefslogtreecommitdiff
path: root/tests/misc (follow)
Commit message (Collapse)AuthorAgeFilesLines
* Make minor modifications to the tests and regenerate the .fst filesSon Ho2022-11-112-15/+15
|
* Make a minor cleanupSon Ho2022-11-101-3/+4
|
* Implement the generation of stateful backward functions (controlled by an ↵Son Ho2022-11-102-25/+42
| | | | option)
* Regenerate the filesSon Ho2022-10-201-1/+1
|
* Use "polonius" in the names instead of "nll"Son Ho2022-10-131-5/+5
|
* Fix MakefilesJonathan Protzenko2022-09-271-11/+10
|
* Regenerate the translated filesSon Ho2022-09-221-1/+1
|
* Correct last PR remarksSidney Congard2022-08-111-3/+3
|
* Corrected translation without using functions, remaining bug in hashmap ↵Sidney Congard2022-08-101-1/+122
| | | | 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
|
* Merge branch 'main' of github.com:Kachoc/aeneas into constants-v2Sidney Congard2022-06-303-17/+193
|\ | | | | | | Complete the constants extraction by making all functions fail
| * Update the MakefilesSon Ho2022-06-271-4/+1
| |
| * Add makefiles to test the F* filesSon Ho2022-06-201-2/+51
| |
* | 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-154-34/+34
|
* Treat integer casts in a general mannerSon Ho2022-05-152-0/+8
|
* Regenerate a test fileSon Ho2022-05-151-6/+8
|
* Update the extraction to set the fuel to 1 in the Z3 optionsSon Ho2022-05-066-6/+6
|
* Regenerate the F* for external.rsSon Ho2022-05-062-2/+2
|
* Regenerate the F* files for external.rsSon Ho2022-05-061-2/+14
|
* Regenerate the F* files for external.rsSon Ho2022-05-051-2/+17
|
* Regenerate the F* files for the external.rs testSon Ho2022-05-042-7/+46
|
* Regenerate some of the test filesSon Ho2022-05-011-5/+6
|
* Regenerate the test filesSon Ho2022-04-214-19/+15
|
* Regenerate the test filesSon Ho2022-04-202-35/+35
|
* Update the evaluation of matches for the cases where the scrutinee is aSon Ho2022-04-201-0/+14
| | | | shared loan
* Regenerate a test fileSon Ho2022-04-201-0/+20
|
* Regenerate Paper.fstSon Ho2022-03-051-0/+16
|
* Generate hashmap_on_diskSon Ho2022-03-041-0/+279
|
* Make minor modifications to the variable names generationSon Ho2022-03-041-1/+1
|
* Commit the translation of external.rsSon Ho2022-03-043-0/+88
|
* Add the betree_nll.rs testSon Ho2022-02-261-0/+41
|
* Improve variable name generationSon Ho2022-02-231-8/+8
|
* Inline more let-bindings and improve formattingSon Ho2022-02-232-35/+24
|
* Track the generated F* files from tests/miscSon Ho2022-02-232-0/+666
|
* More stuff for the paper + interactive mode makefileJonathan Protzenko2022-02-171-0/+2
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-24 01:14:18 +0000