Extend annotations so that they can keep track of global variables and local variables whose address is taken.

- CminorSel, RTL: add "annot" instructions.
- CminorSel to Asm: use type "annot_arg" for arguments of "annot" instructions.
- AST, Events: simplify EF_annot because constants are now part of the arguments.

Implementation is not complete yet.

1 files changed, 2 insertions, 2 deletions

diff --git a/backend/Bounds.v b/backend/Bounds.v
index bcd28487..249ff796 100644
--- a/backend/Bounds.v
+++ b/backend/Bounds.v
@@ -69,7 +69,7 @@ Definition instr_within_bounds (i: instruction) :=
   | Lbuiltin ef args res =>
       forall r, In r res \/ In r (destroyed_by_builtin ef) -> mreg_within_bounds r
   | Lannot ef args =>
-      forall sl ofs ty, In (S sl ofs ty) args -> slot_within_bounds sl ofs ty
+      forall sl ofs ty, In (S sl ofs ty) (params_of_annot_args args) -> slot_within_bounds sl ofs ty
   | _ => True
   end.
 
@@ -121,7 +121,7 @@ Definition slots_of_instr (i: instruction) : list (slot * Z * typ) :=
   match i with
   | Lgetstack sl ofs ty r => (sl, ofs, ty) :: nil
   | Lsetstack r sl ofs ty => (sl, ofs, ty) :: nil
-  | Lannot ef args => slots_of_locs args
+  | Lannot ef args => slots_of_locs (params_of_annot_args args)
   | _ => nil
   end.