Theory Voblint_Analysis_Sign.Sign_Analyses

theory Sign_Analyses
  imports
    Sign_Sound
    Sign_Classify
    "Voblint_Nonrelational.Nonrel_Registration"
begin

section ‹Registering Sign at every context and update rule›

text ‹
  Sign runs through the shared D/G pipeline at the unit context. The CLI runs it as a
  field of the combined state of ‹MCP_Analyses›, whose component and
  soundness the unit registration supplies. Each registration leaves the rule that
  merges a value side-effected into a global as a parameter ‹r›. The
  equation system, the solve, the result table and every soundness endpoint come from
  the interpreted locale; this theory only names the domain's own implementation and
  facts.
›

subsection ‹At the unit context›

global_interpretation sign_rule:
    nonrel_unit_rule sign_ops cinit_sign_st r
  for r
  by (intro nonrel_unit_ruleI nonrel_registrationI
      sign_tf.sound_nonrelational_ops_axioms sign_cinit_gamma)

end