Library Main

Require Import
  Utf8
  Util AdomLib
  Goto GotoSem AbGoto DebugMemDom
  GotoAnalysis
  FirstGotoAnalysis.

Theorem first_analysis_sound (P: memory) (dom: list addr) (fuel: nat) (ab_num: num_domain_index) :
  ∀ mem_debug max_deref widen_oracle,
  first_analysis ab_num mem_debug max_deref widen_oracle P dom fuel ≠ None →
  safe P.


Theorem analysis_sound (P: memory) dom fuel:
  ∀ idx mem_debug max_deref widen_oracle δ,
  analysis idx mem_debug max_deref widen_oracle P dom δ fuel ≠ None →
  safe P.