Module Main

Require Import
  Utf8
  Coqlib Values Maps
  Memory IntervalDomain AbMem
  CFG CFGAnalysis CFGAnalysis_proof.

Theorem value_analysis_sound : forall
  (p: program)
  (stk: list stackframe) (f: function)
  (sp: val) (pc: node) (e: env) (m: Mem.mem)
  (k: num_dom_kind),
    Reach p (State stk f sp pc e m) →
    match vanalysis k f pc with
      | Bot => False
      | NotBot range =>
        ∀ x v,
          PTree.get x e = Some v →
          match v with
            | Vint i
            | Vptr _ i => ints_in_range (range x) i
            | _ => True
          end
    end.