Track the locations of local variables using EF_debug annotations.

SimplLocals:
- record locations of stack-allocated variables with annotations
  (of kind 5) at the beginning of the function;
- mark every assignment to non-stack-allocated variables with an
  annotation of kind 2.

Debugvar: (new pass!)
- perform availability analysis for debug annotations of kind 2
- insert "start of live range" and "end of live range" annotations
  (kind 3 and 4) to delimit intervals of PCs where the location
  of a local variable is known.

1 files changed, 1 insertions, 0 deletions

diff --git a/Makefile b/Makefile
index 0a13bf4b..1bf53bff 100644
--- a/Makefile
+++ b/Makefile
@@ -83,6 +83,7 @@ BACKEND=\
   Linear.v Lineartyping.v \
   Linearize.v Linearizeproof.v \
   CleanupLabels.v CleanupLabelsproof.v \
+  Debugvar.v Debugvarproof.v \
   Mach.v \
   Bounds.v Stacklayout.v Stacking.v Stackingproof.v \
   Asm.v Asmgen.v Asmgenproof0.v Asmgenproof1.v Asmgenproof.v