diff options
Diffstat (limited to 'common')
-rw-r--r-- | common/DebugPrint.ml | 2 | ||||
-rw-r--r-- | common/Values.v | 21 |
2 files changed, 22 insertions, 1 deletions
diff --git a/common/DebugPrint.ml b/common/DebugPrint.ml index f68432d9..6f8449ee 100644 --- a/common/DebugPrint.ml +++ b/common/DebugPrint.ml @@ -5,7 +5,7 @@ open Registers let debug_flag = ref false let debug fmt = - if !debug_flag then (flush stderr; Printf.eprintf fmt) + if !debug_flag then (flush stderr; flush stdout; Printf.eprintf fmt) else Printf.ifprintf stderr fmt let print_ptree_bool oc pt = 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 |