aeneas - aeneas rust verifier with a hacky Isabelle backend

	Commit message (Collapse)	Author	Age	Files	Lines
*	Remove redundant `llbc_name` field	Nadrieril	2024-06-28	1	-6/+6
\| \| \| \|	It's redundant with `item_meta.name`
*	Update charon	Nadrieril	2024-06-24	1	-6/+6
\|
*	Add some proofs for the Lean backend (#255)	Son HO	2024-06-21	1	-11/+11
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	* 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>
*	Update charon	Nadrieril	2024-06-21	1	-3/+3
\|
*	Support for renaming using the rename attribute in charon (#239)	Escherichia	2024-06-18	7	-6/+81
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	* 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>
*	Tiny dedup	Nadrieril	2024-06-18	1	-1/+1
\|
*	Regenerate the tests	Son Ho	2024-06-17	1	-2/+2
\|
*	Update the code of the hashmap	Son Ho	2024-06-17	1	-30/+31
\|
*	Update the tests for tuples	Son Ho	2024-06-11	1	-1/+13
\|
*	Update the betree	Son Ho	2024-06-05	1	-99/+98
\|
*	Regenerate some tests	Son Ho	2024-06-05	1	-14/+2
\|
*	Add some negative tests for the borrow checker	Son Ho	2024-06-05	2	-0/+105
\|
*	Add more tests	Son Ho	2024-06-05	5	-0/+79
\|
*	Update the test runner to allow the syntax [!lean] and [borrow-check]	Son Ho	2024-06-05	11	-19/+19
\|
*	Merge branch 'main' into son/clean-synthesis	Son Ho	2024-06-05	1	-1/+6
\|\
\| *	Merge branch 'main' into son/loops2	Son Ho	2024-06-04	21	-28/+140
\| \|\
\| * \|	Add a test	Son Ho	2024-06-03	1	-1/+6
\| \| \|
* \| \|	Remove the options from the functions synthesizing the symbolic AST	Son Ho	2024-05-30	1	-6/+6
\| \|/ \|/\|
* \|	Reactivate the infinite-loop.rs test	Son Ho	2024-05-28	1	-1/+0
\| \|
* \|	tests: Rename hashmap_utils -> utils	Nadrieril	2024-05-28	1	-4/+4
\| \|
* \|	Add some tests	Nadrieril	2024-05-28	3	-0/+37
\| \|
* \|	runner: Store options for crate tests in a separate file	Nadrieril	2024-05-28	1	-0/+4
\| \|
* \|	tests: Merge the hashmap test files	Nadrieril	2024-05-27	3	-36/+28
\| \|
* \|	runner: Add `no-check-output` option for unstable outputs	Nadrieril	2024-05-27	2	-21/+1
\| \|
* \|	runner: Support negative tests	Nadrieril	2024-05-27	4	-0/+55
\| \|
* \|	runner: Specify subdirectory in magic comments	Nadrieril	2024-05-24	8	-0/+8
\| \|
* \|	runner: Pass options in special comments	Nadrieril	2024-05-24	14	-0/+37
\|/
*	Import test suite from charon	Nadrieril	2024-05-24	22	-0/+4011