(* * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) * Copyright (c) 2022 Apple Inc. All rights reserved. * * SPDX-License-Identifier: BSD-2-Clause *) theory Kmalloc imports "AutoCorres2_Main.AutoCorres_Main" begin (* No proof here, just testing the parser. *) consts KMC :: addr ptr_retyps :: "nat ⇒ addr ⇒ heap_typ_desc ⇒ heap_typ_desc"