Theory Voblint_Analysis_Sign.Sign_Exec

theory Sign_Exec
  imports
    Sign_Transfer
begin

section ‹Sign on the executable carrier›

text ‹
  The executable step and procedure entry are \<^theory>‹Voblint_Nonrelational.Nonrelational_Ops›'s
  generic constructions at the bundle, ‹generic_tf_st_for sign_ops› and
  ‹generic_enter_st_for sign_ops›, and their agreement with the abstract transfer is
  ‹sign_tf.tf_st_for_commute› and ‹sign_tf.enter_st_for_commute›: nothing about them
  is the domain's to state.
›

text ‹The state a run starts in: a declared global holds ‹SZero›, a local ‹STop›.›

abbreviation cinit_sign_st :: "sign default_st" where
  "cinit_sign_st ≡ initial_default_st STop SZero"

end