diff options
| author | Jacques-Henri Jourdan <jacques-henri.jourdan@inria.fr> | 2015-11-04 03:04:21 +0100 |
|---|---|---|
| committer | Jacques-Henri Jourdan <jacques-henri.jourdan@inria.fr> | 2015-11-04 03:04:21 +0100 |
| commit | 5664fddcab15ef4482d583673c75e07bd1e96d0a (patch) | |
| tree | 878b22860e69405ba5cf6fd2798731dac8ce660c /backend/Debugvar.v | |
| parent | b960c83725d7e185ac5c6e3c0d6043c7dcd2f556 (diff) | |
| parent | fe73ed58ef80da7c53c124302a608948fb190229 (diff) | |
| download | compcert-5664fddcab15ef4482d583673c75e07bd1e96d0a.tar.gz compcert-5664fddcab15ef4482d583673c75e07bd1e96d0a.zip | |
Merge remote-tracking branch 'origin/master' into parser_fix
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 := |