Globalenvs: allocate one-byte block with permissions Nonempty for each

  function definition, so that comparisons between function pointers
  are correctly defined.
AST, Globalenvs, and many other files:
  represent programs as a list of (function or variable) definitions
  instead of two lists, one for functions and the other for variables.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2067 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

18 files changed, 127 insertions, 148 deletions

diff --git a/backend/CMparser.mly b/backend/CMparser.mly
index aec0a5e..a62bd74 100644
--- a/backend/CMparser.mly
+++ b/backend/CMparser.mly
@@ -307,10 +307,9 @@ let mkmatch expr cases =
 /* Programs */
 
 prog:
-    global_declarations proc_list EOF
-      { { prog_funct = List.rev $2;
-          prog_main = intern_string "main";
-          prog_vars = List.rev $1; } }
+    global_declarations EOF
+      { { prog_defs = List.rev $1;
+          prog_main = intern_string "main" } }
 ;
 
 global_declarations:
@@ -319,12 +318,14 @@ global_declarations:
 ;
 
 global_declaration:
-    VAR STRINGLIT LBRACKET INTLIT RBRACKET  /* old style */
-      { ($2, {gvar_info = (); gvar_init = [Init_space(z_of_camlint $4)];
-              gvar_readonly = false; gvar_volatile = false}) }
+    proc
+      { $1 }
+  | VAR STRINGLIT LBRACKET INTLIT RBRACKET  /* old style */
+      { ($2, Gvar{gvar_info = (); gvar_init = [Init_space(z_of_camlint $4)];
+                  gvar_readonly = false; gvar_volatile = false}) }
   | VAR STRINGLIT is_readonly is_volatile LBRACE init_data_list RBRACE
-       { ($2, {gvar_info = (); gvar_init = List.rev $6;
-               gvar_readonly = $3; gvar_volatile = $4; } ) }
+       { ($2, Gvar{gvar_info = (); gvar_init = List.rev $6;
+                   gvar_readonly = $3; gvar_volatile = $4; } ) }
 ;
 
 is_readonly:
@@ -359,12 +360,6 @@ init_data:
    | INTLIT LPAREN STRINGLIT RPAREN              { Init_addrof ($3, coqint_of_camlint $1) }
  ;
  
-
-proc_list:
-    /* empty */                                 { [] }
-  | proc_list proc                              { $2 :: $1 }
-;
-
 /* Procedures */
 
 proc:
@@ -378,13 +373,13 @@ proc:
         temporaries := [];
         temp_counter := 0;
         ($1,
-        Internal { fn_sig = $6;
-                   fn_params = List.rev $3;
-                   fn_vars = List.rev (tmp @ $9);
-                   fn_stackspace = $8;
-                   fn_body = $10 }) }
+        Gfun(Internal { fn_sig = $6;
+                        fn_params = List.rev $3;
+                        fn_vars = List.rev (tmp @ $9);
+                        fn_stackspace = $8;
+                        fn_body = $10 })) }
   | EXTERN STRINGLIT COLON signature 
-      { ($2, External(EF_external($2,$4))) }
+      { ($2, Gfun(External(EF_external($2,$4)))) }
 ;
 
 signature:
diff --git a/backend/CMtypecheck.ml b/backend/CMtypecheck.ml
index 4070785..408e9ec 100644
--- a/backend/CMtypecheck.ml
+++ b/backend/CMtypecheck.ml
@@ -349,10 +349,11 @@ let type_function id f =
   with Error s ->
     raise (Error (sprintf "In function %s:\n%s" (extern_atom id) s))
 
-let type_fundef (id, fd) =
-  match fd with
-  | Internal f -> type_function id f
-  | External ef -> ()
+let type_globdef (id, gd) =
+  match gd with
+  | Gfun(Internal f) -> type_function id f
+  | Gfun(External ef) -> ()
+  | Gvar v -> ()
 
 let type_program p =
-  List.iter type_fundef p.prog_funct; p
+  List.iter type_globdef p.prog_defs; p
diff --git a/backend/Constprop.v b/backend/Constprop.v
index 104aa3b..fc242e1 100644
--- a/backend/Constprop.v
+++ b/backend/Constprop.v
@@ -368,17 +368,21 @@ Definition transf_function (gapp: global_approx) (f: function) : function :=
 Definition transf_fundef (gapp: global_approx) (fd: fundef) : fundef :=
   AST.transf_fundef (transf_function gapp) fd.
 
-Fixpoint make_global_approx (gapp: global_approx) (vars: list (ident * globvar unit)) : global_approx :=
-  match vars with
+Fixpoint make_global_approx (gapp: global_approx) (gdl: list (ident * globdef fundef unit)): global_approx :=
+  match gdl with
   | nil => gapp
-  | (id, gv) :: vars' =>
+  | (id, gl) :: gdl' =>
       let gapp1 :=
-        if gv.(gvar_readonly) && negb gv.(gvar_volatile)
-        then PTree.set id gv.(gvar_init) gapp
-        else PTree.remove id gapp in
-      make_global_approx gapp1 vars'
+        match gl with
+        | Gfun f => PTree.remove id gapp
+        | Gvar gv =>
+            if gv.(gvar_readonly) && negb gv.(gvar_volatile)
+            then PTree.set id gv.(gvar_init) gapp
+            else PTree.remove id gapp
+        end in
+      make_global_approx gapp1 gdl'
   end.
 
 Definition transf_program (p: program) : program :=
-  let gapp := make_global_approx (PTree.empty _) p.(prog_vars) in
+  let gapp := make_global_approx (PTree.empty _) p.(prog_defs) in
   transform_program (transf_fundef gapp) p.
diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v
index 8228493..f14e87a 100644
--- a/backend/Constpropproof.v
+++ b/backend/Constpropproof.v
@@ -37,7 +37,7 @@ Variable prog: program.
 Let tprog := transf_program prog.
 Let ge := Genv.globalenv prog.
 Let tge := Genv.globalenv tprog.
-Let gapp := make_global_approx (PTree.empty _) prog.(prog_vars).
+Let gapp := make_global_approx (PTree.empty _) prog.(prog_defs).
 
 (** * Correctness of the static analysis *)
 
@@ -279,31 +279,34 @@ Definition global_approx_charact (g: genv) (ga: global_approx) : Prop :=
   Genv.find_var_info g b = Some (mkglobvar tt il true false).
 
 Lemma make_global_approx_correct:
-  forall vl g ga,
+  forall gdl g ga,
   global_approx_charact g ga ->
-  global_approx_charact (Genv.add_variables g vl) (make_global_approx ga vl).
+  global_approx_charact (Genv.add_globals g gdl) (make_global_approx ga gdl).
 Proof.
-  induction vl; simpl; intros.
+  induction gdl; simpl; intros.
   auto.
-  destruct a as [id gv]. apply IHvl. 
+  destruct a as [id gd]. apply IHgdl. 
   red; intros. 
-  assert (EITHER: id0 = id /\ gv = mkglobvar tt il true false
+  assert (EITHER: id0 = id /\ gd = Gvar(mkglobvar tt il true false)
                \/ id0 <> id /\ ga!id0 = Some il).
-  destruct (gvar_readonly gv && negb (gvar_volatile gv)) as []_eqn.
+  destruct gd.
+  rewrite PTree.grspec in H0. destruct (PTree.elt_eq id0 id); [discriminate|auto].
+  destruct (gvar_readonly v && negb (gvar_volatile v)) as []_eqn.
   rewrite PTree.gsspec in H0. destruct (peq id0 id).
   inv H0. left. split; auto. 
-  destruct gv; simpl in *. 
+  destruct v; simpl in *. 
   destruct gvar_readonly; try discriminate.
   destruct gvar_volatile; try discriminate.
   destruct gvar_info. auto.
-  right; auto.
-  rewrite PTree.grspec in H0. destruct (PTree.elt_eq id0 id); try discriminate.
-  right; auto.
-  unfold Genv.add_variable, Genv.find_symbol, Genv.find_var_info in *;
+  auto.
+  rewrite PTree.grspec in H0. destruct (PTree.elt_eq id0 id); [discriminate|auto].
+
+  unfold Genv.add_global, Genv.find_symbol, Genv.find_var_info in *;
   simpl in *.
   destruct EITHER as [[A B] | [A B]].
   subst id0. rewrite PTree.gss in H1. inv H1. rewrite ZMap.gss. auto.
-  rewrite PTree.gso in H1; auto. rewrite ZMap.gso. eapply H. eauto. auto.
+  rewrite PTree.gso in H1; auto. destruct gd. eapply H; eauto. 
+  rewrite ZMap.gso. eapply H; eauto.
   exploit Genv.genv_symb_range; eauto. unfold ZIndexed.t. omega.
 Qed.
 
diff --git a/backend/Inlining.v b/backend/Inlining.v
index 406447b..3ddfe9a 100644
--- a/backend/Inlining.v
+++ b/backend/Inlining.v
@@ -28,7 +28,7 @@ Ltac xomega := unfold Plt, Ple in *; zify; omega.
 (** ** Environment of inlinable functions *)
 
 (** We maintain a mapping from function names to their definitions.
-  In this mapping, we only include functions that are eligible for
+  In this mapping, we only include internal functions that are eligible for
   inlining, as determined by the external heuristic
   [should_inline]. *)
 
@@ -38,22 +38,18 @@ Definition size_fenv (fenv: funenv) := PTree_Properties.cardinal fenv.
 
 Parameter should_inline: ident -> function -> bool.
 
-Definition add_fundef (fenv: funenv) (idf: ident * fundef) : funenv :=
-  match idf with
-  | (id, External ef) =>
-      PTree.remove id fenv
-  | (id, Internal f) =>
+Definition add_globdef (fenv: funenv) (idg: ident * globdef fundef unit) : funenv :=
+  match idg with
+  | (id, Gfun (Internal f)) =>
       if should_inline id f
       then PTree.set id f fenv
       else PTree.remove id fenv
+  | (id, _) =>
+      PTree.remove id fenv
   end.
 
-Definition remove_vardef (fenv: funenv) (idv: ident * globvar unit) : funenv :=
-  PTree.remove (fst idv) fenv.
-
 Definition funenv_program (p: program) : funenv :=
-  List.fold_left remove_vardef p.(prog_vars)
-    (List.fold_left add_fundef p.(prog_funct) (PTree.empty function)).
+  List.fold_left add_globdef p.(prog_defs) (PTree.empty function).
 
 (** Resources used by a function. *)
 
diff --git a/backend/Inliningproof.v b/backend/Inliningproof.v
index 9ca351a..8de8487 100644
--- a/backend/Inliningproof.v
+++ b/backend/Inliningproof.v
@@ -358,7 +358,8 @@ Inductive match_globalenvs (F: meminj) (bound: Z): Prop :=
       (DOMAIN: forall b, b < bound -> F b = Some(b, 0))
       (IMAGE: forall b1 b2 delta, F b1 = Some(b2, delta) -> b2 < bound -> b1 = b2)
       (SYMBOLS: forall id b, Genv.find_symbol ge id = Some b -> b < bound)
-      (INFOS: forall b gv, Genv.find_var_info ge b = Some gv -> b < bound).
+      (FUNCTIONS: forall b fd, Genv.find_funct_ptr ge b = Some fd -> b < bound)
+      (VARINFOS: forall b gv, Genv.find_var_info ge b = Some gv -> b < bound).
 
 Lemma find_function_agree:
   forall ros rs fd F ctx rs' bound,
@@ -374,9 +375,9 @@ Proof.
     exploit Genv.find_funct_inv; eauto. intros [b EQ].
     assert (A: val_inject F rs#r rs'#(sreg ctx r)). eapply agree_val_reg; eauto.
     rewrite EQ in A; inv A.
-    inv H1. rewrite DOMAIN in H5. inv H5. auto. 
-    rewrite EQ in H; rewrite Genv.find_funct_find_funct_ptr in H.
-    exploit Genv.find_funct_ptr_negative. unfold ge in H; eexact H. omega.
+    inv H1. rewrite DOMAIN in H5. inv H5. auto.
+    apply FUNCTIONS with fd. 
+    rewrite EQ in H; rewrite Genv.find_funct_find_funct_ptr in H. auto.
   rewrite H2. eapply functions_translated; eauto.
   (* symbol *)
   rewrite symbols_preserved. destruct (Genv.find_symbol ge id); try discriminate.
@@ -1219,7 +1220,8 @@ Proof.
     apply Mem.nextblock_pos.
     unfold Mem.flat_inj. apply zlt_true; auto. 
     unfold Mem.flat_inj in H. destruct (zlt b1 (Mem.nextblock m0)); congruence.
-    eapply Genv.find_symbol_not_fresh; eauto. 
+    eapply Genv.find_symbol_not_fresh; eauto.
+    eapply Genv.find_funct_ptr_not_fresh; eauto.
     eapply Genv.find_var_info_not_fresh; eauto. 
     omega.
   eapply Genv.initmem_inject; eauto.
diff --git a/backend/Inliningspec.v b/backend/Inliningspec.v
index ec72290..84bcdcd 100644
--- a/backend/Inliningspec.v
+++ b/backend/Inliningspec.v
@@ -35,43 +35,30 @@ Definition fenv_compat (ge: genv) (fenv: funenv) : Prop :=
   fenv!id = Some f -> Genv.find_symbol ge id = Some b ->
   Genv.find_funct_ptr ge b = Some (Internal f).
 
-Remark add_fundef_compat:
-  forall ge fenv idf,
+Remark add_globdef_compat:
+  forall ge fenv idg,
   fenv_compat ge fenv ->
-  fenv_compat (Genv.add_function ge idf) (Inlining.add_fundef fenv idf).
+  fenv_compat (Genv.add_global ge idg) (Inlining.add_globdef fenv idg).
 Proof.
-  intros. destruct idf as [id fd]. red; simpl; intros.
+  intros. destruct idg as [id gd]. red; simpl; intros.
   unfold Genv.find_symbol in H1; simpl in H1. 
   unfold Genv.find_funct_ptr; simpl.
   rewrite PTree.gsspec in H1. destruct (peq id0 id).
   (* same *)
-  subst id0. inv H1. rewrite ZMap.gss. 
-  destruct fd. destruct (should_inline id f0).
-  rewrite PTree.gss in H0. inv H0; auto.
+  subst id0. inv H1. destruct gd. destruct f0. 
+  destruct (should_inline id f0).
+  rewrite PTree.gss in H0. rewrite ZMap.gss. inv H0; auto.
+  rewrite PTree.grs in H0; discriminate.
   rewrite PTree.grs in H0; discriminate.
   rewrite PTree.grs in H0; discriminate.
   (* different *)
-  rewrite ZMap.gso. eapply H; eauto.
-  destruct fd. destruct (should_inline id f0).
+  destruct gd. rewrite ZMap.gso. eapply H; eauto. 
+  destruct f0. destruct (should_inline id f0).
   rewrite PTree.gso in H0; auto.
   rewrite PTree.gro in H0; auto.
   rewrite PTree.gro in H0; auto.
-  exploit Genv.genv_symb_range; eauto. intros [A B]. unfold ZIndexed.t; omega. 
-Qed.
-
-Remark remove_vardef_compat:
-  forall ge fenv idv,
-  fenv_compat ge fenv ->
-  fenv_compat (Genv.add_variable ge idv) (Inlining.remove_vardef fenv idv).
-Proof.
-  intros. destruct idv as [id vi]. red; simpl; intros.
-  unfold Genv.find_symbol in H1; simpl in H1. 
-  unfold Genv.find_funct_ptr; simpl.
-  unfold remove_vardef in H0; simpl in H0.
-  rewrite PTree.gsspec in H1. rewrite PTree.grspec in H0. 
-  unfold PTree.elt_eq in H0. destruct (peq id0 id).
-  discriminate.
-  eapply H; eauto.
+  exploit Genv.genv_symb_range; eauto. intros [A B]. unfold ZIndexed.t; omega.
+  rewrite PTree.gro in H0; auto. eapply H; eauto. 
 Qed.
 
 Lemma funenv_program_compat:
@@ -79,17 +66,11 @@ Lemma funenv_program_compat:
 Proof.
   intros.
   unfold Genv.globalenv, funenv_program.
-  assert (forall funs ge fenv,
-         fenv_compat ge fenv ->
-         fenv_compat (Genv.add_functions ge funs) (fold_left add_fundef funs fenv)).
-    unfold Genv.add_functions. induction funs; simpl; intros.
-    auto. apply IHfuns. apply add_fundef_compat; auto.
-  assert (forall vars ge fenv,
+  assert (forall gl ge fenv,
          fenv_compat ge fenv ->
-         fenv_compat (Genv.add_variables ge vars) (fold_left remove_vardef vars fenv)).
-    unfold Genv.add_variables. induction vars; simpl; intros.
-    auto. apply IHvars. apply remove_vardef_compat; auto.
-  apply H0. apply H. red; intros. rewrite PTree.gempty in H1; discriminate.
+         fenv_compat (Genv.add_globals ge gl) (fold_left add_globdef gl fenv)).
+    induction gl; simpl; intros. auto. apply IHgl. apply add_globdef_compat; auto. 
+  apply H. red; intros. rewrite PTree.gempty in H0; discriminate.
 Qed.
 
 (** ** Soundness of the computed bounds over function resources *)
diff --git a/backend/LTLintyping.v b/backend/LTLintyping.v
index 1a20f73..e9cc2df 100644
--- a/backend/LTLintyping.v
+++ b/backend/LTLintyping.v
@@ -122,4 +122,4 @@ Inductive wt_fundef: fundef -> Prop :=
       wt_fundef (Internal f).
 
 Definition wt_program (p: program): Prop :=
-  forall i f, In (i, f) (prog_funct p) -> wt_fundef f.
+  forall i f, In (i, Gfun f) (prog_defs p) -> wt_fundef f.
diff --git a/backend/LTLtyping.v b/backend/LTLtyping.v
index 40a584f..2e627e9 100644
--- a/backend/LTLtyping.v
+++ b/backend/LTLtyping.v
@@ -142,4 +142,4 @@ Inductive wt_fundef: fundef -> Prop :=
       wt_fundef (Internal f).
 
 Definition wt_program (p: program): Prop :=
-  forall i f, In (i, f) (prog_funct p) -> wt_fundef f.
+  forall i f, In (i, Gfun f) (prog_defs p) -> wt_fundef f.
diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v
index 3930da3..da73b00 100644
--- a/backend/Lineartyping.v
+++ b/backend/Lineartyping.v
@@ -133,7 +133,7 @@ Inductive wt_fundef: fundef -> Prop :=
       wt_fundef (Internal f).
 
 Definition wt_program (p: program) : Prop :=
-  forall i f, In (i, f) (prog_funct p) -> wt_fundef f.
+  forall i f, In (i, Gfun f) (prog_defs p) -> wt_fundef f.
 
 (** Typing the run-time state.  These definitions are used in [Stackingproof]. *)
 
diff --git a/backend/Machtyping.v b/backend/Machtyping.v
index 2d8c83d..b9d8009 100644
--- a/backend/Machtyping.v
+++ b/backend/Machtyping.v
@@ -111,4 +111,4 @@ Inductive wt_fundef: fundef -> Prop :=
       wt_fundef (Internal f).
 
 Definition wt_program (p: program) : Prop :=
-  forall i f, In (i, f) (prog_funct p) -> wt_fundef f.
+  forall i f, In (i, Gfun f) (prog_defs p) -> wt_fundef f.
diff --git a/backend/PrintCminor.ml b/backend/PrintCminor.ml
index 858ef21..8e49303 100644
--- a/backend/PrintCminor.ml
+++ b/backend/PrintCminor.ml
@@ -273,13 +273,6 @@ let print_extfun p id ef =
   fprintf p "@[<v 0>extern @[<hov 2>\"%s\":@ %a@]@ "
     (extern_atom id) print_sig (ef_sig ef)
 
-let print_fundef p (id, fd) =
-  match fd with
-  | External ef ->
-      print_extfun p id ef
-  | Internal f ->
-      print_function p id f
-
 let print_init_data p = function
   | Init_int8 i -> fprintf p "int8 %ld" (camlint_of_coqint i)
   | Init_int16 i -> fprintf p "int16 %ld" (camlint_of_coqint i)
@@ -306,14 +299,18 @@ let print_globvar p gv =
   print_init_data_list p gv.gvar_init;
   fprintf p "}"
 
-let print_var p (id, gv) =
-  fprintf p "var \"%s\" %a\n" (extern_atom id) print_globvar gv
+let print_globdef p (id, gd) =
+  match gd with
+  | Gfun(External ef) ->
+      print_extfun p id ef
+  | Gfun(Internal f) ->
+      print_function p id f
+  | Gvar gv ->
+     fprintf p "var \"%s\" %a\n" (extern_atom id) print_globvar gv
 
 let print_program p prog =
-  fprintf p "@[<v>";
-  List.iter (print_var p) prog.prog_vars;
-  fprintf p "@]@[<v 0>";
-  List.iter (print_fundef p) prog.prog_funct;
+  fprintf p "@[<v 0>";
+  List.iter (print_globdef p) prog.prog_defs;
   fprintf p "@]@."
 
 let destination : string option ref = ref None
diff --git a/backend/PrintLTLin.ml b/backend/PrintLTLin.ml
index bb360eb..4dc311c 100644
--- a/backend/PrintLTLin.ml
+++ b/backend/PrintLTLin.ml
@@ -95,13 +95,13 @@ let print_function pp id f =
   List.iter (print_instruction pp) f.fn_code;
   fprintf pp "@;<0 -2>}@]@."
 
-let print_fundef pp (id, fd) =
-  match fd with
-  | Internal f -> print_function pp id f
-  | External _ -> ()
+let print_globdef pp (id, gd) =
+  match gd with
+  | Gfun(Internal f) -> print_function pp id f
+  | _ -> ()
 
 let print_program pp prog =
-  List.iter (print_fundef pp) prog.prog_funct
+  List.iter (print_globdef pp) prog.prog_defs
 
 let destination : string option ref = ref None
 
diff --git a/backend/PrintMach.ml b/backend/PrintMach.ml
index 03977a6..dfbc66e 100644
--- a/backend/PrintMach.ml
+++ b/backend/PrintMach.ml
@@ -102,13 +102,13 @@ let print_function pp id f =
   List.iter (print_instruction pp) f.fn_code;
   fprintf pp "@;<0 -2>}@]@."
 
-let print_fundef pp (id, fd) =
-  match fd with
-  | Internal f -> print_function pp id f
-  | External _ -> ()
+let print_globdef pp (id, gd) =
+  match gd with
+  | Gfun(Internal f) -> print_function pp id f
+  | _ -> ()
 
 let print_program pp prog =
-  List.iter (print_fundef pp) prog.prog_funct
+  List.iter (print_globdef pp) prog.prog_defs
 
 let destination : string option ref = ref None
 
diff --git a/backend/PrintRTL.ml b/backend/PrintRTL.ml
index 4fc8f56..4cd3871 100644
--- a/backend/PrintRTL.ml
+++ b/backend/PrintRTL.ml
@@ -103,13 +103,13 @@ let print_function pp id f =
   List.iter (print_instruction pp) instrs;
   fprintf pp "@;<0 -2>}@]@."
 
-let print_fundef pp (id, fd) =
-  match fd with
-  | Internal f -> print_function pp id f
-  | External _ -> ()
+let print_globdef pp (id, gd) =
+  match gd with
+  | Gfun(Internal f) -> print_function pp id f
+  | _ -> ()
 
 let print_program pp (prog: RTL.program) =
-  List.iter (print_fundef pp) prog.prog_funct
+  List.iter (print_globdef pp) prog.prog_defs
 
 let print_if optdest prog =
   match !optdest with
diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v
index 65506c8..a14e944 100644
--- a/backend/RTLtyping.v
+++ b/backend/RTLtyping.v
@@ -158,7 +158,7 @@ Inductive wt_fundef: fundef -> Prop :=
       wt_fundef (Internal f).
 
 Definition wt_program (p: program): Prop :=
-  forall i f, In (i, f) (prog_funct p) -> wt_fundef f.
+  forall i f, In (i, Gfun f) (prog_defs p) -> wt_fundef f.
 
 (** * Type inference *)
 
diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v
index 1cfb738..1d87ad3 100644
--- a/backend/Stackingproof.v
+++ b/backend/Stackingproof.v
@@ -1734,7 +1734,8 @@ Inductive match_globalenvs (j: meminj) (bound: Z) : Prop :=
       (DOMAIN: forall b, b < bound -> j b = Some(b, 0))
       (IMAGE: forall b1 b2 delta, j b1 = Some(b2, delta) -> b2 < bound -> b1 = b2)
       (SYMBOLS: forall id b, Genv.find_symbol ge id = Some b -> b < bound)
-      (INFOS: forall b gv, Genv.find_var_info ge b = Some gv -> b < bound).
+      (FUNCTIONS: forall b fd, Genv.find_funct_ptr ge b = Some fd -> b < bound)
+      (VARINFOS: forall b gv, Genv.find_var_info ge b = Some gv -> b < bound).
 
 Inductive match_stacks (j: meminj) (m m': mem): 
        list Linear.stackframe -> list stackframe -> signature -> Z -> Z -> Prop :=
@@ -2170,9 +2171,8 @@ Proof.
   exploit function_ptr_translated; eauto. intros [tf [A B]].
   exists b; exists tf; split; auto. simpl.
   generalize (AG m0). rewrite EQ. intro INJ. inv INJ.
-  exploit Genv.find_funct_ptr_negative. unfold ge in FF; eexact FF. intros. 
-  inv MG. rewrite (DOMAIN b) in H2. inv H2. auto. omega. 
-  revert FF. case_eq (Genv.find_symbol ge i); intros; try discriminate. 
+  inv MG. rewrite DOMAIN in H2. inv H2. simpl. auto. eapply FUNCTIONS; eauto. 
+  destruct (Genv.find_symbol ge i) as [b|]_eqn; try discriminate. 
   exploit function_ptr_translated; eauto. intros [tf [A B]].
   exists b; exists tf; split; auto. simpl. 
   rewrite symbols_preserved. auto.
@@ -2742,6 +2742,7 @@ Proof.
     intros. unfold Mem.flat_inj. apply zlt_true; auto.
     unfold Mem.flat_inj; intros. destruct (zlt b1 (Mem.nextblock m0)); congruence.
     intros. change (Mem.valid_block m0 b0). eapply Genv.find_symbol_not_fresh; eauto.
+    intros. change (Mem.valid_block m0 b0). eapply Genv.find_funct_ptr_not_fresh; eauto.
     intros. change (Mem.valid_block m0 b0). eapply Genv.find_var_info_not_fresh; eauto.
   rewrite H3. red; intros. contradiction.
   eapply Genv.find_funct_ptr_prop. eexact wt_prog. 
diff --git a/backend/Unusedglob.ml b/backend/Unusedglob.ml
index 4139678..1a88ee9 100644
--- a/backend/Unusedglob.ml
+++ b/backend/Unusedglob.ml
@@ -28,10 +28,6 @@ let add_referenced_instr rf i =
 let referenced_function f =
   List.fold_left add_referenced_instr IdentSet.empty (code_of_function f)
 
-let referenced_fundef = function
-  | Internal f -> referenced_function f
-  | External ef -> IdentSet.empty
-
 (* The set of globals referenced from a variable definition (initialization) *)
 
 let add_referenced_init_data rf = function
@@ -43,10 +39,15 @@ let referenced_globvar gv =
 
 (* The map global |-> set of globals it references *)
 
+let referenced_globdef gd =
+  match gd with
+  | Gfun(Internal f) -> referenced_function f
+  | Gfun(External ef) -> IdentSet.empty
+  | Gvar gv -> referenced_globvar gv
+
 let use_map p =
-  List.fold_left (fun m (id, gv) -> PTree.set id (referenced_globvar gv) m)
-  (List.fold_left (fun m (id, fd) -> PTree.set id (referenced_fundef fd) m)
-   PTree.empty p.prog_funct) p.prog_vars
+  List.fold_left (fun m (id, gd) -> PTree.set id (referenced_globdef gd) m)
+    PTree.empty p.prog_defs
 
 (* Worklist algorithm computing the set of used globals *)
 
@@ -66,9 +67,8 @@ let add_nonstatic wrk id =
   if C2C.atom_is_static id then wrk else id :: wrk
 
 let initial_worklist p =
-  List.fold_left (fun wrk (id, gv) -> add_nonstatic wrk id)
-   (List.fold_left (fun wrk (id, fd) -> add_nonstatic wrk id)
-     [] p.prog_funct) p.prog_vars
+  List.fold_left (fun wrk (id, gd) -> add_nonstatic wrk id)
+    [] p.prog_defs
 
 (* Eliminate unused definitions *)
 
@@ -80,9 +80,8 @@ let rec filter used = function
       else filter used rem
 
 let filter_prog used p =
-  { prog_funct = filter used p.prog_funct;
-    prog_main = p.prog_main;
-    prog_vars = filter used p.prog_vars }
+  { prog_defs = filter used p.prog_defs;
+    prog_main = p.prog_main }
 
 (* Entry point *)