summaryrefslogtreecommitdiff
path: root/common
diff options
context:
space:
mode:
Diffstat (limited to 'common')
-rw-r--r--common/Errors.v40
-rw-r--r--common/Memdataaux.ml1
-rw-r--r--common/Values.v6
3 files changed, 45 insertions, 2 deletions
diff --git a/common/Errors.v b/common/Errors.v
index 2165db3..36e70c5 100644
--- a/common/Errors.v
+++ b/common/Errors.v
@@ -93,10 +93,37 @@ Proof.
intros; discriminate.
Qed.
-Open Local Scope error_monad_scope.
+(** Assertions *)
+
+Definition assertion (b: bool) : res unit :=
+ if b then OK tt else Error(msg "Assertion failed").
+
+Remark assertion_inversion:
+ forall b x, assertion b = OK x -> b = true.
+Proof.
+ unfold assertion; intros. destruct b; inv H; auto.
+Qed.
+
+Remark assertion_inversion_1:
+ forall (P Q: Prop) (a: {P}+{Q}) x,
+ assertion (proj_sumbool a) = OK x -> P.
+Proof.
+ intros. exploit assertion_inversion; eauto.
+ unfold proj_sumbool. destruct a. auto. congruence.
+Qed.
+
+Remark assertion_inversion_2:
+ forall (P Q: Prop) (a: {P}+{Q}) x,
+ assertion (negb(proj_sumbool a)) = OK x -> Q.
+Proof.
+ intros. exploit assertion_inversion; eauto.
+ unfold proj_sumbool. destruct a; simpl. congruence. auto.
+Qed.
(** This is the familiar monadic map iterator. *)
+Open Local Scope error_monad_scope.
+
Fixpoint mmap (A B: Type) (f: A -> res B) (l: list A) {struct l} : res (list B) :=
match l with
| nil => OK nil
@@ -152,6 +179,15 @@ Ltac monadInv1 H :=
destruct (bind2_inversion F G H) as [x1 [x2 [EQ1 EQ2]]];
clear H;
try (monadInv1 EQ2)))))
+ | (assertion (negb (proj_sumbool ?a)) = OK ?X) =>
+ let A := fresh "A" in (generalize (assertion_inversion_2 _ H); intro A);
+ clear H
+ | (assertion (proj_sumbool ?a) = OK ?X) =>
+ let A := fresh "A" in (generalize (assertion_inversion_1 _ H); intro A);
+ clear H
+ | (assertion ?b = OK ?X) =>
+ let A := fresh "A" in (generalize (assertion_inversion _ H); intro A);
+ clear H
| (mmap ?F ?L = OK ?M) =>
generalize (mmap_inversion F L H); intro
end.
@@ -162,6 +198,7 @@ Ltac monadInv H :=
| (Error _ = OK _) => monadInv1 H
| (bind ?F ?G = OK ?X) => monadInv1 H
| (bind2 ?F ?G = OK ?X) => monadInv1 H
+ | (assertion _ = OK _) => monadInv1 H
| (?F _ _ _ _ _ _ _ _ = OK _) =>
((progress simpl in H) || unfold F in H); monadInv1 H
| (?F _ _ _ _ _ _ _ = OK _) =>
@@ -179,4 +216,3 @@ Ltac monadInv H :=
| (?F _ = OK _) =>
((progress simpl in H) || unfold F in H); monadInv1 H
end.
-
diff --git a/common/Memdataaux.ml b/common/Memdataaux.ml
index 0ec7523..8bfd434 100644
--- a/common/Memdataaux.ml
+++ b/common/Memdataaux.ml
@@ -14,4 +14,5 @@ let big_endian =
match Configuration.arch with
| "powerpc" -> true
| "arm" -> false
+ | "ia32" -> false
| _ -> assert false
diff --git a/common/Values.v b/common/Values.v
index 236a5ae..af242c9 100644
--- a/common/Values.v
+++ b/common/Values.v
@@ -139,6 +139,12 @@ Definition floatofintu (v: val) : val :=
| _ => Vundef
end.
+Definition floatofwords (v1 v2: val) : val :=
+ match v1, v2 with
+ | Vint n1, Vint n2 => Vfloat (Float.from_words n1 n2)
+ | _, _ => Vundef
+ end.
+
Definition notint (v: val) : val :=
match v with
| Vint n => Vint (Int.xor n Int.mone)