summaryrefslogtreecommitdiff
path: root/tests/coq (unfollow)
Commit message (Collapse)AuthorFilesLines
2024-06-28Update charonNadrieril5-7/+7
2024-06-24Update charonNadrieril3-3/+3
2024-06-21Add some proofs for the Lean backend (#255)Son HO2-20/+49
* Make progress on the proofs of the hashmap * Make a minor modification to the hashmap * Make progress on the hashmap * Make progress on the proofs * Make progress on the proofs * Make progress on the proof of the hashmap * Progress on the proofs of the hashmap * Update a proof * Update the Charon pin * Make minor modifications to the hashmap * Regenerate the tests * Regenerate the hashmap * Add lemmas to the Lean backend * Make progress on the proofs of the hashmap * Make a minor fix * Finish the proof about the hashmap * Update scalar_tac * Make a minor modification in the hashmap * Update the proofs of the hashmap --------- Co-authored-by: Son Ho <sonho@Sons-MacBook-Pro.local> Co-authored-by: Son Ho <sonho@Sons-MBP.lan>
2024-06-18Support for renaming using the rename attribute in charon (#239)Escherichia2-0/+1084
* support for renaming using the rename attribute in charon * support for global decl * add support for renaming field * applied suggested changes and began adding support for variant * finished support for renaming variant * applied suggested changes * add tests * fixed variant and field renaming * update charon-pin * update flake.lock * Update the charon pin * Fix an issue with renaming trait method implementations * Fix an issue with the renaming of trait implementations * Fix an issue when renaming enumerations * Update the Charon pin * Fix the F* tests * Fix an issue with the spans for the loops * Fix the tests * Update a comment * Use fuel in the coq tests * Generate the template decreases clauses by default --------- Co-authored-by: Escherichia <escherichia@charlotte> Co-authored-by: Son Ho <hosonmarc@gmail.com>
2024-06-18Bump charonNadrieril4-15/+15
2024-06-17Regenerate the testsSon Ho5-6/+6
2024-06-17Update charonNadrieril5-6/+6
2024-06-17Update the code of the hashmapSon Ho3-136/+136
2024-06-11Update the tests for tuplesSon Ho1-7/+26
2024-06-05Regenerate the Coq and Lean betreesSon Ho1-89/+221
2024-06-05Update charonNadrieril9-86/+86
2024-06-03Add a testSon Ho1-34/+39
2024-05-31Regenerate testsAymeric Fromherz9-31/+31
2024-05-31Regenerate test outputAymeric Fromherz5-36/+908
2024-05-30Implement two phases of loops join + collapseAymeric Fromherz5-908/+36
2024-05-28Fix an issue with some names being ignored when generating unique variable namesSon Ho1-2/+2
2024-05-28Reactivate the infinite-loop.rs testSon Ho1-0/+27
2024-05-28tests: Rename hashmap_utils -> utilsNadrieril3-11/+10
2024-05-28Add some testsNadrieril1-0/+54
2024-05-28tests: Rename betree_main -> betreeNadrieril7-84/+84
2024-05-27tests: Merge the hashmap test filesNadrieril13-1734/+96
2024-05-24Rename some subdirectories for consistencyNadrieril9-0/+0
2024-05-24Update output filesNadrieril8-177/+177
2024-05-24Update test outputsNadrieril15-391/+391
2024-05-24Tweak a pathNadrieril15-391/+391
2024-05-23Bump charon versionNadrieril5-7/+7
2024-04-30Update charonNadrieril1-1/+1
2024-04-25Regenerate and fix the testsSon Ho9-19/+60
2024-04-25Regenerate the Primitives filesSon Ho6-0/+450
2024-04-25Update the tests for ExternalSon Ho7-92/+134
2024-04-24Update testsZyad Hassan2-14/+0
2024-04-18Ensure we regenerate files properly in CINadrieril6-6/+0
Files that weren't regenerated were marked as not automatically-generated.
2024-04-17Bump charonNadrieril1-159/+56
2024-04-11Fix a Coq fileSon Ho1-1/+1
2024-04-04Regenerate the test filesSon Ho20-535/+501
2024-04-04Regenerate the test filesSon Ho2-12/+12
2024-04-04Regenerate the test filesSon Ho13-99/+104
2024-03-20Regenerate the codeSon Ho9-126/+119
2024-03-19Regenerate the testsSon Ho9-64/+26
2024-03-19Update the demoSon Ho1-10/+38
2024-03-18Regenerate the test filesSon Ho2-22/+114
2024-03-18Regenerate the constants tests and update Primitives/Base.leanSon Ho1-18/+35
2024-03-11Regenerate the test filesSon Ho3-83/+78
2024-03-11Update the generated filesSon Ho5-128/+134
2024-03-09Regenerate the test filesSon Ho2-0/+133
2024-02-09Add some missing filesSon Ho2-0/+30
2024-02-09Add some demo filesSon Ho2-0/+1066
2024-02-02Rename and regenerate some filesSon Ho5-119/+119
2024-01-25Regenerate the filesSon Ho2-66/+80
2023-12-23Fix an issue in External_FunsExternal.vSon Ho1-15/+3
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-22 20:34:52 +0000