Theory Voblint_Analysis_Interval.Interval_Analyses

theory Interval_Analyses
  imports
    Interval_Sound
    Interval_Classify
    "Voblint_Nonrelational.Nonrel_Registration"
begin

section ‹Registering Interval at every context and update rule›

text ‹
  Interval runs through the shared D/G pipeline at the unit context, keyed by the
  abstract values a callee's formals hold on entry, and keyed by a bounded call
  string. 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›, and the call-string one also its bound
  ‹k›. 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 interval_rule:
    nonrel_unit_rule ivl_ops cinit_ivl_st r
  for r
  by (intro nonrel_unit_ruleI nonrel_registrationI
      ivl_tf.sound_nonrelational_ops_axioms interval_cinit_gamma)

subsection ‹At the entry-state context›

text ‹
  A callee is keyed by the abstract values its formals hold on entry.
›

global_interpretation interval_es_rule:
    nonrel_es_rule ivl_ops cinit_ivl_st r
  for r
  by (intro nonrel_es_ruleI nonrel_registrationI
      ivl_tf.sound_nonrelational_ops_axioms interval_cinit_gamma)

subsection ‹At the call-string context›

text ‹
  A callee is keyed by its last ‹k› call sites.
›

global_interpretation interval_cs_rule:
    nonrel_cs_rule ivl_ops cinit_ivl_st k r
  for k r
  by (intro nonrel_cs_ruleI nonrel_registrationI
      ivl_tf.sound_nonrelational_ops_axioms interval_cinit_gamma)

end