Theory Int_Once_Analyses

theory Int_Once_Analyses
  imports
    Int_Sound
    "Voblint_Nonrelational.Nonrel_Registration"
begin

section ‹Registering Int under \<^const>‹Refine_Once› at every context and update rule›

text ‹
  Int under \<^const>‹Refine_Once› 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 int_once_rule:
    nonrel_unit_rule "int_dom_ops Refine_Once" cinit_int_dom_st r
  for r
  by (intro nonrel_unit_ruleI nonrel_registrationI
      int_tf.sound_nonrelational_ops_axioms int_cinit_gamma)

end