diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2014-12-11 10:14:09 +0100 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2014-12-11 10:14:09 +0100 |
commit | 089a9c8d0eb0b44a12d4008739b7c1cbc9dccd14 (patch) | |
tree | 8b83547ac65690b9a7cae230a9d6195766095577 /ia32/ValueAOp.v | |
parent | b1345b1d0efec39850fb91dcc7e12d341b1a24fd (diff) | |
parent | 0342889a01aa16162232b0a87a4eb10bdb852ba4 (diff) | |
download | compcert-089a9c8d0eb0b44a12d4008739b7c1cbc9dccd14.tar.gz compcert-089a9c8d0eb0b44a12d4008739b7c1cbc9dccd14.zip |
Merge branch 'master' into dwarf
Diffstat (limited to 'ia32/ValueAOp.v')
-rw-r--r-- | ia32/ValueAOp.v | 13 |
1 files changed, 11 insertions, 2 deletions
diff --git a/ia32/ValueAOp.v b/ia32/ValueAOp.v index 874c2be3..53013337 100644 --- a/ia32/ValueAOp.v +++ b/ia32/ValueAOp.v @@ -58,7 +58,7 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | Ointconst n, nil => I n | Ofloatconst n, nil => if propagate_float_constants tt then F n else ftop | Osingleconst n, nil => if propagate_float_constants tt then FS n else ftop - | Oindirectsymbol id, nil => Ptr (Gl id Int.zero) + | Oindirectsymbol id, nil => Ifptr (Gl id Int.zero) | Ocast8signed, v1 :: nil => sign_ext 8 v1 | Ocast8unsigned, v1 :: nil => zero_ext 8 v1 | Ocast16signed, v1 :: nil => sign_ext 16 v1 @@ -145,7 +145,16 @@ Proof. intros; apply symbol_address_sound; apply GENV. Qed. -Hint Resolve symbol_address_sound: va. +Lemma symbol_address_sound_2: + forall id ofs, + vmatch bc (Genv.symbol_address ge id ofs) (Ifptr (Gl id ofs)). +Proof. + intros. unfold Genv.symbol_address. destruct (Genv.find_symbol ge id) as [b|] eqn:F. + constructor. constructor. apply GENV; auto. + constructor. +Qed. + +Hint Resolve symbol_address_sound symbol_address_sound_2: va. Ltac InvHyps := match goal with |