(*
 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
 *
 * SPDX-License-Identifier: BSD-2-Clause
 *)

theory GhostAssertions

imports "CParser.CTranslation"

begin

text \<open>Some framework constants for adding assertion data to the ghost
state and accessing it. These constants don't do much, but using them
allows the SimplExport mechanism to recognise the intent of ghost state
operations.\<close>

end