seL4 specification and proofs
Go to file
2024-01-27 14:09:25 +00:00
.github/workflows github: add num_domains key to artifact upload 2023-12-13 11:30:24 +01:00
.reuse spdx: provide dep5 file with license information 2020-03-16 14:19:15 +08:00
camkes camkes: update to Isabelle2023 mapsto syntax 2023-10-06 14:41:53 +11:00
docs docs: add a guide for commit messages 2024-01-17 15:21:41 +11:00
lib Renamed Word_Lib shipped by AutoCorres to Word_Lib_l4v to avoid a name clash with the AFP entry of same name. 2024-01-27 13:44:24 +00:00
LICENSES spdx: provide dep5 file with license information 2020-03-16 14:19:15 +08:00
misc Merge branch 'cpp_wrapper' 2024-01-27 13:47:10 +00:00
proof Renamed Word_Lib shipped by AutoCorres to Word_Lib_l4v to avoid a name clash with the AFP entry of same name. 2024-01-27 13:44:24 +00:00
spec Renamed Word_Lib shipped by AutoCorres to Word_Lib_l4v to avoid a name clash with the AFP entry of same name. 2024-01-27 13:44:24 +00:00
sys-init lib+proof: proof updates for wpc change 2023-06-15 09:52:15 +10:00
tools Merge branch 'autogenerated_parser' 2024-01-27 13:47:26 +00:00
.gitignore cspec: provide mechanism for adding dts overlays (#591) 2023-03-07 14:35:53 +11:00
.gitlint add gitlint configuration file 2020-04-19 11:28:45 +08:00
.licenseignore license: ignore generated file 2020-10-27 15:52:31 +10:00
.stylefilter stylefilter: do not check make_spec.sh 2022-04-20 09:16:19 +10:00
CODE_OF_CONDUCT.md Provide a link to the seL4 code of conduct 2020-04-02 00:07:22 +11:00
CONTRIBUTING.md contributing: link and contact info for TSC 2020-04-06 20:45:15 +08:00
CONTRIBUTORS.md lib: A tutorial and some 'modify' monad rules for Lib.EquivValid 2020-11-17 06:06:03 +11:00
isabelle release cleanup 2014-07-17 18:22:50 +02:00
LICENSE.md Update license information and move to LICENSE.md 2020-03-31 10:08:14 +08:00
README_l4v.md Updated repository description. 2024-01-27 14:09:25 +00:00
README.md Updated repository description. 2024-01-27 14:09:25 +00:00
ROOTS Renamed Word_Lib shipped by AutoCorres to Word_Lib_l4v to avoid a name clash with the AFP entry of same name. 2024-01-27 13:44:24 +00:00
run_tests runtest: echo NUM_DOMAINS override 2023-12-11 08:28:23 +01:00

A Fork of AutoCorres

This repository is a fork of the seL4/l4v repository. The main purpose is to maintain a local version of AutoCorres.

Each feature changed with respect to the upstream repository is tracked on its own branch.

The main brach (called "master") contains all features from the individual feature branches described below:

Active Branches

Branch "autogenerated_parser"

This branch adds the C-parser files generated by mllex and mlyacc to reduce dependencies required by users of AutoCorres.

Branch "renaming_Word_Lib"

This branch renames the session Word_Lib shipped by AutoCorres to Word_Lib_l4v to avoid a name clash with the AFP entry of same name. This allows one to use AutoCorres with the AFP being registered as an Isabelle component.

Branch "cpp_wrapper"

This branch adds an OS check to the cpp-wrapper script. This allows using the cpp wrapper on all supported operating systems, allowing a uniform declare [[cpp_path = "..."]] across all supported operating systems.

Obsolete Branches

Branch "cpp_path_relative"

This branch converts a relative cpp_path (e.g., declare [[cpp_path = "tools/cpp_wrapper"]] into an absolute path, relative to the theory using install_C_file. This minimized the need for local configuration that cannot be easily shared within a development team. This branch is now obsolete, as the corresponding PR has been accepted upstream.

Branch "umm_types_realtive"

Ensure that umm_types.txt is saved relative to theory file. This branch is now obsolete, as the corresponding PR has been accepted upstream.

Branch "isabelle2023"

This branch provides a port of AutoCorres (and AutoCorres only) to Isabelle 2023. This branch is now obsolete, as the upstream repository supports Isabelle 2023.