diff options
| -rw-r--r-- | common/Values.v | 21 |
1 files changed, 21 insertions, 0 deletions
diff --git a/common/Values.v b/common/Values.v index 4146dd59..5d32e54e 100644 --- a/common/Values.v +++ b/common/Values.v @@ -89,6 +89,27 @@ Definition has_type (v: val) (t: typ) : Prop := | _, _ => False end. +Definition has_type_b (v: val) (t: typ) := + match v, t with + | Vundef, _ => true + | Vint _, Tint => true + | Vlong _, Tlong => true + | Vfloat _, Tfloat => true + | Vsingle _, Tsingle => true + | Vptr _ _, Tint => negb Archi.ptr64 + | Vptr _ _, Tlong => Archi.ptr64 + | (Vint _ | Vsingle _), Tany32 => true + | Vptr _ _, Tany32 => negb Archi.ptr64 + | _, Tany64 => true + | _, _ => false + end. + +Lemma has_type_b_correct: forall v t, + has_type_b v t = true <-> has_type v t. +Proof. + destruct v; destruct t; cbn; destruct Archi.ptr64; cbn; split; intros; auto; discriminate. +Qed. + Fixpoint has_type_list (vl: list val) (tl: list typ) {struct vl} : Prop := match vl, tl with | nil, nil => True |