diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-09-21 19:13:07 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-09-21 19:13:07 +0200 |
| commit | 4b9b0e8f988cdfa1f848919b41bfe24c6e9a052a (patch) | |
| tree | 0068ca2f3c45ffb7e07db62d681ccd3b96bcb167 /backend/RTLgenspec.v | |
| parent | a34b64ee2e7a535ebc0fc731243ab520c4ba430f (diff) | |
| parent | 9147350fdb47f3471ce6d9202b7c996f79ffab2d (diff) | |
| download | compcert-4b9b0e8f988cdfa1f848919b41bfe24c6e9a052a.tar.gz compcert-4b9b0e8f988cdfa1f848919b41bfe24c6e9a052a.zip | |
Merge branch 'debugscopes' into debug_locations
Conflicts:
debug/CtoDwarf.ml
debug/DwarfPrinter.ml
Diffstat (limited to 'backend/RTLgenspec.v')
| -rw-r--r-- | backend/RTLgenspec.v | 18 |
1 files changed, 12 insertions, 6 deletions
diff --git a/backend/RTLgenspec.v b/backend/RTLgenspec.v index 41b5016f..1e665002 100644 --- a/backend/RTLgenspec.v +++ b/backend/RTLgenspec.v @@ -814,7 +814,10 @@ Inductive tr_builtin_res: mapping -> builtin_res ident -> builtin_res reg -> Pro map.(map_vars)!id = Some r -> tr_builtin_res map (BR id) (BR r) | tr_builtin_res_none: forall map, - tr_builtin_res map BR_none BR_none. + tr_builtin_res map BR_none BR_none + | tr_builtin_res_fresh: forall map r, + ~reg_in_map map r -> + tr_builtin_res map BR_none (BR r). (** [tr_stmt c map stmt ns ncont nexits nret rret] holds if the graph [c], starting at node [ns], contains instructions that perform the Cminor @@ -1214,14 +1217,17 @@ Proof. Qed. Lemma convert_builtin_res_charact: - forall map res s res' s' INCR - (TR: convert_builtin_res map res s = OK res' s' INCR) + forall map oty res s res' s' INCR + (TR: convert_builtin_res map oty res s = OK res' s' INCR) (WF: map_valid map s), tr_builtin_res map res res'. Proof. - destruct res; simpl; intros; monadInv TR. -- constructor. unfold find_var in EQ. destruct (map_vars map)!x; inv EQ; auto. -- constructor. + destruct res; simpl; intros. +- monadInv TR. constructor. unfold find_var in EQ. destruct (map_vars map)!x; inv EQ; auto. +- destruct oty; monadInv TR. ++ constructor. eauto with rtlg. ++ constructor. +- monadInv TR. Qed. Lemma transl_stmt_charact: |