summaryrefslogtreecommitdiff
path: root/tests (unfollow)
Commit message (Expand)AuthorFilesLines
2022-02-12Make good progress on the second level of refinements forSon Ho1-11/+272
2022-02-12Make minor modifications to Hashmap.Properties.fstSon Ho1-8/+12
2022-02-12Prove the refinment lemma for move_elementsSon Ho1-35/+43
2022-02-12Start working on move_elementsSon Ho1-14/+45
2022-02-12Prove the refinment lemma for hash_map_move_elements_from_listSon Ho1-20/+27
2022-02-12Start making progress on move_elements_from_listSon Ho1-24/+105
2022-02-11Perform some renamings in the hashmap exampleSon Ho1-50/+51
2022-02-11Make minor modificationsSon Ho1-188/+46
2022-02-11Prove some high-level lemmas about find after insertSon Ho1-2/+69
2022-02-11Finish the proof of [hash_map_insert_no_resize_fwd_back_le]Son Ho1-2/+36
2022-02-11Make good progress on proving the refinement lemma forSon Ho1-5/+178
2022-02-11Cleanup and reorganize the proofsSon Ho1-301/+293
2022-02-11Finish proving the lemmas about [insert_in_list_back]Son Ho1-9/+92
2022-02-11Make more progress on the proofs of hashmapSon Ho1-2/+66
2022-02-11Make good progress on the proofs of hashmapSon Ho1-90/+618
2022-02-10Make progress on the hashmap proofsSon Ho1-1/+219
2022-02-10Make progress on the proofs of HashMapSon Ho2-10/+141
2022-02-10Make minor progressSon Ho1-2/+12
2022-02-10Start working on HashMap.Properties.fstSon Ho1-0/+235
2022-02-10Move the generated files to subdirectoriesSon Ho1-0/+0
2022-02-10Start working on the hash map proofsSon Ho1-0/+59
2022-01-29Remove tests/trace_reference.txtSon Ho1-135234/+0
2022-01-12Regenerate the traceSon Ho1-14723/+0
2022-01-12Regenerate the traceSon Ho1-39168/+114636
2022-01-07Regenerate the traceSon Ho1-9286/+47708
2022-01-06Remove the symbolic_proj_comp def and make the set of ended regions aSon Ho1-916/+2078
2022-01-06Update the traceSon Ho1-2016/+20514
2022-01-05Update the code to deserialize regions_hierarchy informationSon Ho1-1/+1
2022-01-03Cleanup a bit and fix some issuesSon Ho1-22/+22
2021-12-17Use eval_ctx instead of env in many functions of the interpreterSon Ho1-1066/+0
2021-12-15Update the traceSon Ho1-2/+500
2021-12-08Reimplement drop_borrows_loans_at_placeSon Ho1-9/+0
2021-12-08Remove g_value, g_typed_value, etc. to make values and abstract valuesSon Ho1-5/+15
2021-12-07Move files aroundSon Ho1-0/+16974