Module VIntDomain

Require Import Coqlib.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Op.
Require Import Utils.
Require Import LatticeSignatures.
Require Import CfgIterator.


Module MustVInt.

Inductive t := VI | Top.

Definition le (x y:t) : bool :=
    match x,y with
      | VI, _ | _, Top => true | _,_ => false
    end.

Definition gamma (ab:t) (v:val) : Prop :=
  match ab, v with
    | VI, Vint i => True
    | Top, _ => True
    | _, _ => False
  end.

Definition join (i1 i2: t) : t :=
  match i1, i2 with
    | VI, VI => VI
    | _, _ => Top
  end.

Definition widen := join.

Definition top := Top.

  Lemma gamma_top : forall v,
    gamma top v.

  Lemma gamma_monotone : forall ab1 ab2,
    le ab1 ab2 = true -> forall v, gamma ab1 v -> gamma ab2 v.

  Definition wlat : WLattice.t t val :=
   (WLattice.make _ _
    le
    top
    join
    widen
    gamma
    gamma_monotone
    gamma_top ).


End MustVInt.