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/Inlining.v | 18 +++++++----------- 1 file changed, 7 insertions(+), 11 deletions(-) (limited to 'backend/Inlining.v') diff --git a/backend/Inlining.v b/backend/Inlining.v index 406447b7..3ddfe9a4 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. *) -- cgit