Merge remote-tracking branch 'origin/mppa-licm' into mppa-features

2 files changed, 10 insertions, 3 deletions

diff --git a/arm/Archi.v b/arm/Archi.v
index 16d6c71d..738341cc 100644
--- a/arm/Archi.v
+++ b/arm/Archi.v
@@ -97,3 +97,5 @@ Parameter abi: abi_kind.
 (** Whether instructions added with Thumb2 are supported. True for ARMv6T2
   and above. *)
 Parameter thumb2_support: bool.
+
+Definition has_notrap_loads := false.
diff --git a/arm/Op.v b/arm/Op.v
index 671bdbe4..25e48ce1 100644
--- a/arm/Op.v
+++ b/arm/Op.v
@@ -531,14 +531,19 @@ Definition is_trapping_op (op : operation) :=
   end.
                 
 
+Definition args_of_operation op :=
+  if eq_operation op Omove
+  then 1%nat
+  else List.length (fst (type_of_operation op)).
+
 Lemma is_trapping_op_sound:
   forall op vl sp m,
-    op <> Omove ->
     is_trapping_op op = false ->
-    (List.length vl) = (List.length (fst (type_of_operation op))) ->
+    (List.length vl) = args_of_operation op ->
     eval_operation genv sp op vl m <> None.
 Proof.
-  destruct op; intros; simpl in *; try congruence.
+  unfold args_of_operation.
+  destruct op; destruct eq_operation; intros; simpl in *; try congruence.
   all: try (destruct vl as [ | vh1 vl1]; try discriminate).
   all: try (destruct vl1 as [ | vh2 vl2]; try discriminate).
   all: try (destruct vl2 as [ | vh3 vl3]; try discriminate).