Theory Int_Fixpoint_Analyses

theory Int_Fixpoint_Analyses
  imports
    Int_Sound
    "Voblint_Nonrelational.Nonrel_Registration"
begin

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

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

end