diff options
Diffstat (limited to 'arm/Op.v')
| -rw-r--r-- | arm/Op.v | 20 |
1 files changed, 4 insertions, 16 deletions
@@ -307,7 +307,7 @@ Definition type_of_operation (op: operation) : list typ * typ := match op with | Omove => (nil, Tint) (* treated specially *) | Ointconst _ => (nil, Tint) - | Ofloatconst _ => (nil, Tfloat) + | Ofloatconst f => (nil, if Float.is_single_dec f then Tsingle else Tfloat) | Oaddrsymbol _ _ => (nil, Tint) | Oaddrstack _ => (nil, Tint) | Oadd => (Tint :: Tint :: nil, Tint) @@ -345,7 +345,7 @@ Definition type_of_operation (op: operation) : list typ * typ := | Osubf => (Tfloat :: Tfloat :: nil, Tfloat) | Omulf => (Tfloat :: Tfloat :: nil, Tfloat) | Odivf => (Tfloat :: Tfloat :: nil, Tfloat) - | Osingleoffloat => (Tfloat :: nil, Tfloat) + | Osingleoffloat => (Tfloat :: nil, Tsingle) | Ointoffloat => (Tfloat :: nil, Tint) | Ointuoffloat => (Tfloat :: nil, Tint) | Ofloatofint => (Tint :: nil, Tfloat) @@ -384,6 +384,7 @@ Proof with (try exact I). intros. destruct op; simpl; simpl in H0; FuncInv; try subst v... congruence. + destruct (Float.is_single_dec f); red; auto. unfold symbol_address. destruct (Genv.find_symbol genv i)... destruct sp... destruct v0; destruct v1... @@ -422,7 +423,7 @@ Proof with (try exact I). destruct v0; destruct v1... destruct v0; destruct v1... destruct v0; destruct v1... - destruct v0... + destruct v0... simpl. apply Float.singleoffloat_is_single. destruct v0; simpl in H0; inv H0. destruct (Float.intoffloat f); simpl in H2; inv H2... destruct v0; simpl in H0; inv H0. destruct (Float.intuoffloat f); simpl in H2; inv H2... destruct v0; simpl in H0; inv H0... @@ -433,19 +434,6 @@ Proof with (try exact I). destruct (eval_condition c vl m)... destruct b... Qed. -Lemma type_of_chunk_correct: - forall chunk m addr v, - Mem.loadv chunk m addr = Some v -> - Val.has_type v (type_of_chunk chunk). -Proof. - intro chunk. - assert (forall v, Val.has_type (Val.load_result chunk v) (type_of_chunk chunk)). - destruct v; destruct chunk; exact I. - intros until v. unfold Mem.loadv. - destruct addr; intros; try discriminate. - eapply Mem.load_type; eauto. -Qed. - End SOUNDNESS. (** * Manipulating and transforming operations *) |