From 0053b1aa1d26da5d1f995a603b127daf799c2da9 Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 21 May 2012 16:26:30 +0000 Subject: Merge of the newmem branch: - Revised memory model with Max and Cur permissions, but without bounds - Constant propagation of 'const' globals - Function inlining at RTL level - (Unprovable) elimination of unreferenced static definitions git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1899 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Inliningaux.ml | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) create mode 100644 backend/Inliningaux.ml (limited to 'backend/Inliningaux.ml') diff --git a/backend/Inliningaux.ml b/backend/Inliningaux.ml new file mode 100644 index 0000000..4212916 --- /dev/null +++ b/backend/Inliningaux.ml @@ -0,0 +1,18 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +open Camlcoq + +(* To be considered: heuristics based on size of function? *) + +let should_inline (id: AST.ident) (f: RTL.coq_function) = + C2C.atom_is_inline id -- cgit v1.2.3