adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Commit Graph

  • 38fcd0caf2 Updated repository description. master Achim D. Brucker 2024-01-27 14:09:25 +0000
  • a776293799 Merge branch 'autogenerated_parser' Achim D. Brucker 2024-01-27 13:47:26 +0000
  • ed98ff7b35 Merge branch 'cpp_wrapper' Achim D. Brucker 2024-01-27 13:47:10 +0000
  • 7126276e2c Added generated (using mllex and mlyacc) C-parser files to reduce dependencies required by users of AutoCorres. autogenerated_parser Achim D. Brucker 2023-09-24 10:04:59 +0100
  • dd92984a2d Keeping cpp script for the moment. cpp_wrapper Achim D. Brucker 2024-01-22 09:42:42 +0000
  • e59d6ad091 Renamed Word_Lib shipped by AutoCorres to Word_Lib_l4v to avoid a name clash with the AFP entry of same name. renaming_Word_Lib Achim D. Brucker 2023-09-24 10:01:24 +0100
  • 99c79b50df
         Ensure that umm_types.txt is saved relative to theory file. (#674) Achim D. Brucker 2024-01-27 07:47:54 +0000
  • c71c31d163
         If cpp_path is relative, make it relative to the current theory. (#676) Achim D. Brucker 2024-01-27 07:41:18 +0000
  • 809e485205 Removed trailing whitespaces. cpp_path_relative Achim D. Brucker 2024-01-22 09:36:24 +0000
  • deb6cfada8 docs: add a guide for commit messages Gerwin Klein 2023-10-20 18:40:56 +1100
  • 9bf39e287b c-parser: turn README into main C-parser website Gerwin Klein 2024-01-16 11:32:36 +1100
  • d9df1c5621 autocorres: update AFP links Gerwin Klein 2024-01-16 10:14:22 +1100
  • d5fcddecfd autocorres: point C parser links to GitHub Gerwin Klein 2024-01-16 10:11:25 +1100
  • 77050f3034 docs+README: update Isabelle links to https Gerwin Klein 2024-01-16 10:05:16 +1100
  • fb2caf86bc c-parser+autocorres: update Simpl links Gerwin Klein 2024-01-16 10:03:42 +1100
  • c178c09eca lib: add Heap_List to ROOT Michael McInerney 2024-01-15 18:13:01 +1030
  • 1ea5d8b092 aarch64 machine+aspec+cspec: pt_type ghost+table array sizes Gerwin Klein 2024-01-04 11:15:22 +1100
  • e5895dbd64 lib: some sym_heap lemmas regarding heap updates Michael McInerney 2024-01-10 00:56:15 +1030
  • abc0990d4d lib: add "no loops" lemmas for heap_ls Michael McInerney 2024-01-10 00:34:40 +1030
  • 7fdfee1a00 lib: several miscellaneous lemmas for heap_ls Michael McInerney 2024-01-10 00:20:30 +1030
  • 7775f42bc9 lib: add fun_upd_swap Michael McInerney 2024-01-10 00:00:06 +1030
  • 992aa5f657 lib: add heap_path_sym_heap_non_nil_lookup_prev Michael McInerney 2024-01-09 23:55:31 +1030
  • 4ac9ff06ec lib: heap_ls lemmas relating an update to the list to an update to the heap Michael McInerney 2024-01-10 11:20:05 +1030
  • 650771902d lib: add Heap_List.thy, for reasoning about linked lists on heaps Michael McInerney 2024-01-10 11:15:36 +1030
  • 74d8f98e85 lib: add defn of list_insert_before, and some lemmas Michael McInerney 2024-01-10 10:54:38 +1030
  • f857b158a1 lib: add no_ofail_if Michael McInerney 2024-01-09 20:29:08 +1030
  • d212944e50 lib: add ovalid_post_taut Michael McInerney 2024-01-09 19:47:51 +1030
  • ff5e7da215 lib: modify no_ofail_obind and no_ofail_pre_imp Michael McInerney 2024-01-09 19:44:10 +1030
  • b94a78c88c lib: reorder assumptions of no_fail_bind Michael McInerney 2024-01-09 19:36:05 +1030
  • ea943b5a6d lib: add ifM_corres' and orM_corres' Michael McInerney 2024-01-09 19:07:18 +1030
  • d4dd05ca30 lib: add ifM_to_top_of_bind Michael McInerney 2024-01-09 19:07:01 +1030
  • e160e257a0 lib: add monadic_rewrite_corres_r_generic_ex_abs Michael McInerney 2024-01-09 18:21:47 +1030
  • e508d15554 lib: generalise monadic_rewrite_is_valid Michael McInerney 2024-01-09 18:21:26 +1030
  • 71255d25bf lib: add monadic_rewrite_guard_arg_cong Michael McInerney 2024-01-09 18:20:51 +1030
  • f03be1244c lib: strengthen no_ofail_gets_the Michael McInerney 2024-01-09 16:01:14 +1030
  • c840839ab7 lib: add some rules involving ex_abs_underlying, including corres_from_valid Michael McInerney 2024-01-09 15:59:19 +1030
  • 375b19261a lib: add corres_if_strong Michael McInerney 2024-01-09 15:57:11 +1030
  • 7493e71298 lib+refine: strengthen corres_assert_assume_l and move to Lib Michael McInerney 2024-01-09 15:51:44 +1030
  • 3daad13f39 clib: suppress simp warnings in simpl_rewrite Gerwin Klein 2024-01-13 09:26:36 +1100
  • cddd42ae76 lib: provide warning suppression for Eisbach methods Gerwin Klein 2024-01-13 09:24:38 +1100
  • 2b17160c2b github: add num_domains key to artifact upload Gerwin Klein 2023-12-12 11:55:41 +0100
  • 28197a5b9e runtest: echo NUM_DOMAINS override Gerwin Klein 2023-12-10 12:58:22 +0100
  • d2940797c4 github: add NUM_DOMAINS test matrix Gerwin Klein 2023-12-10 11:49:39 +0100
  • 6cc6e1b52f cspec/c: provide NUM_DOMAINS build override option Gerwin Klein 2023-12-10 11:44:14 +0100
  • e01e42943e github: docs for platform branch rebase workflow Gerwin Klein 2023-12-08 14:43:43 +0100
  • 8f0b505826 clib: further improvements to ccorres_While Michael McInerney 2023-12-02 13:10:41 +1030
  • 18640b8db6 arm-hyp crefine: update length to word_t for VCPU functions Rafal Kolanski 2023-12-05 13:23:58 +1100
  • 289bf94e2c autocorres: bring CONTRIBUTORS file up to date Gerwin Klein 2023-11-03 10:46:06 +1100
  • ee7c8101da autocorres: update release ROOT files and manifest Gerwin Klein 2023-11-03 10:21:48 +1100
  • c2e964eb3c autocorres: format ChangeLog Gerwin Klein 2023-11-03 10:15:34 +1100
  • 7bf0cbd8f2 autocorres: update change log for upcoming release Gerwin Klein 2023-11-03 10:12:07 +1100
  • f1f1027125 c-parser: update change log for upcoming release Gerwin Klein 2023-11-03 10:07:51 +1100
  • a881c04a37 autocorres: bump Isabelle version in docs Gerwin Klein 2023-11-03 10:02:09 +1100
  • fdaec17711 c-parser: bump Isabelle version in docs Gerwin Klein 2023-11-03 10:01:56 +1100
  • f2a0f7cfc9 c-parser: update mkrelease for changed lib sessions Gerwin Klein 2023-11-03 09:42:57 +1100
  • 550feb18dd c-parser: clarify mkrelease command line Gerwin Klein 2023-11-03 09:36:58 +1100
  • 02928556ff c-parser: remove obsolete mkrelease checks Gerwin Klein 2023-11-03 09:34:38 +1100
  • 65dabc2a0e cspec: adjust for kernel build change Gerwin Klein 2023-10-28 09:35:02 +1100
  • 4d19f6616f clib: improve ccorres_While Michael McInerney 2023-10-09 11:50:59 +1030
  • 5568eb56a1 clib+crefine: improve and consolidate variants of ccorres_to_vcg Michael McInerney 2023-10-06 20:09:31 +1030
  • 5b618c7fe4 clib: add some rules for hoarep Michael McInerney 2023-10-09 11:37:13 +1030
  • e122ad9d92 clib: improve ccorres_call_getter_setter Michael McInerney 2023-10-06 19:52:21 +1030
  • af3505401b lib/monads: remove more uses of _tac methods Corey Lewis 2023-10-13 10:08:01 +1100
  • ec1f38c8bc run_tests+proof: exclude SimplExportAndRefine for AARCH64 Gerwin Klein 2023-10-10 11:38:37 +1100
  • 5a5e5e363d proof: switch AArch64 quick_and_dirty from Refine to CRefine Gerwin Klein 2023-10-10 11:34:08 +1100
  • ab7fdfeebe run_tests: enable CBaseRefine for AARCH64 Rafal Kolanski 2023-08-18 12:09:46 +1000
  • 2f6771cb50 aarch64 cspec: add Kernel_C.thy to base CKernel image on Rafal Kolanski 2023-08-18 12:08:12 +1000
  • a22c624031 aarch64 asmrefine: copy ArchSetup from RISCV64 Rafal Kolanski 2023-08-18 12:05:50 +1000
  • f089db3448 lib/monads: avoid clarsimp as initial Isar method Gerwin Klein 2023-10-12 15:13:13 +1100
  • 5b5fb045d8 lib/monads: fix remaining document preparation issues Gerwin Klein 2023-10-12 14:42:49 +1100
  • 1182415f0c lib/monads: add new Trace_* files to ROOT Gerwin Klein 2023-10-12 14:34:37 +1100
  • cd40ce33a3 lib/monads: coherent document structure Gerwin Klein 2023-10-12 12:28:46 +1100
  • 9e06a820bf lib/monads: minor style + warning cleanup Gerwin Klein 2023-10-12 12:30:25 +1100
  • ab8b7d2e4d lib/monads: fix document preparation issues Gerwin Klein 2023-10-12 12:26:44 +1100
  • 35256907e9 lib/monads: add AFP document setup Gerwin Klein 2023-10-12 11:37:35 +1100
  • eb65c07d67 misc/scripts: remove Darwin cpp wrapper Gerwin Klein 2023-10-10 08:54:45 +1100
  • 3f12bcde49 If cpp_path is relative, make it relative to the current theory. Achim D. Brucker 2023-10-07 17:24:28 +0100
  • 76dbb29e7e docs: add a guide for commit messages umm_types_relative Gerwin Klein 2023-10-20 18:40:56 +1100
  • a2696127d0 c-parser: turn README into main C-parser website Gerwin Klein 2024-01-16 11:32:36 +1100
  • ea6477ba94 autocorres: update AFP links Gerwin Klein 2024-01-16 10:14:22 +1100
  • 18dd0deb8a autocorres: point C parser links to GitHub Gerwin Klein 2024-01-16 10:11:25 +1100
  • 591735d3e8 docs+README: update Isabelle links to https Gerwin Klein 2024-01-16 10:05:16 +1100
  • ffd76022d4 c-parser+autocorres: update Simpl links Gerwin Klein 2024-01-16 10:03:42 +1100
  • 8e9ba18e00 lib: add Heap_List to ROOT Michael McInerney 2024-01-15 18:13:01 +1030
  • 47fa26c8a8 aarch64 machine+aspec+cspec: pt_type ghost+table array sizes Gerwin Klein 2024-01-04 11:15:22 +1100
  • 5dd241022a lib: some sym_heap lemmas regarding heap updates Michael McInerney 2024-01-10 00:56:15 +1030
  • 0f999d6d39 lib: add "no loops" lemmas for heap_ls Michael McInerney 2024-01-10 00:34:40 +1030
  • 1def78d062 lib: several miscellaneous lemmas for heap_ls Michael McInerney 2024-01-10 00:20:30 +1030
  • 6b4c27b59b lib: add fun_upd_swap Michael McInerney 2024-01-10 00:00:06 +1030
  • bcf6e90a04 lib: add heap_path_sym_heap_non_nil_lookup_prev Michael McInerney 2024-01-09 23:55:31 +1030
  • e4e232ae25 lib: heap_ls lemmas relating an update to the list to an update to the heap Michael McInerney 2024-01-10 11:20:05 +1030
  • f65463b1b1 lib: add Heap_List.thy, for reasoning about linked lists on heaps Michael McInerney 2024-01-10 11:15:36 +1030
  • 3cf0afabc9 lib: add defn of list_insert_before, and some lemmas Michael McInerney 2024-01-10 10:54:38 +1030
  • a7f9a415e6 lib: add no_ofail_if Michael McInerney 2024-01-09 20:29:08 +1030
  • 92ad82ff79 lib: add ovalid_post_taut Michael McInerney 2024-01-09 19:47:51 +1030
  • be7ac0ee39 lib: modify no_ofail_obind and no_ofail_pre_imp Michael McInerney 2024-01-09 19:44:10 +1030
  • 31446bf80c lib: reorder assumptions of no_fail_bind Michael McInerney 2024-01-09 19:36:05 +1030
  • 63dd1bb027 lib: add ifM_corres' and orM_corres' Michael McInerney 2024-01-09 19:07:18 +1030
  • 6110badfda lib: add ifM_to_top_of_bind Michael McInerney 2024-01-09 19:07:01 +1030
  • f1f9a4f0be lib: add monadic_rewrite_corres_r_generic_ex_abs Michael McInerney 2024-01-09 18:21:47 +1030