summaryrefslogtreecommitdiff
path: root/tests (unfollow)
Commit message (Expand)AuthorFilesLines
2024-06-28Remove redundant `llbc_name` fieldNadrieril1-6/+6
2024-06-28Update charonNadrieril15-21/+21
2024-06-25Bump Lean to v4.9.0rc3 (#261)Son HO3-5/+2
2024-06-24Update charonNadrieril1-6/+6
2024-06-24Update charonNadrieril9-9/+9
2024-06-22Do some cleanup in the Lean backend (#257)Son HO1-56/+20
2024-06-22Improve `scalar_tac` and `scalar_decr_tac` (#256)Son HO1-76/+24
2024-06-21Add some proofs for the Lean backend (#255)Son HO9-125/+1038
2024-06-21Update charonNadrieril1-3/+3
2024-06-18Support for renaming using the rename attribute in charon (#239)Escherichia15-6/+2309
2024-06-18Bump charonNadrieril16-60/+60
2024-06-18Tiny dedupNadrieril1-1/+1
2024-06-17Regenerate the testsSon Ho15-18/+18
2024-06-17Update charonNadrieril15-18/+18
2024-06-17Regenerate the testsSon Ho26-2/+77
2024-06-17Update the testsSon Ho6-4/+31
2024-06-17Update Hashmap/Properties.leanSon Ho1-36/+34
2024-06-17Update the code of the hashmapSon Ho12-459/+465
2024-06-17Update the Lean dependenciesSon Ho1-4/+4
2024-06-14Update the testsSon Ho2-4/+4
2024-06-13Update the testsSon Ho3-29/+29
2024-06-12Update the code extraction and regenerate the testsSon Ho1-2/+2
2024-06-12Revert "Regenerate the tests"Son Ho12-333/+338
2024-06-12Revert "Fix some mistakes"Son Ho3-15/+15
2024-06-12Fix some mistakesSon Ho3-15/+15
2024-06-12Regenerate the testsSon Ho12-338/+333
2024-06-11Deactivate the use of tuple projectors in the Lean backendSon Ho1-2/+4
2024-06-11Update the tests for tuplesSon Ho4-22/+85
2024-06-05Regenerate the Coq and Lean betreesSon Ho2-178/+423
2024-06-05Update the F* betreeSon Ho3-144/+280
2024-06-05Update the betreeSon Ho1-99/+98
2024-06-05Regenerate some testsSon Ho1-14/+2
2024-06-05Add some negative tests for the borrow checkerSon Ho2-0/+105
2024-06-05Add more testsSon Ho5-0/+79
2024-06-05Update the test runnerSon Ho1-1/+4
2024-06-05Update the test runner to allow the syntax [!lean] and [borrow-check]Son Ho14-34/+65
2024-06-05Update charonNadrieril27-287/+278
2024-06-03Add a testSon Ho4-103/+123
2024-05-31Regenerate testsAymeric Fromherz13-35/+35
2024-05-31Regenerate test outputAymeric Fromherz19-108/+2588
2024-05-30Remove the options from the functions synthesizing the symbolic ASTSon Ho1-6/+6
2024-05-30Implement two phases of loops join + collapseAymeric Fromherz19-2588/+108
2024-05-30Improve the tests READMENadrieril2-14/+22
2024-05-30runner: Factor out backend-specific optionsNadrieril2-49/+56
2024-05-30runner: Split up into multiple filesNadrieril6-198/+191
2024-05-30runner: make the backend map a submodule of `Backend`Nadrieril1-36/+48
2024-05-30tests: Add a READMENadrieril1-0/+67
2024-05-28Fix an issue with some names being ignored when generating unique variable namesSon Ho2-4/+4
2024-05-28Reactivate the infinite-loop.rs testSon Ho4-1/+76
2024-05-28Add type and set/map for marker and borrow idAymeric Fromherz1-1/+1
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-22 11:33:00 +0000