diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-10-20 13:32:18 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-10-20 13:32:18 +0200 |
| commit | 4d542bc7eafadb16b845cf05d1eb4988eb55ed0f (patch) | |
| tree | 1961b41815fc6e392cc0bd2beeb0fb504bc160ce /backend/Debugvar.v | |
| parent | 7a6bb90048db7a254e959b1e3c308bac5fe6c418 (diff) | |
| download | compcert-kvx-4d542bc7eafadb16b845cf05d1eb4988eb55ed0f.tar.gz compcert-kvx-4d542bc7eafadb16b845cf05d1eb4988eb55ed0f.zip | |
Updated PR by removing whitespaces. Bug 17450.
Diffstat (limited to 'backend/Debugvar.v')
| -rw-r--r-- | backend/Debugvar.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/backend/Debugvar.v b/backend/Debugvar.v index 314f43fd..dcc4327a 100644 --- a/backend/Debugvar.v +++ b/backend/Debugvar.v @@ -10,7 +10,7 @@ (* *) (* *********************************************************************) -(** Computation of live ranges for local variables that carry +(** Computation of live ranges for local variables that carry debugging information. *) Require Import Coqlib. @@ -154,7 +154,7 @@ Definition eq_debuginfo (i1 i2: debuginfo) : {i1=i2} + {i1 <> i2}. Proof. destruct (eq_arg (proj1_sig i1) (proj1_sig i2)). left. destruct i1, i2; simpl in *. subst x0. f_equal. apply proof_irr. - right. congruence. + right. congruence. Defined. Global Opaque eq_debuginfo. @@ -177,7 +177,7 @@ Fixpoint join (s1: avail) (s2: avail) {struct s1} : avail := Definition eq_state (s1 s2: avail) : {s1=s2} + {s1<>s2}. Proof. - apply list_eq_dec. decide equality. apply eq_debuginfo. apply ident_eq. + apply list_eq_dec. decide equality. apply eq_debuginfo. apply ident_eq. Defined. Global Opaque eq_state. @@ -273,7 +273,7 @@ Definition transfer (lm: labelmap) (before: option avail) (i: instruction): end end. -(** One pass of forward analysis over the code [c]. +(** One pass of forward analysis over the code [c]. Return an updated label map. *) Fixpoint ana_code (lm: labelmap) (before: option avail) (c: code) : labelmap := |