From ce4951549999f403446415c135ad1403a16a15c3 Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 12 Nov 2012 13:42:22 +0000 Subject: 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 --- backend/Constprop.v | 20 ++++++++++++-------- 1 file changed, 12 insertions(+), 8 deletions(-) (limited to 'backend/Constprop.v') diff --git a/backend/Constprop.v b/backend/Constprop.v index 104aa3bb..fc242e18 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. -- cgit